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

Tadashi MATSUMOTO; Ken SAIKUSA; Shinichi YAMAZAKI

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

Tadashi MATSUMOTO, Ken SAIKUSA, Shinichi YAMAZAKI

Full Text Views

0

Cite this

Summary :

Petri nets are useful in modeling and analyzing various types of discrete-event systems such as parallel processing systems, distributed systems, and sequential control systems, because Petri nets can easily be used to represent such properties of these systems as concurrency, nondecidability, and causality. Various behavioral analytic problems on Petri nets are reduced to reachability and liveness on them. It is also known that the decidability of liveness is equivalent to that of reachability which is solvable. However, useful necessary and sufficient structural liveness conditions have been given only for extended free-choice (EFC) nets and their subclasses. Moreover recently, a necessary and sufficient structural liveness condition for a useful subclass N_KT=(S_KT, T_KT, F_KT, M_oKT) (i.e., a Petri net in which each minimal structural deadlock (MSDL) contains at least one real or virtual kindling trap, each locally structural-live MSDL N_D=(S_D, T_D, F_D, M_oD) is never globally dead even if all key transitions for local liveness of each MSDL are controlled by the net of S_KTS_D s.t. S_KTS_D, and there exists no singular MSDL of type (α)) has also been given. In this paper, in order to give one of the bases for a necessary and sufficient "structural" or "initial-marking-based" liveness condition for a general Petri net N, we will, first, directly present a necessary and sufficient local liveness condition for each MSDL with a real deadlock-trap structure in a subclass Ñ (N) using the net structure and initial token distribution and extending basic concepts used in N_KT, where Ñ is a general Petri net without live behavioral traps, local liveness means a useful necessary condition for the above final goal, and real deadlock-trap structure means that each MSDL in Ñ contains at least one minimal structural trap. Secondly, a new subclass is shown in which, if the above locally structural liveness condition for each MSDL holds, then the whole-net liveness is also guaranteed. It is also argued that the obtained results are applicable to describing new live behavioral traps and deriving a necessary and sufficient structural liveness condition, which is the final goal in this work, for a general Petri net N.

Publication: IEICE TRANSACTIONS on Fundamentals Vol.E78-A No.12 pp.1848-1861

Publication Date: 1995/12/25

Publicized

Online ISSN

DOI

Type of Manuscript: PAPER

Category: Concurrent Systems

Cite this

Copy

Tadashi MATSUMOTO, Ken SAIKUSA, Shinichi YAMAZAKI, "Necessary and Sufficient Condition of Structural Liveness for General Petri Nets--Real Deadlock-Trap Properties--" in IEICE TRANSACTIONS on Fundamentals, vol. E78-A, no. 12, pp. 1848-1861, December 1995, doi: .
Abstract: Petri nets are useful in modeling and analyzing various types of discrete-event systems such as parallel processing systems, distributed systems, and sequential control systems, because Petri nets can easily be used to represent such properties of these systems as concurrency, nondecidability, and causality. Various behavioral analytic problems on Petri nets are reduced to reachability and liveness on them. It is also known that the decidability of liveness is equivalent to that of reachability which is solvable. However, useful necessary and sufficient structural liveness conditions have been given only for extended free-choice (EFC) nets and their subclasses. Moreover recently, a necessary and sufficient structural liveness condition for a useful subclass N_KT=(S_KT, T_KT, F_KT, M_oKT) (i.e., a Petri net in which each minimal structural deadlock (MSDL) contains at least one real or virtual kindling trap, each locally structural-live MSDL N_D=(S_D, T_D, F_D, M_oD) is never globally dead even if all key transitions for local liveness of each MSDL are controlled by the net of S_KTS_D s.t. S_KTS_D, and there exists no singular MSDL of type (α)) has also been given. In this paper, in order to give one of the bases for a necessary and sufficient "structural" or "initial-marking-based" liveness condition for a general Petri net N, we will, first, directly present a necessary and sufficient local liveness condition for each MSDL with a real deadlock-trap structure in a subclass Ñ (N) using the net structure and initial token distribution and extending basic concepts used in N_KT, where Ñ is a general Petri net without live behavioral traps, local liveness means a useful necessary condition for the above final goal, and real deadlock-trap structure means that each MSDL in Ñ contains at least one minimal structural trap. Secondly, a new subclass is shown in which, if the above locally structural liveness condition for each MSDL holds, then the whole-net liveness is also guaranteed. It is also argued that the obtained results are applicable to describing new live behavioral traps and deriving a necessary and sufficient structural liveness condition, which is the final goal in this work, for a general Petri net N.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e78-a_12_1848/_p

Copy

@ARTICLE{e78-a_12_1848,
author={Tadashi MATSUMOTO, Ken SAIKUSA, Shinichi YAMAZAKI, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Necessary and Sufficient Condition of Structural Liveness for General Petri Nets--Real Deadlock-Trap Properties--},
year={1995},
volume={E78-A},
number={12},
pages={1848-1861},
abstract={Petri nets are useful in modeling and analyzing various types of discrete-event systems such as parallel processing systems, distributed systems, and sequential control systems, because Petri nets can easily be used to represent such properties of these systems as concurrency, nondecidability, and causality. Various behavioral analytic problems on Petri nets are reduced to reachability and liveness on them. It is also known that the decidability of liveness is equivalent to that of reachability which is solvable. However, useful necessary and sufficient structural liveness conditions have been given only for extended free-choice (EFC) nets and their subclasses. Moreover recently, a necessary and sufficient structural liveness condition for a useful subclass N_KT=(S_KT, T_KT, F_KT, M_oKT) (i.e., a Petri net in which each minimal structural deadlock (MSDL) contains at least one real or virtual kindling trap, each locally structural-live MSDL N_D=(S_D, T_D, F_D, M_oD) is never globally dead even if all key transitions for local liveness of each MSDL are controlled by the net of S_KTS_D s.t. S_KTS_D, and there exists no singular MSDL of type (α)) has also been given. In this paper, in order to give one of the bases for a necessary and sufficient "structural" or "initial-marking-based" liveness condition for a general Petri net N, we will, first, directly present a necessary and sufficient local liveness condition for each MSDL with a real deadlock-trap structure in a subclass Ñ (N) using the net structure and initial token distribution and extending basic concepts used in N_KT, where Ñ is a general Petri net without live behavioral traps, local liveness means a useful necessary condition for the above final goal, and real deadlock-trap structure means that each MSDL in Ñ contains at least one minimal structural trap. Secondly, a new subclass is shown in which, if the above locally structural liveness condition for each MSDL holds, then the whole-net liveness is also guaranteed. It is also argued that the obtained results are applicable to describing new live behavioral traps and deriving a necessary and sufficient structural liveness condition, which is the final goal in this work, for a general Petri net N.},
keywords={},
doi={},
ISSN={},
month={December},}

Copy

TY - JOUR
TI - Necessary and Sufficient Condition of Structural Liveness for General Petri Nets--Real Deadlock-Trap Properties--
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 1848
EP - 1861
AU - Tadashi MATSUMOTO
AU - Ken SAIKUSA
AU - Shinichi YAMAZAKI
PY - 1995
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E78-A
IS - 12
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - December 1995
AB - Petri nets are useful in modeling and analyzing various types of discrete-event systems such as parallel processing systems, distributed systems, and sequential control systems, because Petri nets can easily be used to represent such properties of these systems as concurrency, nondecidability, and causality. Various behavioral analytic problems on Petri nets are reduced to reachability and liveness on them. It is also known that the decidability of liveness is equivalent to that of reachability which is solvable. However, useful necessary and sufficient structural liveness conditions have been given only for extended free-choice (EFC) nets and their subclasses. Moreover recently, a necessary and sufficient structural liveness condition for a useful subclass N_KT=(S_KT, T_KT, F_KT, M_oKT) (i.e., a Petri net in which each minimal structural deadlock (MSDL) contains at least one real or virtual kindling trap, each locally structural-live MSDL N_D=(S_D, T_D, F_D, M_oD) is never globally dead even if all key transitions for local liveness of each MSDL are controlled by the net of S_KTS_D s.t. S_KTS_D, and there exists no singular MSDL of type (α)) has also been given. In this paper, in order to give one of the bases for a necessary and sufficient "structural" or "initial-marking-based" liveness condition for a general Petri net N, we will, first, directly present a necessary and sufficient local liveness condition for each MSDL with a real deadlock-trap structure in a subclass Ñ (N) using the net structure and initial token distribution and extending basic concepts used in N_KT, where Ñ is a general Petri net without live behavioral traps, local liveness means a useful necessary condition for the above final goal, and real deadlock-trap structure means that each MSDL in Ñ contains at least one minimal structural trap. Secondly, a new subclass is shown in which, if the above locally structural liveness condition for each MSDL holds, then the whole-net liveness is also guaranteed. It is also argued that the obtained results are applicable to describing new live behavioral traps and deriving a necessary and sufficient structural liveness condition, which is the final goal in this work, for a general Petri net N.
ER -