On supervisory policies that enforce liveness in a class of completely controlled Petri nets obtained via refinement

The authors consider Petri nets (PNs), where each transition can be prevented from firing by an external agent, the supervisor. 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 proposed previously by the author (1996) involves the construction of the coverability graph, which can be computationally expensive. Using the refinement/abstraction procedure of Suzuki and Murata (1983), where a single transition in a 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 PNs, 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.