On partially controlled Petri nets that can be made live by supervision

The existence of a supervisory policy that enforces liveness in partially controlled Petri nets (PNs) is undecidable in general (cf. theorem 5.3 and corollary 5.2,). However, there can be families of partially controlled PNs for which the existence of a supervisory policy that enforces liveness can be tested and synthesized. In this paper we present choice-controlled PNs as an example of such a family. Also, there can be specific examples of partially controlled PNs that be made live by supervision. Typically, this is shown by producing a supervisory policy that enforces liveness in the example at hand. There can be no generalization of this approach in light of theorem 5.3 and corollary 5.2 in reference. However, for partially controlled Free-Choice PNs, there is a necessary and sufficient characterization of supervisory policies that enforce liveness. In specific, the necessary and sufficient condition for the existence of a supervisory policy that enforces liveness in a fully controlled Free-Choice Petri Net (FCPN) in reference also holds for partially controlled FCPNs. This condition can be used to verify that a given supervisory policy does enforce liveness in a specific partially controlled FCPN.