The Research Of Petri Nets' Liveness Decision

Liveness is one of the most basic properties of Petri nets, it is crucial to those systems about the safety of life and wealth such as rocket control system, life maintenance system in medicine and safety system of nuclear power plant. In these systems, the inspection and avoidance of deadlocks(one aspect of liveness called as weak liveness decision)are the most important topics in system control. So liveness decision problem is one of the most important topics in Petri nets theory too. Most references analyze liveness of Petri nets by two methods, one of which is to analyze liveness from the structure of Petri nets, which is limited to some subsets of Petri nets with special structure; the other rests on reachable marking graph and is easy and direct. Deciding liveness of bounded Petri nets with its reachable marking graph is easy, but for unbounded Petri nets that are generally existing, finding an algorithm for its liveness decision is not easy. In this paper, we decrease the information losing during unbounded Petri nets running by finding a modified form of reachablity graph, and use this form to propose a way for liveness decision of a subset of Petri nets which is the net system without associated ω- number. Then we improve the modified form in order to lose less information, and propose a method for liveness decision from zero to third-level of any Petri nets by making use of this improved form.