论文标题
用最小值基础可及性图验证有限的培养皿网中的非封锁性
Verification of Nonblockingness in Bounded Petri Nets With Minimax Basis Reachability Graphs
论文作者
论文摘要
本文提出了一种半结构的方法，以验证培养皿网的非堵塞性。我们构建了一个称为最小值基准可及性图（Minimax-BRG）的结构：它提供了对网络的可及性集的抽象描述，同时保留了测试网络是否阻塞所需的所有信息。我们证明，当且仅当它的最小值brg毫无障碍时，无界的无僵硬的培养皿是非封锁的，可以通过求解一组整数约束，然后检查minimax-brg来验证。对于不含僵局的培养皿网，需要确定一组僵局标记。这可以通过基于Minimax-BRG中标记启用的最大隐式触发序列的计算来完成。我们开发的方法不需要构建可及性图，并且具有广泛的适用性。
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.
