Reachability in Bidirected Pushdown VASS

Moses Ganardi*, Rupak Majumdar, Andreas Pavlogiannis, Lia Schütze, Georg Zetzsche

*Corresponding author for this work

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

Abstract

A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown store. A PVASS is said to be bidirected if every transition (pushing/popping a symbol or modifying a counter) has an accompanying opposite transition that reverses the effect. Bidirectedness arises naturally in many models; it can also be seen as a overapproximation of reachability. We show that the reachability problem for bidirected PVASS is decidable in Ackermann time and primitive recursive for any fixed dimension. For the special case of one-dimensional bidirected PVASS, we show reachability is in PSPACE, and in fact in polynomial time if the stack is polynomially bounded. Our results are in contrast to the directed setting, where decidability of reachability is a long-standing open problem already for one dimensional PVASS, and there is a PSPACE-lower bound already for one-dimensional PVASS with bounded stack. The reachability relation in the bidirected (stateless) case is a congruence over ℕd. Our upper bounds exploit saturation techniques over congruences. In particular, we show novel elementary-time constructions of semilinear representations of congruences generated by finitely many vector pairs. In the case of one-dimensional PVASS, we employ a saturation procedure over bounded-size counters. We complement our upper bound with a TOWER-hardness result for arbitrary dimension and k-EXPSPACE hardness in dimension 2k + 6 using a technique by Lazić and Totzke to implement iterative exponentiations.

Original languageEnglish
Title of host publication49th EATCS International Conference on Automata, Languages, and Programming, ICALP 2022
EditorsMikolaj Bojanczyk, Emanuela Merelli, David P. Woodruff
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Publication dateJul 2022
Article number124
ISBN (Electronic)9783959772358
DOIs
Publication statusPublished - Jul 2022
Event49th EATCS International Conference on Automata, Languages, and Programming, ICALP 2022 - Paris, France
Duration: 4 Jul 20228 Jul 2022

Conference

Conference49th EATCS International Conference on Automata, Languages, and Programming, ICALP 2022
Country/TerritoryFrance
CityParis
Period04/07/202208/07/2022
SponsorFrench National Centre for Scientific Research (CNRS), Inria, Nomadic Lab, Universite Paris 5
SeriesLeibniz International Proceedings in Informatics, LIPIcs
Volume229
ISSN1868-8969

Keywords

  • Complexity
  • Decidability
  • Pushdown
  • Reachability
  • Vector addition systems

Fingerprint

Dive into the research topics of 'Reachability in Bidirected Pushdown VASS'. Together they form a unique fingerprint.

Cite this