𝒯-liveness enforcement in Petri nets based on structural net properties

We introduce a semi-decidable procedure which, given a Petri net structure and a set 𝒯 of transitions, synthesizes a supervisor enforcing the transitions in 𝒯 to be live. We call this liveness property 𝒯-liveness. When 𝒯 equals the total set of Petri net transitions, 𝒯-liveness corresponds to liveness. Enforcing only a subset of transitions to be live is useful when some Petri net transitions model undesired events such as failures, and/or when the Petri net structure does not allow enforcing all transitions to be live. The supervisors generated by our procedure are often least restrictive, and their synthesis is independent of the initial marking. No assumptions are made on the Petri net structure: the Petri nets may be unbounded and have integer weights. We have extended the procedure to Petri nets having uncontrollable and unobservable transitions, however, in this paper we restrict our attention to fully controllable and observable Petri nets