License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2022.124
URN: urn:nbn:de:0030-drops-164651
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16465/
Ganardi, Moses ;
Majumdar, Rupak ;
Pavlogiannis, Andreas ;
Schütze, Lia ;
Zetzsche, Georg
Reachability in Bidirected Pushdown VASS
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.
BibTeX - Entry
@InProceedings{ganardi_et_al:LIPIcs.ICALP.2022.124,
author = {Ganardi, Moses and Majumdar, Rupak and Pavlogiannis, Andreas and Sch\"{u}tze, Lia and Zetzsche, Georg},
title = {{Reachability in Bidirected Pushdown VASS}},
booktitle = {49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
pages = {124:1--124:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-235-8},
ISSN = {1868-8969},
year = {2022},
volume = {229},
editor = {Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16465},
URN = {urn:nbn:de:0030-drops-164651},
doi = {10.4230/LIPIcs.ICALP.2022.124},
annote = {Keywords: Vector addition systems, Pushdown, Reachability, Decidability, Complexity}
}
|
Keywords: |
|
Vector addition systems, Pushdown, Reachability, Decidability, Complexity |
|
Collection: |
|
49th International Colloquium on Automata, Languages, and Programming (ICALP 2022) |
|
Issue Date: |
|
2022 |
|
Date of publication: |
|
28.06.2022 |
