Deadlock and Liveness Properties of Petri Nets
Systems & control · 2006
This chapter presents new results characterizing deadlock, liveness, and $$ \mathcal{T} $$ -liveness in Petri nets. These results can be useful when dealing with the corresponding supervision problems: deadlock prevention, liveness enforcement, and $$ \mathcal{T} $$ -liveness enforcement. $$ \mathcal{T} $$ -liveness enforcement means ensuring that all transitions in a transition subset $$ \mathcal{T} $$ of a Petri net are live. Deadlock prevention corresponds to preventing the system from reaching a state of total deadlock. Liveness corresponds to the stronger requirement that no local deadlock occurs, or in other words, all transitions are live. $$ \mathcal{T} $$ -liveness means that all transitions in the set $$ \mathcal{T} $$ are live. The concept of $$ \mathcal{T} $$ -liveness is useful in problems in which some transitions correspond to undesirable system events (such as faults) or when the system model contains transitions modeling an initialization process. Unless otherwise stated, supervision in this chapter assumes all transitions are controllable and observable. Note that this does not affect the generality of the main results of the chapter, as they deal with structural net properties rather than supervision.