Liveness enforcing supervisory policies tolerant to controllability failures for discrete-event systems modeled by Petri Nets

A Discrete Event System (DES) modeled by a Petri Net (PN) is live if it is possible to fire any transition, although not necessarily immediately, from any marking that is reachable from the initial marking. A Liveness Enforcing Supervisory Policy (LESP) for a PN enforces liveness by preventing the firing of a subset of transitions called the controllable transitions, which correspond to the preventable events in a DES.