A Reachability-Decidable Petri Net Modeling Method for Discrete Event Systems

Petri nets (PNs) are graphical and mathematical tools used to model a variety of discrete event systems and analyze their properties. Reachability is their fundamental property that is undecidable for PNs in general and has exponential complexity with respect to net size. One of the possible computation techniques of reachable states (markings) is based on the determination of legal firing sequences (LFSs) that correspond to a non-negative integer solutions (NISs) of a state equation. Our previous work has proposed an algorithm to decide the existence of LFSs corresponding to an NIS in polynomial time. However, it is impossible to check all NISs to decide a marking's reachability in the case of an infinite number of NISs in a state equation. Hence, this work studies the relationship between the structure of a PN and the number of NISs of its state equation. Furthermore, an innovative method is proposed to modify its structure such that its state equation has no more than one NIS. The relationship between the properties of a PN and its modified one is studied in this article. We conclude that we can modify its structure while maintaining the function of the modeled system such that the reachability of the model can be decided in polynomial time. This can be viewed as a breakthrough result in the area of PN theory and applications. The correctness and time efficiency of the algorithm are verified by case studies and experiments. This work is important in putting PNs into the industrial use.