T-Liveness Enforcement in Petri Nets Based on Structural Net Properties

M.V. Iordache, P.J. Antsaklis

Proceedings of the 2001 Conference on Decision and Control
pp. 2478-2483. Orlando, FL, USA, December 4-7, 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.

[pdf file]