Document Open Access Logo

PVASS Reachability Is Decidable

Authors Roland Guttenberg , Eren Keskin , Roland Meyer

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.53.pdf
  • Filesize: 0.93 MB
  • 25 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • Pushdowns
  • Petri Nets
  • VASS
  • PVASS
  • Reachability
  • Decidability
  • Complexity

Metrics

Abstract

Reachability in pushdown vector addition systems with states (PVASS) is among the longest standing open problems in Theoretical Computer Science. We show that the problem is decidable in full generality. Our decision procedure is similar in spirit to the KLMST algorithm for VASS reachability, but works over objects that support an elaborate form of procedure summarization as known from pushdown reachability.

Cite As Get BibTex

Roland Guttenberg, Eren Keskin, and Roland Meyer. PVASS Reachability Is Decidable. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 53:1-53:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.53

Author Details

Roland Guttenberg
  • University of Warsaw, Poland
Eren Keskin
  • TU Braunschweig, Germany
Roland Meyer
  • TU Braunschweig, Germany

Funding

  • Guttenberg, Roland: Supported by the ERC grant INFSYS, agreement no. 950398.

References

  1. Ashwani Anand, Sylvain Schmitz, Lia Schütze, and Georg Zetzsche. Verifying unboundedness via amalgamation. In LICS, pages 4:1-4:15. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662133.
  2. Mohamed Faouzi Atig and Pierre Ganty. Approximating petri net reachability along context-free traces. In FSTTCS, 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.
  3. Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. Checking refinement of asynchronous programs against context-free specifications. In ICALP, volume 261 of LIPIcs, pages 110:1-110:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ICALP.2023.110.
  4. Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. Context-bounded verification of context-free specifications. Proc. ACM Program. Lang., 7(POPL):2141-2170, 2023. URL: https://doi.org/10.1145/3571266.
  5. Clotilde Bizière and Wojciech Czerwinski. Reachability in one-dimensional pushdown vector addition systems is decidable. In STOC, pages 1851-1862. ACM, 2025. URL: https://doi.org/10.1145/3717823.3718149.
  6. Michael Blondin and François Ladouceur. Population protocols with unordered data. In ICALP, volume 261 of LIPIcs, pages 115:1-115:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ICALP.2023.115.
  7. Rémi Bonnet. The reachability problem for vector addition system with one zero-test. In MFCS, volume 6907 of Lecture Notes in Computer Science, pages 145-157. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22993-0_16.
  8. Rémi Bonnet. Theory of Well-Structured Transition Systems and Extended Vector-Addition Systems. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, 2013. URL: http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bonnet-phd13.pdf.
  9. Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman. Separability of reachability sets of vector addition systems. In STACS, volume 66 of LIPIcs, pages 24:1-24:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.STACS.2017.24.
  10. Lorenzo Clemente, Slawomir Lasota, Ranko Lazic, and Filip Mazowiecki. Timed pushdown automata and branching vector addition systems. In LICS, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005083.
  11. Wojciech Czerwiński, Ismaël Jecker, Sławomir Lasota, Jérôme Leroux, and Łukasz Orlikowski. New lower bounds for reachability in vector addition systems. In FSTTCS, volume 284 of LIPIcs, pages 35:1-35:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2023.35.
  12. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for petri nets is not elementary. In STOC, pages 24-33. ACM, 2019. URL: https://doi.org/10.1145/3313276.3316369.
  13. Wojciech Czerwinski and Lukasz Orlikowski. Reachability in vector addition systems is ackermann-complete. In FOCS, pages 1229-1240. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00120.
  14. 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.
  15. J. Esparza. Petri nets, commutative context-free grammars, and basic parallel processes. Fundam. Informaticae, 31(1):13-25, 1997. URL: https://doi.org/10.3233/FI-1997-3112.
  16. Diego Figueira, Santiago Figueira, Sylvain Schmitz, and Philippe Schnoebelen. Ackermannian and primitive-recursive bounds with dickson’s lemma. In LICS, pages 269-278. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/LICS.2011.39.
  17. Alain Finkel and Jean Goubault-Larrecq. Forward analysis for wsts, part I: completions. In STACS, volume 3 of LIPIcs, pages 433-444. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2009. URL: https://doi.org/10.4230/LIPIcs.STACS.2009.1844.
  18. 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. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2018.31.
  19. Pierre Ganty and Rupak Majumdar. Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst., 34(1):6:1-6:48, 2012. URL: https://doi.org/10.1145/2160910.2160915.
  20. R. Guttenberg, E. Keskin, and R. Meyer. Pvass reachability is decidable, 2026. URL: https://arxiv.org/abs/2504.05015.
  21. Roland Guttenberg. Flattability of priority vector addition systems. In ICALP, volume 297 of LIPIcs, pages 141:1-141:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.ICALP.2024.141.
  22. Roland Guttenberg, Wojciech Czerwinski, and Slawomir Lasota. Reachability and related problems in vector addition systems with nested zero tests. In LICS, pages 581-593. IEEE, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00050.
  23. Peter Habermehl, Roland Meyer, and Harro Wimmel. The downward-closure of petri net languages. In ICALP (2), volume 6199 of Lecture Notes in Computer Science, pages 466-477. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14162-1_39.
  24. Piotr Hofman, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Sylvain Schmitz, and Patrick Totzke. Coverability trees for petri nets with unordered data. In FoSSaCS, volume 9634 of Lecture Notes in Computer Science, pages 445-461. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49630-5_26.
  25. Richard M. Karp and Raymond E. Miller. Parallel program schemata. JCSS, 3(2):147-195, 1969. URL: https://doi.org/10.1016/S0022-0000(69)80011-5.
  26. Eren Keskin and Roland Meyer. On the separability problem of VASS reachability languages. In LICS, pages 49:1-49:14. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662116.
  27. S. Rao Kosaraju. Decidability of reachability in vector addition systems. In STOC, pages 267-281. ACM, 1982. Google Scholar
  28. Jean-Luc Lambert. A structure to decide reachability in petri nets. Theor. Comput. Sci., 99(1):79-104, 1992. URL: https://doi.org/10.1016/0304-3975(92)90173-D.
  29. R. Lazic. The reachability problem for vector addition systems with a stack is not elementary. CoRR, abs/1310.1767, 2013. URL: https://arxiv.org/abs/1310.1767.
  30. Ranko Lazic. The reachability problem for branching vector addition systems requires doubly-exponential space. Inf. Process. Lett., 110(17):740-745, 2010. URL: https://doi.org/10.1016/J.IPL.2010.06.008.
  31. Ranko Lazic and Sylvain Schmitz. The complexity of coverability in ν-petri nets. In LICS, pages 467-476. ACM, 2016. URL: https://doi.org/10.1145/2933575.2933593.
  32. Jérôme Leroux. The general vector addition system reachability problem by presburger inductive invariants. In LICS, pages 4-13. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/LICS.2009.10.
  33. Jérôme Leroux. Vector addition system reachability problem: A short self-contained proof. In LATA, volume 6638 of Lecture Notes in Computer Science, pages 41-64. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21254-3_3.
  34. Jérôme Leroux. The reachability problem for petri nets is not primitive recursive. In FOCS, pages 1241-1252. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00121.
  35. Jérôme Leroux, M. Praveen, Philippe Schnoebelen, and Grégoire Sutre. On functions weakly computable by pushdown petri nets and related systems. Log. Methods Comput. Sci., 15(4), 2019. URL: https://doi.org/10.23638/LMCS-15(4:15)2019.
  36. Jérôme Leroux, M. Praveen, and Grégoire Sutre. Hyper-ackermannian bounds for pushdown vector addition systems. In CSL-LICS, pages 63:1-63:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603146.
  37. Jérôme Leroux and Sylvain Schmitz. Demystifying reachability in vector addition systems. In LICS, pages 56-67. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.16.
  38. 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. URL: https://doi.org/10.1109/LICS.2019.8785796.
  39. Jérôme Leroux and Grégoire Sutre. Reachability in two-dimensional vector addition systems with states: One test is for free. In CONCUR, volume 171 of LIPIcs, pages 37:1-37:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.37.
  40. 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 Lecture Notes in Computer Science, pages 324-336. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_26.
  41. Ernst W. Mayr. An algorithm for the general petri net reachability problem. In STOC, pages 238-246. ACM, 1981. URL: https://doi.org/10.1145/800076.802477.
  42. T. Place and M. Zeitoun. Separating regular languages with first-order logic. In CSL-LICS, pages 75:1-75:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603098.
  43. Charles Rackoff. The covering and boundedness problems for vector addition systems. TCS, 6:223-231, 1978. URL: https://doi.org/10.1016/0304-3975(78)90036-1.
  44. Klaus Reinhardt. Reachability in petri nets with inhibitor arcs. In RP, volume 223 of Electronic Notes in Theoretical Computer Science, pages 239-264. Elsevier, 2008. URL: https://doi.org/10.1016/J.ENTCS.2008.12.042.
  45. Thomas W. Reps, Susan Horwitz, and Shmuel Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL, pages 49-61. ACM Press, 1995. URL: https://doi.org/10.1145/199448.199462.
  46. Fernando Rosa-Velardo and David de Frutos-Escrig. Decidability and complexity of petri nets with unordered data. Theor. Comput. Sci., 412(34):4439-4451, 2011. URL: https://doi.org/10.1016/J.TCS.2011.05.007.
  47. George S. Sacerdote and Richard L. Tenney. The decidability of the reachability problem for vector addition systems (preliminary version). In STOC, pages 61-76. ACM, 1977. URL: https://doi.org/10.1145/800105.803396.
  48. Sylvain Schmitz. Complexity hierarchies beyond elementary. ACM Trans. Comput. Theory, 8(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2858784.
  49. Sergey Sevast'janov and Wojciech Banaszczyk. To the Steinitz Lemma in Coordinate Form. Discrete Mathematics, 169(1-3):145-152, 1997. URL: https://doi.org/10.1016/0012-365X(94)00240-J.
  50. M Sharir and A Pnueli. Two approaches to interprocedural data flow analysis. New York Univ. Comput. Sci. Dept., 1978. Google Scholar
  51. Ernst Steinitz. Bedingt Konvergente Reihen und Konvexe Systeme, 1913. Google Scholar
  52. 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.
  53. Georg Zetzsche. Monoids as Storage Mechanisms. PhD thesis, Kaiserslautern University of Technology, Germany, 2016. URL: https://kluedo.ub.rptu.de/frontdoor/index/index/docId/4400.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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