On supervisory policies that enforce liveness in discrete event dynamic systems modeled by partially controlled Petri nets

We consider discrete-state plants represented by controlled Petri nets (CtlPNs). A transition in a CtlPN is live if for every marking reachable under supervision, there exists a valid firing sequence that results in a marking under which the said transition can fire. A supervisory policy enforces liveness if every transition in the CtlPN is live under supervision. In this paper we show that the existence of a supervisory policy that enforces liveness for an arbitrary CtlPN is undecidable