1-3hit |
Tadashi MATSUMOTO Yasuhiko TSURUTA
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.
Tadashi MATSUMOTO Ken SAIKUSA Kohkichi TSUJI
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 ND=(SD, TD, FD, MoD)) in a net contains at least one live minimal structural trap (MSTR NT=(ST, TT, FT, MoT)) which is initially marked. However, the necessary and sufficient liveness conditions for EFCF, EBCF, EMGEFCFEBCF, AC (EFCFC), and the net with kindling traps NKT have recently been determined, in which each MSDL without real d-t properties was also activated by a new type of trap 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 ND s.t. SDST, SD
Tadashi MATSUMOTO Kohkichi TSUJI
The structural necessary and sufficient condition for "the transition-liveness means the place-liveness and vice-versa" of a subclass NII of general Petri nets is given as "the place and transition live Petri net, or PTL net, ÑII". Furthermore, "the one-token-condition Petri net, or OTC net,