期刊
IEEE TRANSACTIONS ON SYSTEMS MAN CYBERNETICS-SYSTEMS
卷 50, 期 6, 页码 2007-2016出版社
IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
DOI: 10.1109/TSMC.2018.2791527
关键词
Light rail systems; System recovery; Petri nets; Algorithm design and analysis; Cybernetics; Indexes; Tools; Boundedness; deadlock; discrete event systems; liveness; Petri nets (PNs); reachability tree; reversibility; unbounded Petri nets
资金
- National Natural Science Foundation of China [61773115, 61374069, 61374148]
- Natural Science Foundation of Jiangsu Province [BK20161427]
- Fundamental Research Funds for the Central Universities [2242017K41054]
At present, no efficient method is proposed for the liveness analysis of general unbounded Petri nets (UPNs) except some of their subclasses. Our previous work presents a non-Karp-Miller finite reachability tree, i.e., lean reachability tree (LRT) to represent their markings. It faithfully expresses and folds the reachability set of an unbounded net. It can totally avoid the efforts made by the existing modified Karp-Miller trees on the expression of potentially unbounded nodes and elimination of all fake markings. By exploiting it, this paper presents a method for comprehensively analyzing the properties of general UPNs. Particularly, we reveal the repeatability of deadlock with the unfolding of some unbounded leaves in LRT and present a sufficient and necessary condition of deadlock existence. Then, LRT and some partial trees generated from it, instead of entire reachability graphs, are utilized to analyze the liveness and reversibility of general UPNs rather than some special ones. The related theoretical results are proven. A unified algorithm based on LRT for analysis of boundedness, liveness, deadlock, and reversibility of general UPNs is developed for the first time. The results of a case study show that the presented method is effective for general UPNs.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据