Document Open Access Logo

Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One

Authors Diego Figueira, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki, Grégoire Sutre

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2017.119.pdf
  • Filesize: 0.76 MB
  • 14 pages

Document Identifiers

Author Details

Diego Figueira
Ranko Lazic
Jérôme Leroux
Filip Mazowiecki
Grégoire Sutre

Cite As Get BibTex

Diego Figueira, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki, and Grégoire Sutre. Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 119:1-119:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.ICALP.2017.119

Abstract

Whether the reachability problem for branching vector addition systems, or equivalently the provability problem for multiplicative exponential linear logic, is decidable has been a long-standing open question. The one-dimensional case is a generalisation of the extensively studied one-counter nets, and it was recently established polynomial-time complete provided counter updates are given in unary.  Our main contribution is to determine the complexity when the encoding is binary: polynomial-space complete.

Subject Classification

Keywords
  • branching vector addition systems
  • reachability problem

Metrics

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

References

  1. Sergio Abriola, Diego Figueira, and Santiago Figueira. Logics of repeating values on data trees and branching counter systems. In FoSSACS, volume 10203 of LNCS. Springer, 2017, to appear. Google Scholar
  2. Katalin Bimbó. The decidability of the intensional fragment of classical linear logic. Theor. Comput. Sci., 597:1-17, 2015. URL: http://dx.doi.org/10.1016/j.tcs.2015.06.019.
  3. 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. URL: http://dx.doi.org/10.1109/LICS.2015.14.
  4. Mikołaj Bojańczyk. Automata column. SIGLOG News, 1(2):3-12, 2014. URL: http://dx.doi.org/10.1145/2677161.2677163.
  5. Ahmed Bouajjani and Michael Emmi. Analysis of recursively parallel programs. ACM Trans. Program. Lang. Syst., 35(3):10:1-10:49, 2013. URL: http://dx.doi.org/10.1145/2518188.
  6. Lorenzo Clemente, Sławomir Lasota, Ranko Lazić, and Filip Mazowiecki. Timed pushdown automata and branching vector addition systems. Submitted, 2017. Google Scholar
  7. Conrad Cotton-Barratt, Andrzej S. Murawski, and C.-H. Luke Ong. ML and extended BVASS. In ESOP, 2017. To appear. Google Scholar
  8. Philippe de Groote, Bruno Guillaume, and Sylvain Salvati. Vector addition tree automata. In LICS, pages 64-73. IEEE Computer Society, 2004. URL: http://dx.doi.org/10.1109/LICS.2004.1319601.
  9. 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. URL: http://dx.doi.org/10.1145/2933575.2933577.
  10. Stefan Göller, Christoph Haase, Ranko Lazić, and Patrick Totzke. A polynomial-time algorithm for reachability in branching VASS in dimension one. In ICALP, volume 55 of LIPIcs, pages 105:1-105:13. Schloss Dagstuhl, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.105.
  11. 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. URL: http://dx.doi.org/10.1007/978-3-642-04081-8_25.
  12. John E. Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci., 8:135-159, 1979. URL: http://dx.doi.org/10.1016/0304-3975(79)90041-0.
  13. Florent Jacquemard, Luc Segoufin, and Jerémie Dimino. FO2(less, +1, asciitilde) on data trees, data tree automata and branching vector addition systems. Log. Meth. Comput. Sci., 12(2), 2016. URL: http://dx.doi.org/10.2168/LMCS-12(2:3)2016.
  14. S. Rao Kosaraju. Decidability of reachability in vector addition systems (preliminary version). In STOC, pages 267-281. ACM, 1982. URL: http://dx.doi.org/10.1145/800070.802201.
  15. Pascal Lafourcade, Denis Lugiez, and Ralf Treinen. Intruder deduction for AC-like equational theories with homomorphisms. Research Report LSV-04-16, ENS de Cachan, 2004. Google Scholar
  16. Ranko Lazić and Sylvain Schmitz. Nonelementary complexities for branching VASS, MELL, and extensions. ACM Trans. Comput. Log., 16(3):20:1-20:30, 2015. URL: http://dx.doi.org/10.1145/2733375.
  17. Jérôme Leroux and Sylvain Schmitz. Ideal decompositions for vector addition systems (invited talk). In STACS, volume 47 of LIPIcs, pages 1:1-1:13. Schloss Dagstuhl, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2016.1.
  18. 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. URL: http://dx.doi.org/10.1007/978-3-540-28644-8_26.
  19. Patrick Lincoln, John C. Mitchell, Andre Scedrov, and Natarajan Shankar. Decision problems for propositional linear logic. Ann. Pure Appl. Logic, 56(1-3):239-311, 1992. URL: http://dx.doi.org/10.1016/0168-0072(92)90075-B.
  20. Owen Rambow. Multiset-valued linear index grammars: Imposing dominance constraints on derivations. In ACL, pages 263-270. Morgan Kaufmann Publishers / ACL, 1994. URL: http://aclweb.org/anthology/P/P94/P94-1036.pdf.
  21. Wolfgang Reisig. Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-33278-4.
  22. Sylvain Schmitz. On the computational complexity of dominance links in grammatical formalisms. In ACL, pages 514-524. The Association for Computer Linguistics, 2010. URL: http://www.aclweb.org/anthology/P10-1053.
  23. Sylvain Schmitz. The complexity of reachability in vector addition systems. SIGLOG News, 3(1):4-21, 2016. URL: http://dx.doi.org/10.1145/2893582.2893585.
  24. Leslie G. Valiant and Mike Paterson. Deterministic one-counter automata. J. Comput. Syst. Sci., 10(3):340-350, 1975. URL: http://dx.doi.org/10.1016/S0022-0000(75)80005-5.
  25. Kumar Neeraj Verma and Jean Goubault-Larrecq. Karp-Miller trees for a branching extension of VASS. Discr. Math. & Theor. Comput. Sci., 7(1):217-230, 2005. URL: http://www.dmtcs.org/volumes/abstracts/dm070113.abs.html.
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 About DROPS Imprint Privacy Contact