Document Open Access Logo

On the Reachability Problem for Two-Dimensional Branching VASS

Authors Clotilde Bizière , Thibault Hilaire , Jérôme Leroux , Grégoire Sutre

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2025.22.pdf
  • Filesize: 0.94 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Vector addition systems
  • Reachability problem
  • Semilinear sets
  • Verification

Metrics

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

Abstract

Vectors addition systems with states (VASS), or equivalently Petri nets, are arguably one of the most studied formalisms for the modeling and analysis of concurrent systems. A central decision problem for VASS is reachability: whether there exists a run from an initial configuration to a final one. This problem has been known to be decidable for over forty years, and its complexity has recently been precisely characterized. Our work concerns the reachability problem for BVASS, a branching generalization of VASS. In dimension one, the exact complexity of this problem is known. In this paper, we prove that the reachability problem for 2-dimensional BVASS is decidable. In fact, we even show that the reachability set admits a computable semilinear presentation. The decidability status of the reachability problem for BVASS remains open in higher dimensions.

Cite As Get BibTex

Clotilde Bizière, Thibault Hilaire, Jérôme Leroux, and Grégoire Sutre. On the Reachability Problem for Two-Dimensional Branching VASS. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.MFCS.2025.22

Author Details

Clotilde Bizière
  • LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP, Talence, France
Thibault Hilaire
  • LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP, Talence, France
Jérôme Leroux
  • LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP, Talence, France
Grégoire Sutre
  • LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP, Talence, France

References

  1. Mohamed Faouzi Atig and Pierre Ganty. Approximating petri net reachability along context-free traces. In Supratik Chakraborty and Amit Kumar, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011, December 12-14, 2011, Mumbai, India, volume 13 of LIPIcs, pages 152-163. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2011.152.
  2. Clotilde Bizière, Thibault Hilaire, Jérôme Leroux, and Grégoire Sutre. On the reachability problem for two-dimensional branching VASS, 2025. URL: https://arxiv.org/abs/2506.22561.
  3. Michael Blondin, Matthias Englert, Alain Finkel, Stefan Göller, Christoph Haase, Ranko Lazic, Pierre McKenzie, and Patrick Totzke. The reachability problem for two-dimensional vector addition systems with states. J. ACM, 68(5):34:1-34:43, 2021. URL: https://doi.org/10.1145/3464794.
  4. Mikolaj Bojanczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data trees and XML reasoning. In Stijn Vansummeren, editor, Proceedings of the Twenty-Fifth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 26-28, 2006, Chicago, Illinois, USA, pages 10-19. ACM, 2006. URL: https://doi.org/10.1145/1142351.1142354.
  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. Dmitry Chistikov, Wojciech Czerwinski, Filip Mazowiecki, Lukasz Orlikowski, Henry Sinclair-Banks, and Karol Wegrzycki. The tractability border of reachability in simple vector addition systems with states. In 65th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2024, Chicago, IL, USA, October 27-30, 2024, pages 1332-1354. IEEE, 2024. URL: https://doi.org/10.1109/FOCS61266.2024.00086.
  7. Lorenzo Clemente, Slawomir Lasota, Ranko Lazic, 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. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005083.
  8. Conrad Cotton-Barratt, Andrzej S. Murawski, and C.-H. Luke Ong. ML and extended branching VASS. In Hongseok Yang, editor, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10201 of Lecture Notes in Computer Science, pages 314-340. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_12.
  9. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for Petri nets is not elementary. J. ACM, 68(1):7:1-7:28, 2021. URL: https://doi.org/10.1145/3422822.
  10. Philippe de Groote, Bruno Guillaume, and Sylvain Salvati. Vector addition tree automata. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 64-73. IEEE Computer Society, 2004. URL: https://doi.org/10.1109/LICS.2004.1319601.
  11. Stéphane Demri, Marcin Jurdzinski, Oded Lachish, and Ranko Lazic. The covering and boundedness problems for branching vector addition systems. J. Comput. Syst. Sci., 79(1):23-38, 2013. URL: https://doi.org/10.1016/J.JCSS.2012.04.002.
  12. 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 Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 119:1-119:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPICS.ICALP.2017.119.
  13. Alain Finkel, Jérôme Leroux, and Grégoire Sutre. Reachability for two-counter machines with one test and one reset. In Sumit Ganguly and Paritosh K. Pandya, editors, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, December 11-13, 2018, Ahmedabad, India, volume 122 of LIPIcs, pages 31:1-31:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2018.31.
  14. Moses Ganardi, Rupak Majumdar, Andreas Pavlogiannis, Lia Schütze, and Georg Zetzsche. Reachability in bidirected pushdown VASS. In Mikolaj Bojanczyk, Emanuela Merelli, and David P. Woodruff, editors, 49th International Colloquium on Automata, Languages, and Programming, ICALP 2022, July 4-8, 2022, Paris, France, volume 229 of LIPIcs, pages 124:1-124:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.ICALP.2022.124.
  15. 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: https://doi.org/10.4230/LIPIcs.ICALP.2016.105.
  16. 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: https://doi.org/10.1016/0304-3975(79)90041-0.
  17. Florent Jacquemard, Luc Segoufin, and Jerémie Dimino. Fo2(<, +1, ~) on data trees, data tree automata and branching vector addition systems. Log. Methods Comput. Sci., 12(2), 2016. URL: https://doi.org/10.2168/LMCS-12(2:3)2016.
  18. Richard M. Karp and Raymond E. Miller. Parallel Program Schemata. J. Comput. Syst. Sci., 3(2):147-195, 1969. URL: https://doi.org/10.1016/S0022-0000(69)80011-5.
  19. Ranko Lazic. The reachability problem for vector addition systems with a stack is not elementary. CoRR, abs/1310.1767, 2013. URL: https://doi.org/10.48550/arXiv.1310.1767.
  20. Ranko Lazic, Thomas Christopher Newcomb, Joël Ouaknine, A. W. Roscoe, and James Worrell. Nets with tokens which carry data. Fundam. Informaticae, 88(3):251-274, 2008. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi88-3-03.
  21. 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: https://doi.org/10.1145/2733375.
  22. Jérôme Leroux. The reachability problem for Petri nets is not primitive recursive. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1241-1252. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00121.
  23. Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785796.
  24. Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. On the coverability problem for pushdown vector addition systems in one dimension. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 324-336. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_26.
  25. Denis Lugiez. Counting and equality constraints for multitree automata. In Andrew D. Gordon, editor, Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, volume 2620 of Lecture Notes in Computer Science, pages 328-342. Springer, 2003. URL: https://doi.org/10.1007/3-540-36576-1_21.
  26. 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.
  27. Filip Mazowiecki and Michal Pilipczuk. Reachability for bounded branching VASS. In Wan J. Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands, volume 140 of LIPIcs, pages 28:1-28:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPICS.CONCUR.2019.28.
  28. Hitoshi Ohsaki. Beyond regularity: Equational tree automata for associative and commutative theories. In Laurent Fribourg, editor, Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings, volume 2142 of Lecture Notes in Computer Science, pages 539-553. Springer, 2001. URL: https://doi.org/10.1007/3-540-44802-0_38.
  29. Owen Rambow. Multiset-valued linear index grammars: Imposing dominance constraints on derivations. In James Pustejovsky, editor, 32nd Annual Meeting of the Association for Computational Linguistics, 27-30 June 1994, New Mexico State University, Las Cruces, New Mexico, USA, Proceedings, pages 263-270. Morgan Kaufmann Publishers / ACL, 1994. URL: https://doi.org/10.3115/981732.981768.
  30. Sylvain Schmitz. On the computational complexity of dominance links in grammatical formalisms. In Jan Hajic, Sandra Carberry, and Stephen Clark, editors, ACL 2010, Proceedings of the 48th Annual Meeting of the Association for Computational Linguistics, July 11-16, 2010, Uppsala, Sweden, pages 514-524. The Association for Computer Linguistics, 2010. URL: https://aclanthology.org/P10-1053/.
  31. Kumar Neeraj Verma and Jean Goubault-Larrecq. Karp-miller trees for a branching extension of VASS. Discret. Math. Theor. Comput. Sci., 7(1):217-230, 2005. URL: https://doi.org/10.46298/DMTCS.350.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact