Design of T-liveness enforcing supervisors in Petri nets

This paper presents a procedure for the design of supervisors that enforce the transitions in a given set T to be live. T-liveness enforcement corresponds to full liveness enforcement when T equals the total set of transitions. Rather than assuming a given initial marking, this procedure generates at every iteration a convex set of admissible initial markings. In the case of full liveness enforcement and under certain conditions also in the case of T-liveness enforcement, the convex set of each iteration includes the set of markings for which liveness/T-liveness can be enforced. When the procedure terminates, and if it terminates, the final convex set contains only markings for which T-liveness can be enforced. Then, the supervisor keeping the Petri net (PN) marking in this convex set can be easily designed using the place invariant based approach. This paper focuses on the fully controllable and observable PNs. Several extensions of the procedure, including to partially controllable and observable PNs, are outlined.