Reachability in Bidirected Pushdown VASS

TL;DR

This paper proves that reachability in bidirected PVASS is decidable with high complexity bounds, contrasting with the open problem in the directed case, and introduces new saturation techniques for analyzing these systems.

Contribution

It establishes decidability and complexity bounds for reachability in bidirected PVASS, introduces saturation techniques over congruences, and provides new elementary constructions for semilinear representations.

Findings

Reachability in bidirected PVASS is decidable in Ackermann time.

One-dimensional bidirected PVASS reachability is in PSPACE and polynomial with bounded stack.

The problem is TOWER-hard in arbitrary dimensions and EXPSPACE-hard in certain cases.

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 \emph{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 \emph{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 $\mathsf{PSPACE}$, and in fact in polynomial time if the stack is polynomially bounded. Our results are in contrast to the \emph{directed} setting, where decidability of reachability is a long-standing open problem already for one dimensional PVASS, and there is a $\mathsf{PSPACE}$-lower bound already for one-dimensional PVASS with bounded stack. The reachability relation in the bidirected (stateless) case is a congruence over $\mathbb{N}^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 $\mathsf{TOWER}$-hardness result for arbitrary dimension and $k$-$\mathsf{EXPSPACE}$ hardness in dimension $2k+6$ using a technique by Lazi\'{c} and Totzke to implement iterative exponentiations.