PVASS Reachability Is Decidable
Roland Guttenberg, Eren Keskin, Roland Meyer
2026Year
2Top-tier citations
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.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Cited by top-tier papers2
- General Decidability Results for Systems with Continuous CountersA. R. Balasubramanian, Matthew Hague, Rupak Majumdar, Ramanathan S. Thinniyam et al.POPL 2026
- Reachability in VASS Extended with Integer CountersClotilde Bizière, Wojciech Czerwinski, Roland Guttenberg, Jérôme Leroux et al.LICS 2026
Builds on7
- Reachability in Vector Addition Systems is Ackermann-completeWojciech Czerwinski, Lukasz OrlikowskiFOCS 2021 · 69 citations
- The Reachability Problem for Petri Nets is Not Primitive RecursiveJérôme LerouxFOCS 2021 · 62 citations
- Reachability and Related Problems in Vector Addition Systems with Nested Zero TestsRoland Guttenberg, Wojciech Czerwinski, Slawomir LasotaLICS 2025 · 10 citations
- Verifying Unboundedness via AmalgamationAshwani Anand, Sylvain Schmitz, Lia Schütze, Georg ZetzscheLICS 2024 · 5 citations
- Context-Bounded Verification of Context-Free SpecificationsPascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam et al.POPL 2023 · 3 citations
Related papers
- Reachability in One-Dimensional Pushdown Vector Addition Systems Is DecidableClotilde Bizière, Wojciech CzerwinskiSTOC 2025 · 2 citations
- Reachability in Continuous Pushdown VASSA. R. Balasubramanian, Rupak Majumdar, Ramanathan S. Thinniyam, Georg ZetzschePOPL 2024 · 1 citation
- An Approach to Regular Separability in Vector Addition SystemsWojciech Czerwinski, Georg ZetzscheLICS 2020 · 4 citations
- The Complexity of Reachability in Affine Vector Addition Systems with StatesMichael Blondin, Mikhail A. RaskinLICS 2020 · 4 citations
- The Tractability Border of Reachability in Simple Vector Addition Systems with StatesDmitry Chistikov, Wojciech Czerwinski, Filip Mazowiecki, Lukasz Orlikowski et al.FOCS 2024 · 1 citation
