IEEE Transactions on Automatic Control, Vol.44, No.1, 173-177, 1999
On supervisory policies that enforce liveness in a class of completely controlled Petri nets obtained via refinement
The authors consider Petri nets (PN's) [3], where each transition can be prevented from firing by an external agent, the supervisor. References [5] and [6] contain necessary and sufficient conditions for the existence of a supervisory policy that enforces liveness in a PN that is not live. A PN is said to be lire if it is possible to fire any transition from every reachable marking, although not necessarily immediately. The procedure in [5] and [6] involves the construction of the coverability graph (cf. [3, Sec. 5.1]), which can be computationally expensive. Using the refinement/abstraction procedure of Suzuki and Murata [8], where a single transition in a abstracted PN N is replaced by a PN (N) over tilde to yield a larger refined PN (N) over tilde, we show that when (N) over tilde belongs to a class of marked-graph PN's (cf. [3, Sec. 6.1]), there is a supervisory policy that enforces liveness in the refined PN (N) over cap if and only if there is a similar policy for the abstracted PN N. Since the coverability graph of the PN N is smaller than that of the PN (N) over cap, it is possible to achieve significant computational savings by using the process of abstraction on (N) over cap. This is illustrated by example.