Verification of Nonblockingness in Bounded Petri Nets With Min-Max Basis Reachability Graphs
Chao Gu, Ziyue Ma, Zhiwu Li, Alessandro Giua · IEEE Transactions on Systems Man and Cybernetics Systems · 2022
This article proposes a semi-structural approach to verify thenonblockingnessof a Petri net. We construct a structure, called minimal-maximal basis reachability graph (min-max-BRG): it provides an abstract description of the reachability set of a net while preserving all information needed to test if the net isblocking. We prove that a bounded deadlock-free Petri net isnonblockingif and only if its min-max-BRG isunobstructed, which can be verified by solving a set of integer constraints and then examining the min-max-BRG. For Petri nets that are not deadlock-free, one needs to determine the set of dead markings. This can be done with an approach based on the computation ofmaximal implicit firing sequencesenabled by the markings in the min-max-BRG. The approach we developed does not require the construction of the reachability graph and has wide applicability.