Analysis for one-place unbounded Petri nets based on modified reachability trees

Analysis approaches of reachability decision is fundamental to Petri nets theory; however, the relevant research work in the past cannot always guarantee the correctness of analysis conclusions. This paper firstly reveals the root cause of wrong conclusions, which are drawn in analysis for deadlock of Petri nets based on modified reachability trees (MRT), and then proposes the rectified calculation of the next-state function and some corresponding definitions, which guarantee MRT´s usefulness and correctness in analyzing reachability and deadlock of one-place unbounded Petri nets. Finally, a necessary and sufficient condition of MRT´s reachability and the theoretical proof are presented. Examples are given to illustrate the method.