We define a new method for taking advantage of net reductions in combination with a SMT-based model checker. Our approach consists in transforming a reachability problem about some Petri net, into the verification of an updated reachability property on a reduced version of this net. This method relies on a new state space abstraction based on systems of constraints, called polyhedral abstraction. We prove the correctness of this method using a new notion of equivalence between nets. We provide a complete framework to define and check the correctness of equivalence judgements; prove that this relation is a congruence; and give examples of basic equivalence relations that derive from structural reductions. Our approach has been implemented in a tool, named SMPT, that provides two main procedures: Bounded Model Checking (BMC) and Property Directed Reachability (PDR). Each procedure has been adapted in order to use reductions and to work with arbitrary Petri nets. We tested SMPT on a large collection of queries used in the Model Checking Contest. Our experimental results show that our approach works well, even when we only have a moderate amount of reductions.
翻译:我们与基于SMT的模型核对器共同界定了利用净减量的新方法。我们的方法包括将某些Petri网的可达性问题转化为对这个网的简化版本上最新可达性财产的核查。这个方法依靠基于限制系统的新状态空间抽象,称为多元抽象抽象。我们用一种新的网对等概念来证明这种方法的正确性。我们提供了一个完整的框架来界定和检查等同性判断的正确性;证明这种关系是一致的;并举例说明结构性减量产生的基本等同关系。我们的方法已在一个称为SMPT的工具中实施,该工具提供了两个主要程序:完善的示范检查(BMC)和财产直接可达性(PDR),每个程序都经过调整,以便使用削减和与专制的Petri网合作。我们测试了SMPT在模型测试比赛中使用的大量查询中的测试结果。我们的实验结果表明,我们的方法效果良好,即使我们只有适度的减量。