Verification of Nonblockingness in Bounded Petri Nets with a Semi-Structural Approach

In this paper, we propose a basis marking method- based semi-structural approach to verify nonblockingness of a Petri net. By solving a set of integer linear programming problems, the unobstructiveness of a basis reachability graph, which is a necessary condition for nonblockingness, is determined. We propose an algorithm to expand the basis reachability graph and show that a bounded Petri net is nonblocking if and only if its expanded basis reachability graph is unobstructed. The main advantages of this method are that it does not require to enumerate all the reachable markings and has wide applicability.