更好的拟序转移系统
Better Quasi-Ordered Transition Systems
摘要：
许多现有的算法的模型检验的无限状态系统的约束，这是用来表示（潜在的无限）的状态集。一个通用的强大的技术，可以用来证明终止这些算法是良好的准序。已经提出了几种方法来推导新的良好的准序约束系统。然而，这些约束系统中的许多遭受“约束爆炸问题”，因为生成的约束的数量随着问题的大小呈指数增长。在本文中，我们证明了一个完善的理论，良好的准序，称为理论的更好的准序，是更合适的符号模型检验，因为它允许发明的约束系统，这是良好的准序和紧凑的。作为一个主要的应用程序，我们引入存在区，一个约束系统的无限多的时钟系统的验证，并使用我们的方法来证明存在区是更好的准有序。我们展示了如何使用存在区的时间Petri网的验证，并提出了一些实验结果。此外，我们应用我们的方法来获得新的约束系统的验证广播协议，有损信道系统，和积分关系自动机。新的约束系统是指数更简洁比现有的，他们的良好的准序不能显示由以前的方法在文献中。
英文摘要：
Many existing algorithms for model checking of infinite-state systems operate on constraints which are used to represent (potentially infinite) sets of states. A general powerful technique which can be employed for proving termination of these algorithms is that of well quasi-orderings. Several methodologies have been proposed for derivation of new well quasi-ordered constraint systems. However, many of these constraint systems suffer from a "constraint explosion problem", as the number of the generated constraints grows exponentially with the size of the problem. In this paper, we demonstrate that a refinement of the theory of well quasi-orderings, called the theory of better quasi-orderings, is more appropriate for symbolic model checking, since it allows inventing constraint systems which are both well quasi-ordered and compact. As a main application, we introduce existential zones, a constraint system for verification of systems with unboundedly many clocks and use our methodology to prove that existential zones are better quasi-ordered. We show how to use existential zones in verification of timed Petri nets and present some experimental results. Also, we apply our methodology to derive new constraint systems for verification of broadcast protocols, lossy channel systems, and integral relational automata. The new constraint systems are exponentially more succinct than existing ones, and their well quasi-ordering cannot be shown by previous methods in the literature.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
