The existence of supervisory policies that enforce liveness in discrete event dynamic systems modeled by partially controlled Petri nets is undecidable

We consider discrete-state plants represented by controlled Petri nets (CPN). A supervisory policy can be thought as an implicitly defined table that lists the transitions permitted to fire for each reachable marking. The set of transitions in a CPN is partitioned into controllable and uncontrollable transitions. Any transition in a CPN is state-enabled at a given marking if every input place to the said transition has a nonzero token-load. Similarly, a transition in a CPN is control-enabled at a given marking if the supervisory policy permits the firing of the said transition. Uncontrollable transitions are always control-enabled, while controllable transition can be control-disabled, if deemed necessary. The transition in a CPN has to be state-enabled and control-enabled to fire. A transition in a CPN 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 is control-enabled and state-enabled. A supervisory policy enforces liveness if every transition in the CPN is live under supervision. In this paper we show that the existence of a supervisory policy that enforces liveness for an arbitrary CPN is undecidable