On a minimally restrictive supervisory policy that enforces liveness in partially controlled free choice Petri nets

A Petri net (PN) is said to be live if it is possible to fire any transition from every reachable marking, although not necessarily immediately. Under appropriate conditions, a non-live PN can be made live via supervision. Under this paradigm an external-agent, the supervisor, prevents the firing of certain transitions at each reachable marking so as to enforce liveness. A PN is partially controlled if the supervisor can prevent the firing of only a subset of transitions. A free choice Petri net (FCPN) is a PN where every arc from a place to a transition is either the unique output arc from that place, or, it is the unique input arc to the transition. We show for each partially controlled FCPN that can be made live via supervision, any marking that is reachable under a policy that enforces liveness should cover a member of a specific, finite set of minimal-markings. Assuming this set is readily available, this observation is used to: 1) test the existence, and 2) synthesize a minimally restrictive supervisory policy that enforces liveness in a partially controllable FCPN. We suggest investigations into the computation of this specific, finite set of minimal markings as a future research topic