Liveness verification of discrete event systems modeled by n-safe ordinary Petri nets

This paper discusses liveness verification of discrete-event systems modeled by n-safe ordinary Petri nets. A Petri net is live, if it is possible to fire any transition from any reachable marking. The verification method we propose is based on a partial order method called network unfolding. Network unfolding maps the original Petri net to an acyclic occurrence net. A finite prefix of the occurrence net is defined to give a compact representation of the original net's reachability graph. A set of transition cycles is identified in the finite prefix. These cycles are then used to establish necessary and sufficient conditions that determine the original net's liveness.