Document Open Access Logo

Reachability for Bounded Branching VASS

Authors Filip Mazowiecki, Michał Pilipczuk

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.28.pdf
  • Filesize: 0.69 MB
  • 13 pages

Document Identifiers

Author Details

Filip Mazowiecki
  • LaBRI, Université de Bordeaux, France
Michał Pilipczuk
  • University of Warsaw, Poland

Funding

  • Mazowiecki, Filip: This study has been carried out with financial support from the French State, managed by the French National Research Agency (ANR) in the frame of the "Investments for the future" Programme IdEx Bordeaux (ANR-10-IDEX-03-02).
  • Pilipczuk, Michał: This work is a part of project TOTAL that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme, grant agreement No. 677651.

Acknowledgements

The authors would like to thank Marthe Bonamy for feeding them during the work on this project. No beavers were harmed in the making of this paper.

Cite AsGet BibTex

Filip Mazowiecki and Michał Pilipczuk. Reachability for Bounded Branching VASS. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 28:1-28:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CONCUR.2019.28

Abstract

In this paper we consider the reachability problem for bounded branching VASS. Bounded VASS are a variant of the classic VASS model where all values in all configurations are upper bounded by a fixed natural number, encoded in binary in the input. This model gained a lot of attention in 2012 when Haase et al. showed its connections with timed automata. Later in 2013 Fearnley and Jurdziński proved that the reachability problem in this model is PSPACE-complete even in dimension 1. Here, we investigate the complexity of the reachability problem when the model is extended with branching transitions, and we prove that the problem is EXPTIME-complete when the dimension is 2 or larger.

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
Keywords
  • Branching VASS
  • counter machines
  • reachability problem
  • bobrvass

Metrics

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

Related Versions

References

  1. Rajeev Alur and David L. Dill. A Theory of Timed Automata. Theor. Comput. Sci., 126(2):183-235, 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  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 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 32-43, 2015. URL: https://doi.org/10.1109/LICS.2015.14.
  3. Mikolaj Bojańczyk. Automata column. SIGLOG News, 1(2):3-12, 2014. URL: https://dl.acm.org/citation.cfm?id=2677163.
  4. Mikolaj Bojańczyk, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data trees and XML reasoning. J. ACM, 56(3):13:1-13:48, 2009. URL: https://doi.org/10.1145/1516512.1516515.
  5. Ahmed Bouajjani and Michael Emmi. Analysis of Recursively Parallel Programs. ACM Trans. Program. Lang. Syst., 35(3):10:1-10:49, 2013. URL: https://doi.org/10.1145/2518188.
  6. Lorenzo Clemente, Sławomir Lasota, Ranko Lazi\c', and Filip Mazowiecki. Timed pushdown automata and branching vector addition systems. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12, 2017. URL: https://doi.org/10.1109/LICS.2017.8005083.
  7. Costas Courcoubetis and Mihalis Yannakakis. Minimum and Maximum Delay Problems in Real-Time Systems. Formal Methods in System Design, 1(4):385-415, 1992. URL: https://doi.org/10.1007/BF00709157.
  8. Wojciech Czerwinski and Slawomir Lasota. Regular separability of one counter automata. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12, 2017. URL: https://doi.org/10.1109/LICS.2017.8005079.
  9. Matthias Englert, Ranko Lazic, and Patrick Totzke. Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 477-484, 2016. URL: https://doi.org/10.1145/2933575.2933577.
  10. John Fearnley and Marcin Jurdzinski. Reachability in two-clock timed automata is PSPACE-complete. Inf. Comput., 243:26-36, 2015. URL: https://doi.org/10.1016/j.ic.2014.12.004.
  11. 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, July 10-14, 2017, Warsaw, Poland, pages 119:1-119:14, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.119.
  12. Alain Finkel, Stefan Göller, and Christoph Haase. Reachability in Register Machines with Polynomial Updates. In Mathematical Foundations of Computer Science 2013 - 38th International Symposium, MFCS 2013, Klosterneuburg, Austria, August 26-30, 2013. Proceedings, pages 409-420, 2013. URL: https://doi.org/10.1007/978-3-642-40313-2_37.
  13. Stefan Göller, Christoph Haase, Ranko Lazic, and Patrick Totzke. A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. In 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, pages 105:1-105:13, 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.105.
  14. Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in Succinct and Parametric One-Counter Automata. In CONCUR 2009 - Concurrency Theory, 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings, pages 369-383, 2009. URL: https://doi.org/10.1007/978-3-642-04081-8_25.
  15. Christoph Haase, Joël Ouaknine, and James Worrell. On the Relationship between Reachability Problems in Timed and Counter Automata. In Reachability Problems - 6th International Workshop, RP 2012, Bordeaux, France, September 17-19, 2012. Proceedings, pages 54-65, 2012. URL: https://doi.org/10.1007/978-3-642-33512-9_6.
  16. Marcin Jurdziński, Jeremy Sproston, and François Laroussinie. Model Checking Probabilistic Timed Automata with One or Two Clocks. Logical Methods in Computer Science, 4(3), 2008. URL: https://doi.org/10.2168/LMCS-4(3:12)2008.
  17. Jérôme Leroux and Sylvain Schmitz. Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension. In LICS, 2019. URL: http://arxiv.org/abs/1903.08575.
  18. Ernst W. Mayr. An Algorithm for the General Petri Net Reachability Problem. SIAM J. Comput., 13(3):441-460, 1984. URL: https://doi.org/10.1137/0213029.
  19. Rich Schroeppel. A two counter machine cannot calculate 2N. Artificial Intelligence Memo No. 257, 1972. Google Scholar
  20. Leslie G. Valiant and Mike Paterson. Deterministic One-Counter Automata. J. Comput. Syst. Sci., 10(3):340-350, 1975. URL: https://doi.org/10.1016/S0022-0000(75)80005-5.
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