首页    期刊浏览 2024年11月09日 星期六
登录注册

文章基本信息

  • 标题: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
国家哲学社会科学文献中心版权所有