A Method For Reachability Decision Of Live Single Branch Petri-Nets And An Algorithm For Construction Of Improved Coverability Tree

Petri net is a system description and analysis tool.Reachability research is one of the most basic properties of Petri-Nets in all properties research. In a sense, reachability is the foundation of the study on other dynamic property of Petri-Nets, many problems on Petri-Nets can be described by it. So reachability decision problem is one of the most important topics in Petri-Nets theory.At present, there are two mature analysis methods---matrix equation and,but both methods are localized.For the first method, the variable"ω" cause the localization, so the reachability, liveness are not solved by the first method, It also can not sure that if it can fire sequence.For the second method, the matrix A can not appropriately reflect the structure of Petri-Nets, and the sequence information is lacked in firing vectors. Firstly, afterstudying the algorithm for reachability decision of a subnet of live Petri- Nets——live single branch Petri-Nets using local analysis method, three conclusions is proposed and then proved. Secondly, after studying the weighted unbounded Petri-Nets using global analysis method, the reason why the reachability decision of unbounded Petri-Nets can not only depends coverability tree is found.In order to use a limited form to Express the situation of the operating system that has unlimited state,the ICT introduces a "ω" to mark the unbounded variables, so when the place of the token in Petri Nets tends to unlimited Growth, we can use to a "ω" to identify the first j-component, which covers all such a marking.The limitless variable "ω" in it bring the information losing during unbounded Petri-Nets running so that decision of its reachability can not be achieved.Based on idea of using one positive integer equation in place of any positive integer variable "ω"in order to cut the span, an improved node of coverability tree is introduced. This improved method can decrease information losing during unbounded Petri-Nets running by refining the node of coverability tree to sequence node, copied node and prospective node. So the method provide basis of the reachability decision of any Petri-Nets (include unbounded Petri-Nets). The disadvantage of this research is most but not all reachable markings on prospective node are reachable on prospective source node. So the prospective source node and children node must be specially handled in order to guarantee that the rest are not missing. Future work is directed toward special method so that the reachability decision is strict.