A Complexity Dichotomy for Semilinear Target Sets in Automata with One Counter

TL;DR

The paper analyzes the computational hardness of reachability in one-counter systems under fixed Presburger target sets, revealing sharp dichotomies: for three models—the integer, natural, and VASS semantics—the problem is either in $AC^1$ or $NP$-complete. Central to the approach is the local density measure $D(S)$ (and $D^+(S)$ for natural semantics), which characterizes tractable instances; positive density yields $AC^1$ decidability, while zero density yields $NP$-hardness. The authors introduce constructive building blocks $S^{( ho,m)}$ based on $ ho$-chains of intervals and develop a semiring-based framework and residue-class reductions to realize $AC^1$ algorithms, including a new $AC^1$-algorithm for coverability in 1-VASS. They also show decidability of the dichotomy boundaries and provide reductions to establish hardness results, offering a comprehensive map of the tractability landscape for semilinear target sets in one-counter automata with different semantics. The work advances both theoretical understanding and practical verification of infinite-state systems by pinpointing when efficient, parallelizable solutions are possible and when inherent combinatorial hardness persists.

Abstract

In many kinds of infinite-state systems, the coverability problem has significantly lower complexity than the reachability problem. In order to delineate the border of computational hardness between coverability and reachability, we propose to place these problems in a more general context, which makes it possible to prove complexity dichotomies. The more general setting arises as follows. We note that for coverability, we are given a vector $t$ and are asked if there is a reachable vector $x$ satisfying the relation $x\ge t$. For reachability, we want to satisfy the relation $x=t$. In the more general setting, there is a Presburger formula $\varphi(t,x)$, and we are given $t$ and are asked if there is a reachable $x$ with $\varphi(t,x)$. We study this setting for systems with one counter and binary updates: (i) integer VASS, (ii) Parikh automata, and (i) standard (non-negative) VASS. In each of these cases, reachability is NP-complete, but coverability is known to be in polynomial time. Our main results are three dichotomy theorems, one for each of the cases (i)--(iii). In each case, we show that for every $\varphi$, the problem is either NP-complete or belongs to $\mathsf{AC}^1$, a circuit complexity class within polynomial time. We also show that it is decidable on which side of the dichotomy a given formula falls.

Figures (5)

• Figure 1: An illustration for \ref{['exa:z3']}. The solid black and dashed grey horizonal line segments represent the set $S_3[t]$ and its complement, respectively. The top picture shows that $D_k(S_3[t], \textcolor{red}{x_1}) \geq \frac{1}{2}$ for any (red) point $\textcolor{red}{x_1} \in (-\infty, 0]$. The bottom picture shows that $D_k(S_3[t], \textcolor{blue}{x_2}) \geq \frac{1}{4}$ for any (blue) point $\textcolor{blue}{x_2} \in [t,2t]$.
• Figure 2: An illustration for \ref{['exa:z4']}. The solid black and dashed grey horizonal line segments represent the set $S_4[t]$ and its complement, respectively. The top picture shows that $D_k(S_4[t], \textcolor{red}{x_1}) \geq \frac{1}{2}$ for any (red) point $\textcolor{red}{x_1} \in (-\infty, 0]$. The middle picture shows that $D_k(S_4[t], \textcolor{Green}{x_2}) \geq \frac{1}{3}$ for any (green) point $\textcolor{Green}{x_2} \in [t+s, 2t+2s]$. The bottom picture shows that $D_k(S_4[t], \textcolor{blue}{x_3}) \geq \frac{1}{4}$ for any (blue) point $\textcolor{blue}{x_3} \in [3t+2s, 4t+2s]$.
• Figure 3: An illustration for Condition \ref{['itm:december']} of \ref{['def:chain']} (when $m = 3$). The solid black horizonal line segments represent a sequence of pairwise disjoint intervals $I_1, I_2, I_3, I_4$ where $|I_1| \leq \ldots \leq |I_4| = \infty$. The dashed grey horizonal line segments represent the complement of $I_1 \cup I_2 \cup I_3 \cup I_4$. The top picture shows a scenario when Condition \ref{['itm:december']} is satisfied; notice that for $i = 3$, $I_3 < I_1$ and $I_3 < I_2$ (and for $i = 2$, $I_2 > I_1$). The bottom picture shows a scenario when Condition \ref{['itm:december']} is falsified; observe for $i = 3$: $I_3 > I_1$ but $I_3 < I_2$.
• Figure 4: Drawn in blue is the coverability function $f$ (labelled with its two discontinuities) for the $\langle p,q \rangle$ coverability table $\langle 4, 2 \rangle, \langle 9, 9 \rangle$. Drawn in red is $\sigma(f) = \bar{X}^4$. For the definition of $\bar{X}$, see the text above \ref{['discontinuities']}; and for the definition of $\sigma$, please turn to def:sigma. Note that the $y$-axis has been scale by a factor of $0.5$.
• Figure 5: The $1$-VASS $\mathcal{V}$; here $v \geq 0$ is a variable. The instance of reachability in $\mathcal{V}$ from $\langle p, 0 \rangle$ to $\langle r, v \rangle$ is positive if and only if the instance of subset sum $\langle x_1, \ldots, x_n, y \rangle$ is positive; see \ref{['clm:subset-sum-vas']}.

Theorems & Definitions (145)

• Remark 3.1
• Theorem 3.2
• Example 3.3
• Example 3.4
• Example 3.5
• Example 3.6
• Example 3.7
• Theorem 3.8
• Theorem 3.9
• Example 3.10