Reachability in Bidirected Pushdown VASS

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ć and Totzke to implement iterative exponentiations.

No reviews yet.

No comments yet.