In: IEEE Trans. on Automatic Control, Vol. 44, No. 1, pages 173-177. 1999.
Abstract: The authors consider Petri nets (PN's), where each transition can be prevented from firing by an external agent, the supervisor. Earlier work provided 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 live if it is possible to fire any transition from every reachable marking, although not necessarily immediately. The procedure involves the construction of the coverability graph which can be computationally expensive. Using the refinement/abstraction procedure of Suzuki and Murata, where a single transition in an abstracted PN, N is replaced by a PN N' to yield a larger refined PN N''. We show that when N' belongs to a class of marked-graph PN's, there is a supervisory policy that enforces liveness in the refined PN N'' 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'', it is possible to achieve significant computational savings by using the process of abstraction on N'. This is illustrated by example.
Keywords: controlled Petri nets, net refinements, supervisory policies.