On the existence of supervisory policies that enforce liveness in partially controlled free-choice petri nets

We first show that the existence, or nonexistence, of a supervisory policy that enforces liveness in an arbitrary Petri net (PN) is not semidecidable. Following this, we show that this is not the case if we restrict our attention to an arbitrary, partially controlled, free-choice Petri net (FCPN). Starting from the observation that the set of initial markings for which there is a supervisory policy that enforces liveness in a free-choice structure is right-closed, we present a string of observations that eventually lead to the conclusion that the existence of a supervisory policy that enforces liveness in an arbitrary FCPN is decidable. The paper concludes with some suggested directions for future research.