更好的准序过渡系统
摘要：无穷状态系统模型检测算法通常操作用于表示（可能是无限的）状态集合的约束。一个常用的技术是使用良好拟序的方法来证明这些算法的终止性。有几种方法被提出来生成新的良好拟序约束系统。然而，许多这些约束系统都存在“约束爆炸问题”，因为生成的约束数量随着问题规模的增大呈指数级增长。本文证明了一个被称为更好拟序的良好拟序理论改进版，更适合符号模型检测，因为它允许发明既良好拟序又紧凑的约束系统。作为一个主要应用，我们引入了存在性区域，一种用于验证具有无限数量时钟的系统的约束系统，并使用我们的方法证明了存在性区域是更好拟序的。我们展示了如何在时态Petri网的验证中使用存在性区域，并呈现了一些实验结果。此外，我们将我们的方法应用于导出用于验证广播协议、有丢失信道系统和积分关系自动机的新约束系统。这些新的约束系统比现有系统更紧凑，并且无法通过以前的方法在文献中显示其良好拟序。
作者：Parosh Aziz Abdulla and Aletta Nylen
论文ID：cs/0409052
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23