自动多面体抽象证明
摘要：自动化地证明Petri网的多面体抽象的程序的提出。多面体抽象是一种基于线性整数约束的新型状态空间等价。我们的方法依赖于编码成一组SMT公式，其满足性意味着等价性成立。在这种情况下的困难在于我们需要处理无穷状态系统。为了完整性，我们利用与具有Presburger可定义可达性集合的Petri网类的连接。我们已经实现了我们的程序，并且我们以几个例子说明了其用途。
作者：Nicolas Amat (LAAS, LAAS-VERTICS), Silvano Dal Zilio (LAAS-VERTICS, LAAS), Didier Le Botlan (LAAS-VERTICS, LAAS)
论文ID：2306.01466
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-05