Lecture Notes in Computer Science, 2000, Volume 1825/2000, 227-243, DOI: 10.1007/3-540-44988-4_14

Liveness Verification of Discrete Event Systems Modeled by n -Safe Ordinary Petri Nets

Kevin X. He and Michael D. Lemmon

View Related Documents

Abstract

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.

Fulltext Preview

Image of the first page of the fulltext document