Liveness Analysis of ω-Independent Petri Nets Based on New Modified Reachability Trees
提出一种活性判断可达图方法，用于分析ω-独立Petri网的活性，通过将新型修正可达树转换为图结构来判断系统是否无死锁，为无界Petri网活性分析提供新工具。
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.