Necessary and Sufficient Condition of Structural Liveness for General Petri Nets with Globally Structural Live Minimal Deadlocks

Tadashi MATSUMOTO; Shinichi YAMAZAKI

Necessary and Sufficient Condition of Structural Liveness for General Petri Nets with Globally Structural Live Minimal Deadlocks

Tadashi MATSUMOTO, Shinichi YAMAZAKI

Full Text Views

0

Cite this

Summary :

If a general Petri net N = (S, T, F, M_o) is transition-live under M_o, it is evident that each maximal structural deadlock SDL(_D) in N as well as each minimal structural deadlock MSDL (N_D) in each _D is also transition-live under M_o. However, since the converse of the latter of the above is not always true, it is important to obtain the conditions for this converse to be true if we want to have a useful necessary and sufficient "initial-marking-based" or "structural" liveness condition for N. Up to now, usefull and well-known structural or initial-marking-based necessary and sufficient liveness conditions of Petri nets have only been those of an asymmetric choice (AC) net and its subclasses such as an EFC net, an FC net, an FCF net, MG, and SM. However, all the above subclasses are activated only by real or virtual deadlock-trap properties which are local liveness for each minimal deadlocks; in other words, the above topics of this paper are unconditionally satisfied in those subclasses because of their special structure of nets. In this paper, a necessary and sufficient structural liveness condition for a general Petri net N with globally structural live minimal structural deadlocks is presented as follows: The next () or () is satisfied. () N has no SDL _D. () If N has at least one SDL _D, () or () is satisfied under the condition that each MSDL N_D in N is transition-live under M_o. () N has no singular MSDL (α) (i.e., (α-) and (α-)). () If N has at least one singular MSDL (α-)((α-), resp.), every semi-MDSL ()((), resp.) N_DS = (S_DS, T_DS, F_DS, M_oDS with respect to each singular MSDL (α-)((α-), resp.), is transition-live under the M_oDS under the condition of "the condition (**)", where the locally structural liveness for this N_DS means (1) or (2)((3), resp.) of Lemma 4-4 and "the condition (**)" is defined in Lemma 4-7 of this paper. The relationship between the above results and the liveness problem for N is also shown.

Publication: IEICE TRANSACTIONS on Fundamentals Vol.E78-A No.12 pp.1875-1889

Publication Date: 1995/12/25

Publicized

Online ISSN

DOI

Type of Manuscript: PAPER

Category: Concurrent Systems

Cite this

Copy

Tadashi MATSUMOTO, Shinichi YAMAZAKI, "Necessary and Sufficient Condition of Structural Liveness for General Petri Nets with Globally Structural Live Minimal Deadlocks" in IEICE TRANSACTIONS on Fundamentals, vol. E78-A, no. 12, pp. 1875-1889, December 1995, doi: .
Abstract: If a general Petri net N = (S, T, F, M_o) is transition-live under M_o, it is evident that each maximal structural deadlock SDL(_D) in N as well as each minimal structural deadlock MSDL (N_D) in each _D is also transition-live under M_o. However, since the converse of the latter of the above is not always true, it is important to obtain the conditions for this converse to be true if we want to have a useful necessary and sufficient "initial-marking-based" or "structural" liveness condition for N. Up to now, usefull and well-known structural or initial-marking-based necessary and sufficient liveness conditions of Petri nets have only been those of an asymmetric choice (AC) net and its subclasses such as an EFC net, an FC net, an FCF net, MG, and SM. However, all the above subclasses are activated only by real or virtual deadlock-trap properties which are local liveness for each minimal deadlocks; in other words, the above topics of this paper are unconditionally satisfied in those subclasses because of their special structure of nets. In this paper, a necessary and sufficient structural liveness condition for a general Petri net N with globally structural live minimal structural deadlocks is presented as follows: The next () or () is satisfied. () N has no SDL _D. () If N has at least one SDL _D, () or () is satisfied under the condition that each MSDL N_D in N is transition-live under M_o. () N has no singular MSDL (α) (i.e., (α-) and (α-)). () If N has at least one singular MSDL (α-)((α-), resp.), every semi-MDSL ()((), resp.) N_DS = (S_DS, T_DS, F_DS, M_oDS with respect to each singular MSDL (α-)((α-), resp.), is transition-live under the M_oDS under the condition of "the condition (**)", where the locally structural liveness for this N_DS means (1) or (2)((3), resp.) of Lemma 4-4 and "the condition (**)" is defined in Lemma 4-7 of this paper. The relationship between the above results and the liveness problem for N is also shown.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e78-a_12_1875/_p

Copy

@ARTICLE{e78-a_12_1875,
author={Tadashi MATSUMOTO, Shinichi YAMAZAKI, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Necessary and Sufficient Condition of Structural Liveness for General Petri Nets with Globally Structural Live Minimal Deadlocks},
year={1995},
volume={E78-A},
number={12},
pages={1875-1889},
abstract={If a general Petri net N = (S, T, F, M_o) is transition-live under M_o, it is evident that each maximal structural deadlock SDL(_D) in N as well as each minimal structural deadlock MSDL (N_D) in each _D is also transition-live under M_o. However, since the converse of the latter of the above is not always true, it is important to obtain the conditions for this converse to be true if we want to have a useful necessary and sufficient "initial-marking-based" or "structural" liveness condition for N. Up to now, usefull and well-known structural or initial-marking-based necessary and sufficient liveness conditions of Petri nets have only been those of an asymmetric choice (AC) net and its subclasses such as an EFC net, an FC net, an FCF net, MG, and SM. However, all the above subclasses are activated only by real or virtual deadlock-trap properties which are local liveness for each minimal deadlocks; in other words, the above topics of this paper are unconditionally satisfied in those subclasses because of their special structure of nets. In this paper, a necessary and sufficient structural liveness condition for a general Petri net N with globally structural live minimal structural deadlocks is presented as follows: The next () or () is satisfied. () N has no SDL _D. () If N has at least one SDL _D, () or () is satisfied under the condition that each MSDL N_D in N is transition-live under M_o. () N has no singular MSDL (α) (i.e., (α-) and (α-)). () If N has at least one singular MSDL (α-)((α-), resp.), every semi-MDSL ()((), resp.) N_DS = (S_DS, T_DS, F_DS, M_oDS with respect to each singular MSDL (α-)((α-), resp.), is transition-live under the M_oDS under the condition of "the condition (**)", where the locally structural liveness for this N_DS means (1) or (2)((3), resp.) of Lemma 4-4 and "the condition (**)" is defined in Lemma 4-7 of this paper. The relationship between the above results and the liveness problem for N is also shown.},
keywords={},
doi={},
ISSN={},
month={December},}

Copy

TY - JOUR
TI - Necessary and Sufficient Condition of Structural Liveness for General Petri Nets with Globally Structural Live Minimal Deadlocks
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 1875
EP - 1889
AU - Tadashi MATSUMOTO
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 - If a general Petri net N = (S, T, F, M_o) is transition-live under M_o, it is evident that each maximal structural deadlock SDL(_D) in N as well as each minimal structural deadlock MSDL (N_D) in each _D is also transition-live under M_o. However, since the converse of the latter of the above is not always true, it is important to obtain the conditions for this converse to be true if we want to have a useful necessary and sufficient "initial-marking-based" or "structural" liveness condition for N. Up to now, usefull and well-known structural or initial-marking-based necessary and sufficient liveness conditions of Petri nets have only been those of an asymmetric choice (AC) net and its subclasses such as an EFC net, an FC net, an FCF net, MG, and SM. However, all the above subclasses are activated only by real or virtual deadlock-trap properties which are local liveness for each minimal deadlocks; in other words, the above topics of this paper are unconditionally satisfied in those subclasses because of their special structure of nets. In this paper, a necessary and sufficient structural liveness condition for a general Petri net N with globally structural live minimal structural deadlocks is presented as follows: The next () or () is satisfied. () N has no SDL _D. () If N has at least one SDL _D, () or () is satisfied under the condition that each MSDL N_D in N is transition-live under M_o. () N has no singular MSDL (α) (i.e., (α-) and (α-)). () If N has at least one singular MSDL (α-)((α-), resp.), every semi-MDSL ()((), resp.) N_DS = (S_DS, T_DS, F_DS, M_oDS with respect to each singular MSDL (α-)((α-), resp.), is transition-live under the M_oDS under the condition of "the condition (**)", where the locally structural liveness for this N_DS means (1) or (2)((3), resp.) of Lemma 4-4 and "the condition (**)" is defined in Lemma 4-7 of this paper. The relationship between the above results and the liveness problem for N is also shown.
ER -