For the most recent entries see the Petri Nets Newsletter.

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

He, Kevin X.; Lemmon, Michael D.

In: Nielsen, M.; Simpson, D.: Lecture Notes in Computer Science, Vol. 1825: 21st International Conference on Application and Theory of Petri Nets (ICATPN 2000), Aarhus, Denmark, June 2000, pages 227-243. Springer-Verlag, 2000.

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.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography