Paper: PVASS Reachability Is Decidable (at LICS 2026)

Authors: Roland Guttenberg Eren Keskin Roland Meyer

Open access: https://doi.org/10.4230/LIPIcs.LICS.2026.53

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.

BibTeX

  @InProceedings{GuttenbergKeskinMey-PVASSReachabilityIs,
    author = 	 {Roland Guttenberg and Eren Keskin and Roland Meyer},
    title = 	 {PVASS Reachability Is Decidable},
    booktitle =  {Proceedings of the Forty-First Annual Symposium on Logic in Computer Science (LICS 2026)},
    year =	 {2026},
    month =	 {July}, 
    pages =      {53:1--53:25},
    location =   {Lisbon, Portugal}, 
    publisher =	 {Schloss Dagstuhl -- Leibniz-Zentrum für Informatik},
    doi =        {10.4230/LIPIcs.LICS.2026.53}
  }