文章基本信息

标题：Reachability for Two-Counter Machines with One Test and One Reset
本地全文：下载
作者：Alain Finkel ; J{\'e}r{\^o}me Leroux ; Gr{\'e}goire Sutre 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2018
卷号：122
页码：1-14
DOI：10.4230/LIPIcs.FSTTCS.2018.31
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We prove that the reachability relation of two-counter machines with one zero-test and one reset is Presburger-definable and effectively computable. Our proof is based on the introduction of two classes of Presburger-definable relations effectively stable by transitive closure. This approach generalizes and simplifies the existing different proofs and it solves an open problem introduced by Finkel and Sutre in 2000.
关键词：Counter machine; Vector addition system; Reachability problem; Formal verification; Presburger arithmetic; Infinite-state system