A Structure-Modification-Based Petri Net Modeling and Reachability Analysis Method for Automated Manufacturing Systems

Due to their graphical representation and capability for property analysis, Petri nets (PNs) have been widely used in developing automated manufacturing systems (AMS). When designing them, it is important to perform their state reachability analysis and verify their functionality. The most common approach is to traverse a reachability tree of their PN models. However, it has the problem of state space explosion. A way to determine a state’s reachability is to find a firing sequence (FS) that corresponds to nonnegative integer solutions (NISs) of a state equation. Our prior work has given an algorithm to decide the existence of FS corresponding to an NIS in polynomial time. Yet it is impossible to decide the reachability of a marking given an infinite number of NISs of a state equation. This work studies the relationship between the PN model and NIS count of any state equation. An innovative method is proposed to modify a PN structure such that, for any given initial state and destination one, its state equation has no more than one NIS. Given an initial PN model of an AMS, by analyzing the relationship between initial PN properties and the modified one’s, we have that the proposed method can maintain the functionality of the modeled AMS. As a result, by using the modified PN as the AMS’s final model, the reachability of any marking can be determined in polynomial time, which can be viewed as a breakthrough result in the field of PN analysis. The proposed method is illustrated via case studies.