Continuous Pushdown VASS in One Dimension are Easy

TL;DR

The paper addresses the reachability, coverability, and boundedness analysis of one-dimensional continuous pushdown VASS (C1PVASS). By reducing problems to PDAs and using Presburger arithmetic, it proves that these analyses are computable in polynomial time for 0-C1PVASS, and in NP (reachability and coverability) with coNP (boundedness) when lower-bound guards are added. A key technique is the Dense Normal Form (DNF) for k-reachability, along with PDA constructions and Presburger encodings that preserve the Parikh image structure. The results significantly improve the tractability of analysis for this relaxed model and offer a framework for approximating PVASS behavior in recursive-program contexts, with potential extensions to bounded counter domains.

Abstract

A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown stack. The algorithmic analysis of PVASS has applications such as static analysis of recursive programs manipulating integer variables. Unfortunately, reachability analysis, even for one-dimensional PVASS is not known to be decidable. We relax the model of one-dimensional PVASS to make the counter updates continuous and show that in this case reachability, coverability, and boundedness are decidable in polynomial time. In addition, for the extension of the model with lower-bound guards on the states, we show that coverability and reachability are in NP, and boundedness is in coNP.

Figures (4)

• Figure 1: An example of a C1PVASS $\mathcal{A}$.
• Figure 2: Simulating $n$ many $+1$ updates using simple binary arithmetic.
• Figure 5: A slice of the PDA $\mathcal{P}$ constructed for $k$-coverability of a C1PVASS. The subscript being $i$ for $0\leq i\leq m$ of a block (for example, $i$ in $\mathcal{I}_{i}^{}$) denotes that all the states in the block have lower bounds at most $\ell_i$. Note $+0 : \epsilon$ is omitted unless it is the only option for transitions in the block.
• Figure 6: The $i^\text{th}$ slice of the PDA $\mathcal{P}$ constructed for $k$-reachability of a C1PVASS. The slice itself is inside the dashed box, the text to the right provides intuition for the layer. The subscript being $i$ for $0\leq i\leq m$ of a block (eg, $i$ in $\mathcal{I}_{i}^{}$) denotes that all the states in the block have lower bounds at most $\ell_i$. Note $+0$ is omitted unless it is the only option for transitions in the block.

Theorems & Definitions (28)

• definition 1: Pushdown automata
• definition 2: Context-free grammars
• definition 3: C1PVASS
• lemma 1
• lemma 2
• definition 4: 0-C1PVASS
• lemma 3
• Remark 1
• Remark 2
• theorem 1