Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

PVASS Reachability is Decidable

Roland Guttenberg, Eren Keskin, Roland Meyer

TL;DR

The paper proves that reachability for pushdown vector addition systems with states (PVASS) is decidable in full generality by embedding PVASS into nested grammar vector addition systems (NGVAS) and reducing reachability to NGVAS emptiness. It develops a layered framework combining perfect NGVAS, deconstructions, pumping (horizontal and vertical), and a wide-tree theorem to bridge Z-runs to actual runs, yielding a KLMST-style decision procedure with Hyper-Ackermann time complexity. A novel coverability grammar and a Karp–Miller–style construction enable precise computation of pre/post relations and decompositions, whileRackoff-type arguments provide essential bounds for pumping. The approach yields a semilinear approximation of PVAS reachability that may be reusable in broader contexts, and it establishes the decidability and complexity of PVASS reachability with a rigorous, multi-faceted machinery.

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.

PVASS Reachability is Decidable

TL;DR

The paper proves that reachability for pushdown vector addition systems with states (PVASS) is decidable in full generality by embedding PVASS into nested grammar vector addition systems (NGVAS) and reducing reachability to NGVAS emptiness. It develops a layered framework combining perfect NGVAS, deconstructions, pumping (horizontal and vertical), and a wide-tree theorem to bridge Z-runs to actual runs, yielding a KLMST-style decision procedure with Hyper-Ackermann time complexity. A novel coverability grammar and a Karp–Miller–style construction enable precise computation of pre/post relations and decompositions, whileRackoff-type arguments provide essential bounds for pumping. The approach yields a semilinear approximation of PVAS reachability that may be reusable in broader contexts, and it establishes the decidability and complexity of PVASS reachability with a rigorous, multi-faceted machinery.

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.

Paper Structure

This paper contains 65 sections, 118 theorems, 139 equations.

Table of Contents

  1. Introduction
  2. Proof Outline
  3. Overall Argument
  4. Iteration Lemma
  5. NGVAS
  6. Perfectness
  7. Proof of the Iteration Lemma (Proposition \ref{['Proposition:Iteration']})
  8. Rank of an NGVAS
  9. Up- and Down-Pumping
  10. Computing $\mathsf{refine}_{\textsf{(R2)}}$
  11. Generalization
  12. Computing $\mathsf{pre}_{}$ and $\mathsf{post}_{}$: Simple Cases
  13. Computing $\mathsf{pre}_{}$ and $\mathsf{post}_{}$: Hard Case 1
  14. Computing $\mathsf{pre}_{}$ and $\mathsf{post}_{}$: Hard Case 2
  15. Preliminaries
  16. ...and 50 more sections

Key Result

Theorem 1

$\mathit{R}_{\mathbb{N}}(\mathit{N})\neq\emptyset$ is decidable (in Hyper-Ackermann time).

Theorems & Definitions (165)

  • Theorem 1
  • Proposition 2: Iteration Lemma
  • Proposition 3: Deconstruction
  • Proposition 4
  • Lemma 5
  • Lemma 6
  • Theorem 7
  • Lemma 7
  • Lemma 7
  • Lemma 7
  • ...and 155 more