Necessary and Sufficient Condition of Structural Liveness for General Petri Nets : Virtual Deadlock-Trap Properties

スポンサーリンク

概要

• 論文の詳細を見る

• Up to now, the only useful and well-known structural or initial-marking-based necessary and sufficient liveness conditions of Petri nets have only been those of an extended free-choice (EFC) net and its subclasses such as a free-choice (FC) net, a forward conflict free (FCF) net, a marked graph (MG), and a state machine (SM). All the above subclasses are activated only by deadlock-trap properties (i.e., real d-t properties in this paper), which mean that every minimal structural deadlock (MSDL N_D = (S_D, T_D, F_D, M_<oD>)) in a net contains at least one live minimal structural trap (MSTR N_T = (S_T, T_T, F_T, M_<oT>)) which is initially marked. However, the necessary and sufficient liveness conditions for EFCF, EBCF, EMG⊂EFCF∩EBCF, AC (⊃EFC⊃FC), and the net with kindling traps N_<KT> have recently been determined, in which each MSDL without real d-t properties was also activated by a new type of trap, i.e., behavioral traps (BTRs), which are defined by introducing a virtual MSTR, a virtual maximal structural trap (virtual STR), a virtual MSDL, and a virtual maximal structural deadlock (virtual SDL) into a target MSDL. In this paper, a structural or initial-marking-based necessary and sufficient condition for local liveness (i.e., virtual deadlock-trap properties) of each MSDL N_D s. t. S_D ⫋ S_T, S_D ? S_T, S_D ⫆ S_T (but N_D S. t. S_D ⫆ S_T is dead owing to real deadlock-trap properties) in a general Petri net N is presented by extending that in N_<KT>. Specifically, live minimal behavioral traps (MBTRs) as well as live maximal behavioral traps (BTRs), i.e., virtual deadlock-trap properties, in a general Petri net N are characterized using the real d-t properties of each MSDL N_D s. t. S_D ⫆ S_T for a general Petri net N, which were also obtained by exteniding the concept of return paths in N_<KT> in connection with an MSDL which contains at least one MSTR and by using the concepts of T-cornucopias and absolute T-cornucopias in a subclass N of N. In other words, BTRs are defined by introducing a virtual MSTR, a virtual STR, a virtual MSDL, and a virtual SDL into a target MSDL without real d-t properties. Additionally, a structural or initial-marking-based necessary and sufficient condition for liveness of a new subclass N_n of a general Petri net N (i.e., a general Petri net without time) is derived, and the usefulness of the obtained results is also discussed.

• 社団法人電子情報通信学会の論文
• 1995-12-25

著者

• Tsuji Kohkichi

  Faculty Of Engineering Fukui University

• MATSUMOTO Tadashi

  Faculty of Engineering, Fukui University

• Saikusa Ken

  Faculty of Engineering, Fukui University

• Saikusa Ken

  Faculty Of Engineering Fukui University

• Matsumoto Tadashi

  Faculty Of Engineering Fukui University

関連論文

• On Liveness of Extended Partially Ordered Condition Nets (Special Section on Concurrent Systems Technology)
• Necessary and Sufficient Condition for Liveness of Asymmetric Choice Petri Nets (Special Section of Selected Papers from the 9th Karuizawa Workshop on Circuits and Systems)
• Necessary and Sufficient Condition of Structural Liveness for General Petri Nets : Virtual Deadlock-Trap Properties
• A Method to Validate the Correctness of Test Logic Programs Applied in a Protocol Conformance Test System Using Petri Nets (Special Section on Net Theory and Its Applications)
• Computational Complexity of Liveness Problem of Normal Petri Net
• Necessary and Sufficient Condition of Structural Liveness for General Petri Nets : Real Deadlock-Trap Properties
• An Equivalence Net-Condition between Place-Liveness and Transition-Liveness of Petri Nets and Their Initial-Marking-Based Necessary and Sufficient Liveness Conditions
• Verifying Structurally Weakly Persistent Net Is Co-NP Complete

スポンサーリンク