基于SMT的模型检查中用于Petri网的多面体抽象
摘要：利用SMT基于模型检查的网络减少方法的新方法定义。我们的方法包括将有关某个Petri网的可达性问题转化为对该网的缩减版本上的更新可达性属性的验证。该方法依赖一种基于约束系统的新状态空间抽象，称为多面体抽象。我们使用一种新的等价性概念证明了该方法的正确性。我们提供了一个完整的框架来定义和检查等价关系的正确性；证明了该关系是一个合同关系；并且给出了由结构减少导出的基本等价关系的示例。我们的方法已经在一个名为SMPT的工具中实现，该工具提供了两个主要过程：有界模型检查（BMC）和属性导向的可达性（PDR）。为了使用减少和处理任意Petri网，每个过程都经过了适应性调整。我们在模型检查竞赛中使用的大量查询集上测试了SMPT。我们的实验结果表明，即使我们只有适度的减少量，我们的方法也能很好地工作。
作者：Nicolas Amat (LAAS-VERTICS), Bernard Berthomieu (LAAS-VERTICS), Silvano Dal Zilio (LAAS-VERTICS)
论文ID：2104.09850
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22