Liveness Analysis of \omega -Independent Petri Nets Based on New Modified Reachability Trees

• Published in: IEEE transactions on systems, man, and cybernetics. Systems man, and cybernetics. Systems, 2017-09, Vol.47 (9), p.2601-2612
• Main Authors: Yang, Ru, Ding, Zhijun, Pan, Meiqin, Jiang, Changjun, Zhou, MengChu
• Format: Article
• Language: English
• Subjects: Algorithm design and analysis; Analytical models; Control theory; Discrete event systems; Intelligent agents; liveness; Petri nets; reachability graph (RG); Subspace constraints; System recovery; Transforms; unbounded Petri net; ω-independent Petri net
• ISSN: 2168-2216; 2168-2232
• DOI: 10.1109/TSMC.2016.2524062

Liveness of Petri nets means all activities in a modeled system can potentially take place and thus implies deadlock freedom. The research on liveness analysis approaches is inadequate. This paper proposes a liveness judgment reachability graph (LJRG) approach to analyze the liveness of ω-independent Petri nets. Such nets can be loosely explained as a class of unbounded Petri nets in which the changes of tokens in unbounded places are not related to each other. This paper proposes several algorithms to transform a new modified reachability tree to a new modified reachability graph and then transform it to an LJRG. It then develops the application of LJRG into the liveness analysis of ω-independent unbounded Petri nets. The proposed method provides a new theoretical method and important tool for the liveness analysis of unbounded Petri nets. It is illustrated via some examples.