Document Open Access Logo

Reachability in Two-Dimensional Vector Addition Systems with States: One Test Is for Free

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

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.37.pdf
  • Filesize: 0.54 MB
  • 17 pages

Document Identifiers

Author Details

Jérôme Leroux
  • LaBRI, Université Bordeaux, CNRS, Bordeaux-INP, Talence, France
Grégoire Sutre
  • LaBRI, Université 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

Jérôme Leroux and Grégoire Sutre. Reachability in Two-Dimensional Vector Addition Systems with States: One Test Is for Free. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CONCUR.2020.37

Abstract

Vector addition system with states is an ubiquitous model of computation with extensive applications in computer science. The reachability problem for vector addition systems is central since many other problems reduce to that question. The problem is decidable and it was recently proved that the dimension of the vector addition system is an important parameter of the complexity. In fixed dimensions larger than two, the complexity is not known (with huge complexity gaps). In dimension two, the reachability problem was shown to be PSPACE-complete by Blondin et al. in 2015. We consider an extension of this model, called 2-TVASS, where the first counter can be tested for zero. This model naturally extends the classical model of one counter automata (OCA). We show that reachability is still solvable in polynomial space for 2-TVASS. As in the work Blondin et al., our approach relies on the existence of small reachability certificates obtained by concatenating polynomially many cycles.

Subject Classification

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

Metrics

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

Related Versions

References

  1. 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, 2015. Google Scholar
  2. Rémi Bonnet. The reachability problem for vector addition system with one zero-test. In MFCS, volume 6907 of LNCS, pages 145-157. Springer, 2011. Google Scholar
  3. I. Borosh and L. B. Treybig. A sharp bound on positive solutions of linear diophantine equations. SIAM J. Matrix Analysis Applications, 13(2):454-458, 1992. Google Scholar
  4. Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for Petri nets is not elementary. In STOC, pages 24-33. ACM, 2019. Google Scholar
  5. Wojciech Czerwiński, Sławomir Lasota, Christof Löding, and Radoslaw Piórkowski. New pumping technique for 2-dimensional VASS. In MFCS, volume 138 of LIPIcs, pages 62:1-62:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  6. Catherine Dufourd, Alain Finkel, and Philippe Schnoebelen. Reset nets between decidability and undecidability. In ICALP, volume 1443 of LNCS, pages 103-115. Springer, 1998. Google Scholar
  7. Matthias Englert, Ranko Lazić, 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. John Fearnley and Marcin Jurdzinski. Reachability in two-clock timed automata is PSPACE-complete. Inform. Comput., 243:26-36, 2015. Google Scholar
  9. Alain Finkel, Jérôme Leroux, and Grégoire Sutre. Reachability for two-counter machines with one test and one reset. In FSTTCS, volume 122 of LIPIcs, pages 31:1-31:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  10. Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in succinct and parametric one-counter automata. In CONCUR, volume 5710 of LNCS, pages 369-383. Springer, 2009. Google Scholar
  11. John Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci., 8(2):135-159, 1979. Google Scholar
  12. S. Rao Kosaraju. Decidability of reachability in vector addition systems (preliminary version). In STOC, pages 267-281. ACM, 1982. Google Scholar
  13. Jean-Luc Lambert. A structure to decide reachability in Petri nets. Theor. Comput. Sci., 99(1):79-104, 1992. Google Scholar
  14. Michel Latteux. Langages à un compteur. J. Comput. Syst. Sci., 26(1):14-33, 1983. Google Scholar
  15. Jérôme Leroux. The general vector addition system reachability problem by Presburger inductive invariants. Logical Methods in Computer Science, 6(3), 2010. Google Scholar
  16. Jérôme Leroux. Vector addition system reachability problem: a short self-contained proof. In POPL, pages 307-316. ACM, 2011. Google Scholar
  17. Jérôme Leroux. Vector addition systems reachability problem (A simpler solution). In Turing-100, volume 10 of EPiC Series in Computing, pages 214-228. EasyChair, 2012. Google Scholar
  18. Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In LICS, pages 1-13. IEEE, 2019. Google Scholar
  19. Jérôme Leroux and Grégoire Sutre. On flatness for 2-dimensional vector addition systems with states. In CONCUR, volume 3170 of LNCS, pages 402-416. Springer, 2004. Google Scholar
  20. Jérôme Leroux and Grégoire Sutre. Flat counter automata almost everywhere! In ATVA, volume 3707 of LNCS, pages 489-503. Springer, 2005. Google Scholar
  21. Jérôme Leroux and Grégoire Sutre. Reachability in two-dimensional vector addition systems with states: One test is for free, 2020. URL: http://arxiv.org/abs/2007.09096.
  22. Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. On the coverability problem for pushdown vector addition systems in one dimension. In ICALP (2), volume 9135 of LNCS, pages 324-336. Springer, 2015. Google Scholar
  23. Richard J. Lipton. The reachability problem requires exponential space. Technical Report 62, Yale University, 1976. URL: http://cpsc.yale.edu/sites/default/files/files/tr63.pdf.
  24. Ernst W. Mayr. An algorithm for the general Petri net reachability problem. In STOC, pages 238-246. ACM, 1981. Google Scholar
  25. Ernst W. Mayr. An algorithm for the general Petri net reachability problem. SIAM J. Comput., 13(3):441-460, 1984. Google Scholar
  26. Marvin L. Minsky. Computation: finite and infinite machines. Prentice-Hall, Inc., 1967. Google Scholar
  27. Loic Pottier. Minimal solutions of linear diophantine systems: Bounds and algorithms. In RTA, volume 488 of LNCS, pages 162-173. Springer, 1991. Google Scholar
  28. Klaus Reinhardt. Reachability in Petri nets with inhibitor arcs. Electr. Notes Theor. Comput. Sci., 223:239-264, 2008. Google Scholar
  29. Philippe Schnoebelen. Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In MFCS, volume 6281 of LNCS, pages 616-628. Springer, 2010. Google Scholar
  30. Leslie G. Valiant and Mike Paterson. Deterministic one-counter automata. J. Comput. Syst. Sci., 10(3):340-350, 1975. 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