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 live 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 Ǹ to yield a larger refined PN N̂, we show that when Ǹ 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̂ 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.