An Efficient Liveness Analysis Method for Petri Nets via Maximally Good-Step Graphs

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.