Minimum Number of Live Minimal Structural Traps to Make a Minimal Deadlock Locally Live in General Petri Nets

概要

論文の詳細を見る
Petri nets are one of useful models for discrete event systems in which liveness problem as well as reachability problem is one of big issues. But, it has not been completely solved from the point of view of useful initial-marking-based liveness conditions in general Petri nets. In this paper, to guarantee local liveness (i.e., liveness under M_<OD>) for each minimal deadlock (MSDL), N_D=(S_D, T_D, F_D, M_<OD>), with real deadlock-trap structure, it is shown that the minimum number of required live minimal structural traps (MSTRs), N_T=(S_T, T_T, F_T, M_<OT>) s.t. S_D⫆S_T, is conditionally (which means that the conditions of Lemma 4-9 are fulfilled for a bounded MSDL ND containing at least one MSTR N_T s.t. S_D⫌S_T and see also Remarks 4-2(3) in Sect.4.3) "one." Note that this local liveness for N_D s.t. S_D⫆S_T is one of useful necessary Conditions for liveness condition of general Petri nets N=(S, T, F, M_O) s.t. S⫆S_D. However, because this has not been discussed in literature and is not trivial, some new concepts such as T-cornucopias and return paths are introduced into the real deadlock-trap structure s.t. S_D⫆S_T in N and this is proven by dividing it into two cases: N_D s.t. S_D⫆S_T is live and unbounded under. M_<OD> and N_D s.t. S_D⫆S_T is live and bounded under M_<OD>). Usefulness for the results obtained is also discussed.
社団法人電子情報通信学会の論文
1998-01-25