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

TL;DR

This paper establishes a clear complexity dichotomy for semilinear target set problems in automata with one counter, showing they are either NP-complete or in AC^1, depending on the formula.

Contribution

It proves the first complexity dichotomies for these problems and provides a method to decide the complexity class for any given formula.

Findings

NP-complete or AC^1 complexity depending on the formula

Decidability of the complexity class for each formula

Main results are three dichotomy theorems for different systems

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.