On Liveness Enforcing Supervisory Policies for Arbitrary Petri Nets

Neither the existence nor the nonexistence of a liveness enforcing supervisory policy (LESP) for an arbitrary Petri net (PN) is semidecidable. In an attempt to identify decidable instances, we explore the decidability of certain properties of the set of initial markings for which an LESP exists, and the decidability of the existence of a specific class of LESPs. We first prove that for an arbitrary PN structure, determining if there is an initial marking, or there are no initial markings, for which there is an LESP, is not semidecidable. Then, we characterize the class of PN structures for which the set of all initial markings for which an LESP exists is right-closed . We show that testing membership, or nonmembership, of an arbitrary PN in this class of PNs is not semidecidable. We then consider a restricted class of LESPs, called marking monotone LESPs (MM-LESPs). We show that the existence of an MM-LESP for an arbitrary PN is decidable.