Verification of Nonblockingness in Bounded Petri Nets With Min-Max Basis Reachability Graphs
提出一种半结构化方法，通过构造最小-最大基可达图来验证有界Petri网的非阻塞性，无需构建完整可达图，适用于死锁自由和非死锁自由网。
This article proposes a semi-structural approach to verify the <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">nonblockingness</i> of 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 is <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">blocking</i> . We prove that a bounded deadlock-free Petri net is <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">nonblocking</i> if and only if its min-max-BRG is <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">unobstructed</i> , 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 of <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">maximal implicit firing sequences</i> enabled 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.