Necessary and Sufficient Condition for Liveness of Asymmetric Choice Petri Nets

Tadashi MATSUMOTO; Yasuhiko TSURUTA

Necessary and Sufficient Condition for Liveness of Asymmetric Choice Petri Nets

Tadashi MATSUMOTO, Yasuhiko TSURUTA

Full Text Views

0

Cite this

Summary :

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.

Publication: IEICE TRANSACTIONS on Fundamentals Vol.E80-A No.3 pp.521-533

Publication Date: 1997/03/25

Publicized

Online ISSN

DOI

Type of Manuscript: Special Section PAPER (Special Section of Selected Papers from the 9th Karuizawa Workshop on Circuits and Systems)

Category

Cite this

Copy

Tadashi MATSUMOTO, Yasuhiko TSURUTA, "Necessary and Sufficient Condition for Liveness of Asymmetric Choice Petri Nets" in IEICE TRANSACTIONS on Fundamentals, vol. E80-A, no. 3, pp. 521-533, March 1997, doi: .
Abstract: 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.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e80-a_3_521/_p

Copy

@ARTICLE{e80-a_3_521,
author={Tadashi MATSUMOTO, Yasuhiko TSURUTA, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Necessary and Sufficient Condition for Liveness of Asymmetric Choice Petri Nets},
year={1997},
volume={E80-A},
number={3},
pages={521-533},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={March},}

Copy

TY - JOUR
TI - Necessary and Sufficient Condition for Liveness of Asymmetric Choice Petri Nets
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 521
EP - 533
AU - Tadashi MATSUMOTO
AU - Yasuhiko TSURUTA
PY - 1997
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E80-A
IS - 3
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - March 1997
AB - 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.
ER -