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)

概要

論文の詳細を見る
Petri net is a graphical and mathematical tool for modelling, analysis, verification, and evaluation of discrete event systems. Liveness is one of the most important problems of Petri net analysis. This is concerned with a capability for firing of transitions and can be interpreted as a problem to decide whether the system under consideration is always able to reach a stationary behavior, or to decide whether the system is free from any redundant elements. An asymmetric choice (AC) net is a superclass of useful subclasses such as EFCs, FCs, SMs, and MGs, where SMs admit no synchronization, MGs admit no conflicts, FCs as well as EFCs admit no confusion, and ACs allow asymmetric confusion but disallow symmetric confusion. It is known that an AC net N is live iff it is place-live, but this is not the "initial-marking-based" condition and place-liveness is in general hard to test. For the initial-marking-based liveness for AC nets, it is only known that an AC net N is live if (but not only if) every deadlock in N contains a marked structural trap. In this paper, a necessary and sufficient condition for the initial-marking-based liveness of AC nets is given by introducing new behavioral traps, proving real or virtual deadlock-trap properties (i.e., local liveness which is due to Definitions 2-7 and 4-1, respectively) for minimal deadlocks through new approach, and also showing that there needs no global liveness condition in the above sense for each minimal deadlock of AC nets.
社団法人電子情報通信学会の論文
1997-03-25

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)

スポンサーリンク

概要

著者

関連論文

スポンサーリンク