Research On Property Checking For Unbounded Petri Nets Based On Reachability Trees

Petri net is a mathematical representation of discrete parallel system, and itsuitable for describing asynchronous concurrent computer system model. Petri net hasnot only the rigorous mathematical expression, but also the intuitive graphical way.Among various analysis methods and tools, the reachability tree of a Petri net is afundamental and powerful one for various properties including liveness, boundedness,conservation, reachability, and coverability. Therefore, the research of reachabilitytree is one of the most important topics in Petri Nets theory.At present, there is one mature analysis method—the finite reachability treewhich can analyze the properties of Petri nets. However, this method cannot be usedto solve the deadlock, liveness, or reachability problems for unbounded nets due to theinformation loss resulting from the introduction of the symbol ω. Therefore, In orderto improve the drawbacks of the finite reachability tree, this paper would research intothe improvement of the reachability tree. First, this paper described the basicprinciples, basic properties and methods of the Petri nets, conducted in-depth study onthe basis of the finite reachability tree method, and described the advantages anddisadvantages of the finite reachability tree. By using a positive integer expressiona+bniin place of the original unbounded symbol ω component, we get an idea ofmodified reachability tree. Second, this paper proposed the realization ideas andconstruction algorithm of the modified and improved reachability trees. In the end, byusing the modified and improved reachability trees we can analyze properties of theunbounded Petri nets, and their superiority and differences.The main research results of this paper have been summarized as follows:1. By introducing the ω-expression can represent the unbound information, thispaper achieved up to the construct the modified reachability tree. And focused on thedeadlock criterion of the method, perfected a full conditional node classification. The examples of the application show that the method to improve the shortage of thefinite reachability tree in analyzing the properties of the unbounded Petri nets. Themethod can also be used to solve the liveness, deadlock, and reachability problems.2. By exploring the inner change regularity of the token numbers in theunbounded place, this paper perfected the form of the ω-expression. It compressesexactly all the reachable states into the nodes in the improved reachability tree andfinally achieves the property checking. The examples of the application show that themethod can provide a complete representation of the token numbers in the unboundedplace.The chapters of this paper are organized as follows: First chapter of this paper, itcontains the background and meaning, the current domestic, as well as foreign relatedfields study the status quo. Second chapter of this paper simply described the basicprinciples, basic properties and methods of the Petri nets. Third chapter of this paperanalyzed the drawbacks of the finite reachability tree on the checking of liveness andreachability. Fourth chapter of this paper achieved up to the construct the modifiedreachability tree and check the property. Fifth chapter of this paper achieved up to theconstruct the improved reachability tree and illustrate the improvements andadvantages of the method by some specific examples. Finally, we summarize theresearch work and make the prospect of the further work.In summary, this study is mainly based on the finite reachability treeof unbounded Petri net. In order to improve the drawbacks of checking the propertiesof the unbounded Petri net, this paper achieved up to the construct the modified andimproved reachability trees. The examples of the application show that they can beused to solve the liveness, deadlock, and reachability problems.