Analysis for one-place unbounded Petri nets based on modified reachability trees
Analysis for one-place unbounded Petri nets based on modified reachability trees
复制标题
DOI：
10.1109/icnsc.2012.6204900
复制
发表时间：
2012-04
期刊：
影响因子：
--
通讯作者：
Yu Wang;Z. Ding
中科院分区：
文献类型：
--
作者：
Yu Wang;Z. Ding
可达性决策的分析方法是Petri网理论的基础；然而，以往的相关研究工作并不能保证分析结论的正确性。本文首先揭示了基于改进可达树（MRT）的Petri网死锁分析中得出错误结论的根本原因，然后提出了下一状态函数的修正计算方法和相应的定义，保证了MRT在分析一元无界Petri网的可达性和死锁时的有效性和正确性。最后，给出了MRT可达性的充分必要条件和理论证明。给出了实例来说明该方法。
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.