M. V. Iordache and P. J. Antsaklis
In the Proceedings of the 40th IEEE International Conference on Decision and Control, pp.4984-4989, December 2001.
Abstract -- We introduce a semidecidable procedure which, given a Petri net structure and a set T of transitions, synthesizes a supervisor enforcing the transitions in T to be live. We call this liveness property T-liveness. When T equals the total set of Petri net transitions, T-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.
Slides available: [pdf, 98k]