Reachability in Bidirected Pushdown VASS

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

*Corresponding author af dette arbejde

Publikation: Bidrag til bog/antologi/rapport/proceedingKonferencebidrag i proceedingsForskningpeer review


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.

Titel49th EATCS International Conference on Automata, Languages, and Programming, ICALP 2022
RedaktørerMikolaj Bojanczyk, Emanuela Merelli, David P. Woodruff
ForlagSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Publikationsdatojul. 2022
ISBN (Elektronisk)9783959772358
StatusUdgivet - jul. 2022
Begivenhed49th EATCS International Conference on Automata, Languages, and Programming, ICALP 2022 - Paris, Frankrig
Varighed: 4 jul. 20228 jul. 2022


Konference49th EATCS International Conference on Automata, Languages, and Programming, ICALP 2022
SponsorCentre National de la Recherche Scientifique ( CNRS ), Inria, Nomadic Lab, Université Paris Cité (Paris V, Paris VII)
NavnLeibniz International Proceedings in Informatics, LIPIcs


Dyk ned i forskningsemnerne om 'Reachability in Bidirected Pushdown VASS'. Sammen danner de et unikt fingeraftryk.