An Efficient Liveness Analysis Method for Petri Nets via Maximally Good-Step Graphs
提出一种基于最大好步图（MGs）的Petri网活性分析方法，通过缩减可达图有效缓解状态空间爆炸问题，实验表明在大规模自动化制造系统中能显著降低状态空间和时间消耗。
Liveness is among the most significant properties when Petri net (PN) models of automated systems are analyzed, which ensures systems’ deadlock-freeness. Traditionally, the liveness analysis methods based on reachability graphs (RGs) of PNs often suffer from state-space explosion problems. In this article, we propose a novel liveness-analysis method for PN based on maximally good-step graphs (MGs), namely, the reduced form of RGs, which can effectively alleviate such problems in liveness analysis. First, we introduce the concept of sound steps and establish an algorithm for assessing the soundness of an enabled step at the current marking from a practice point of view. Second, we propose a definition of maximal sound steps and construct an algorithm for calculating a maximal-sound-step set at each marking whose computational complexity grows polynomial with the number of places and transitions. Then, we introduce a definition for good steps and an algorithm for generating maximally good step graphs of PN; and discuss its computational complexity with respect to the net size and initial marking. Next, we for the first time answer how to evaluate the liveness of PN by using MGs. Experiments in diverse large-scale automated manufacturing systems demonstrate that the proposed method significantly reduces state space and time consumption in the liveness analysis of network systems.