Reachability in One-Dimensional Pushdown Vector Addition Systems is Decidable

TL;DR

This paper proves that the reachability problem for one-dimensional Pushdown Vector Addition Systems (1-PVAS) is decidable by transforming the problem into an equivalent model with the thin property, resolving a long-standing open problem.

Contribution

It introduces a method to convert any 1-GVAS into a thin 1-GVAS with the same reachability, establishing decidability for 1-PVAS and linking it to elementary time complexity.

Findings

Decidability of reachability in 1-PVAS established.

Construction of a thin 1-GVAS equivalent to any given 1-GVAS.

If reachability in thin 1-GVAS is elementary, then it is for all 1-GVAS.

Abstract

We consider the model of one-dimensional Pushdown Vector Addition Systems (1-PVAS), a fundamental computational model simulating both recursive and concurrent behaviours. Our main result is decidability of the reachability problem for 1-PVAS, an important open problem investigated for at least a decade. In the algorithm we actually consider an equivalent model of Grammar Vector Addition Systems (GVAS). We prove the main result by showing that for every one-dimensional GVAS (1-GVAS) one can compute another 1-GVAS, which has the same reachability relation as the original one and additionally has the so-called thin property. Due to the work of Atig and Ganty from 2011, thin 1-GVAS have decidable reachability problem, therefore our construction implies decidability of the problem for all 1-GVAS. Moreover, we also show that if reachability in thin 1-GVAS can be decided in elementary time then also reachability in all 1-GVAS can be decided in elementary time.