基于极小极大基可达图的有界Petri网非阻塞性验证
Verification of Nonblockingness in Bounded Petri Nets With Minimax Basis Reachability Graphs
AI总结：
针对有界Petri网非阻塞性验证问题，提出基于极小极大基可达图的半结构化方法，无需构建完整可达图即可完成验证，适用范围广。
摘要：
本文提出一种半结构化方法来验证Petri网的非阻塞性。我们构建了一种名为极小极大基可达图（minimax basis reachability graph，minimax-BRG）的结构：它对Petri网的可达集提供抽象描述，同时保留检验网是否为阻塞所需的全部信息。我们证明，一个有界且无死锁的Petri网是非阻塞的，当且仅当其极小极大基可达图是无阻碍的，这一点可通过求解一组整数约束并检查极小极大基可达图来验证。对于存在死锁的Petri网，需要确定死锁标识集合，这可通过一种基于计算极小极大基可达图中标识所激活的最大隐式引发序列的方法实现。我们提出的方法无需构建可达图，适用范围广。
英文摘要：
This paper proposes a semi-structural approach to verify the nonblockingness of a Petri net. We construct a structure, called minimax basis reachability graph (minimax-BRG): it provides an abstract description of the reachability set of a net while preserving all information needed to test if the net is blocking. We prove that a bounded deadlock-free Petri net is nonblocking if and only if its minimax-BRG is unobstructed, which can be verified by solving a set of integer constraints and then examining the minimax-BRG. For Petri nets that are not deadlock-free, one needs to determine the set of deadlock markings. This can be done with an approach based on the computation of maximal implicit firing sequences enabled by the markings in the minimax-BRG. The approach we developed does not require the construction of the reachability graph and has wide applicability.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
