On Supervisory Policies that Enforce Liveness in a Class of Completely Controlled Petri Nets obtained via Refinement

We consider Petri nets (PNs) [3, 5] where each transition can be prevented from firing by an external agent, the supervisor. References [6, 7] 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 references [6, 7] involves the construction of the coverability graph (cf. section 5.1, [3]; section 4.2.1, [5]), 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 e N to yield a larger refined PN b N , we show that when e N belongs to a class of marked-graph PNs (cf. section 6.1, [3]), there is a supervisory policy that enforces liveness in the refined PN b N if and only if there is a similar policy for the abstracted PN N . Since the c..