Document Open Access Logo

Reachability for Two-Counter Machines with One Test and One Reset

Authors Alain Finkel, Jérôme Leroux, Grégoire Sutre

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2018.31.pdf
  • Filesize: 0.52 MB
  • 14 pages

Document Identifiers

Author Details

Alain Finkel
  • LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay, France
Jérôme Leroux
  • LaBRI, Univ. Bordeaux, CNRS, Bordeaux-INP, Talence, France
Grégoire Sutre
  • LaBRI, Univ. Bordeaux, CNRS, Bordeaux-INP, Talence, France

Funding

This work was supported by the grant ANR-17-CE40-0028 of the French National Research Agency ANR (project BRAVAS).

Cite AsGet BibTex

Alain Finkel, Jérôme Leroux, and Grégoire Sutre. Reachability for Two-Counter Machines with One Test and One Reset. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 31:1-31:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSTTCS.2018.31

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Counter machine
  • Vector addition system
  • Reachability problem
  • Formal verification
  • Presburger arithmetic
  • Infinite-state system

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. S. Akshay, Supratik Chakraborty, Ankush Das, Vishal Jagannath, and Sai Sandeep. On Petri Nets with Hierarchical Special Arcs. In CONCUR, volume 85 of LIPIcs, pages 40:1-40:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. Google Scholar
  2. Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase, and Pierre McKenzie. Reachability in Two-Dimensional Vector Addition Systems with States Is PSPACE-Complete. In LICS, pages 32-43. IEEE Computer Society, 2015. Google Scholar
  3. Rémi Bonnet. The reachability problem for Vector Addition Systems with one zero-test. In Filip Murlak and Piotr Sankowski, editors, Proceedings of the 36th International Symposium on Mathematical Foundations of Computer Science (MFCS'11), volume 6907 of Lecture Notes in Computer Science, pages 145-157, Warsaw, Poland, August 2011. Springer. Google Scholar
  4. Rémi Bonnet, Alain Finkel, Jérôme Leroux, and Marc Zeitoun. Place-Boundedness for Vector Addition Systems with one zero-test. In Kamal Lodaya and Meena Mahajan, editors, Proceedings of the 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'10), volume 8 of Leibniz International Proceedings in Informatics, pages 192-203, Chennai, India, December 2010. Leibniz-Zentrum für Informatik. Google Scholar
  5. Catherine Dufourd, Alain Finkel, and Philippe Schnoebelen. Reset Nets Between Decidability and Undecidability. In ICALP, volume 1443 of Lecture Notes in Computer Science, pages 103-115. Springer, 1998. Google Scholar
  6. Catherine Dufourd, Petr Jancar, and Philippe Schnoebelen. Boundedness of Reset P/T Nets. In ICALP, volume 1644 of Lecture Notes in Computer Science, pages 301-310. Springer, 1999. Google Scholar
  7. Matthias Englert, Ranko Lazic, and Patrick Totzke. Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete. In LICS, pages 477-484. ACM, 2016. Google Scholar
  8. Alain Finkel and Arnaud Sangnier. Mixing coverability and reachability to analyze VASS with one zero-test. In David Peleg and Anca Muscholl, editors, Proceedings of the 36th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'10), volume 5901 of Lecture Notes in Computer Science, pages 394-406, Špindlerův Mlýn, Czech Republic, January 2010. Springer. Google Scholar
  9. Alain Finkel and Philippe Schnoebelen. Well-Structured Transition Systems Everywhere! Theoretical Computer Science, 256(1-2):63-92, April 2001. Google Scholar
  10. Alain Finkel and Grégoire Sutre. An Algorithm Constructing the Semilinear Post^* for 2-Dim Reset/Transfer VASS. In MFCS, volume 1893 of Lecture Notes in Computer Science, pages 353-362. Springer, 2000. Google Scholar
  11. Alain Finkel and Grégoire Sutre. Decidability of Reachability Problems for Classes of Two Counters Automata. In STACS, volume 1770 of Lecture Notes in Computer Science, pages 346-357. Springer, 2000. Google Scholar
  12. Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in Succinct and Parametric One-Counter Automata. In CONCUR, volume 5710 of Lecture Notes in Computer Science, pages 369-383. Springer, 2009. Google Scholar
  13. John Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science, 8(2):135-159, 1979. Google Scholar
  14. Ranko Lazic. The reachability problem for vector addition systems with a stack is not elementary. CoRR, abs/1310.1767, 2013. Google Scholar
  15. Ranko Lazic and Patrick Totzke. What Makes Petri Nets Harder to Verify: Stack or Data? In Concurrency, Security, and Puzzles, volume 10160 of Lecture Notes in Computer Science, pages 144-161. Springer, 2017. Google Scholar
  16. Jérôme Leroux, M. Praveen, and Grégoire Sutre. Hyper-Ackermannian bounds for pushdown vector addition systems. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, page 63. ACM, 2014. Google Scholar
  17. Jérôme Leroux and Grégoire Sutre. On Flatness for 2-Dimensional Vector Addition Systems with States. In CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings, volume 3170 of Lecture Notes in Computer Science, pages 402-416. Springer, 2004. Google Scholar
  18. M. Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Comptes Rendus du premier congrès de mathématiciens des Pays Slaves, Warszawa, pages 92-101, 1929. Google Scholar
  19. Klaus Reinhardt. Reachability in Petri Nets with Inhibitor Arcs. Electr. Notes Theor. Comput. Sci., 223:239-264, 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact