Proof by model: a new knowledge-based reachability analysis methodology for Petri net
Daniel Yuh Chao, Yen‐Ping Chi, Tsung-Hsien Yu, Li-Chih Yu, Mike Y. J. Lee · IMA Journal of Mathematical Control and Information · 2016
To solve the state explosion problem in the reachability analysis of Petri nets, Chao recently broke the NP(nondeterministic polynomial time)-complete barrier by developing the first closed-form solution of the number of Control Related States for the kth-order system. In this paper, we propose a new proof methodology known as proof by model, which is based on the validated information of the reverse net, to simplify and accelerate the construction of the closed-form solution for Petri nets. Here, we apply this methodology to the proof procedure of Top-Right systems with one non-sharing resource placed in the top position of the right-side process. The core theoretical and data basis are that any forbidden (resp. live) state in a Petri net is non-reachable (resp. live) in its reverse net; and the validated information of the Bottom-Right system, the reverse net of Top-Right.