具有一个零检验的向量加法系统的模型检验
Model Checking Vector Addition Systems with one zero-test
摘要：
我们设计了Karp-Miller算法的一个变体，以向前的方式计算覆盖的有限表示（即，可达集的向下闭包）的一个零测试的向量加法系统。该算法产生的决策程序，这些系统的几个问题，开放到现在，如地方有界性或LTL模型检查。处理零测试的证明技术基于两个新的覆盖概念：精炼覆盖和过滤覆盖。精化覆盖是可达集和经典覆盖的混合。它继承了可达集的性质：两个加细覆盖的相等性是不可判定的，即使对于通常的向量加法系统（没有零检验），但向量加法系统的加细覆盖是递归集。覆盖的第二个概念，称为过滤覆盖，是我们算法的核心工具。它继承了经典覆盖的性质，特别是，可以有效地计算这个集合的有限表示，即使对于具有一个零测试的向量加法系统。
英文摘要：
We design a variation of the Karp-Miller algorithm to compute, in a forward manner, a finite representation of the cover (i.e., the downward closure of the reachability set) of a vector addition system with one zero-test. This algorithm yields decision procedures for several problems for these systems, open until now, such as place-boundedness or LTL model-checking. The proof techniques to handle the zero-test are based on two new notions of cover: the refined and the filtered cover. The refined cover is a hybrid between the reachability set and the classical cover. It inherits properties of the reachability set: equality of two refined covers is undecidable, even for usual Vector Addition Systems (with no zero-test), but the refined cover of a Vector Addition System is a recursive set. The second notion of cover, called the filtered cover, is the central tool of our algorithms. It inherits properties of the classical cover, and in particular, one can effectively compute a finite representation of this set, even for Vector Addition Systems with one zero-test.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
