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

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 ≥ t. For reachability, we want to satisfy the relation x = t. In the more general setting, there is a Presburger formula φ(t, x), and we are given t and are asked if there is a reachable x with φ(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 φ, the problem is either NP-complete or belongs to 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.

For (i) and (ii), we introduce novel density measures for sets of integer vectors, and show an AC 1 upper bound if the respective density of the set defined by φ is positive; and NP-completeness otherwise. For (iii), the complexity border is characterized by a new notion of uniform quasi-upward closedness. In particular, we improve the best known upper bound for coverability in (binary encoded) 1-VASS from NC 2 (as shown by Almagor, Cohen, Pérez, Shirmohammadi, and Worrell in 2020) to AC 1 .

Deciding coverability in one-dim. Z-VASS via weighted automata over the tropical semiring (Z ∪ -∞, max, +, 0, 1) is a classical technique 2 : In this approach, the automaton is turned into a matrix, for which the n-th power is computed, where n is the number of states. Via repeated squaring, this leads to circuits of logarithmic depth, i.e. AC 1 . In our setting, we introduce a semiring F that permits the same for 1-VASS. However, matrix squaring in F seems to require TC 0 , meaning repeated squaring would only yield a TC 1 upper bound (see Remark VII.4; recall that AC 1 ⊆ TC 1 ⊆ NC 2 ). Instead, we include an additional approximation step to achieve the AC 1 upper bound.

We use boldface for vectors, and square brackets to index vectors. For example, if v ∈ Z k , then

Given u ∈ Z k1 and v ∈ Z k2 , we use the shorthand ⟨u, v⟩ to denote the vector ⟨u

A Z-weighted automaton A = ⟨Q, T, q 0 , q 1 ⟩ is an automaton where Q is a finite set of states, T ⊆ Q × Z × Q is a finite set of transitions, and q 0 , q 1 ∈ Q are the initial and final state, respectively. Here, for a transition ⟨q, w, r⟩ ∈ T , the number w is the weight of the transition. Transition weights are always encoded in binary.

We define three semantics. A configuration is a pair ⟨q, x⟩ for some q ∈ Q and x ∈ Z. For configurations ⟨q, x⟩, ⟨r, y⟩, we write ⟨q, x⟩ -→ Z ⟨r, y⟩ if there a transition ⟨q, w, r⟩ ∈ T with y = x + w. Moreover, ⟨q, x⟩ -→ VASS ⟨r, y⟩ means ⟨q, x⟩ -→ Z ⟨r, y⟩ and also x, y ≥ 0. Finally, ⟨q, x⟩ -→ N ⟨r, y⟩ means ⟨q, x⟩ -→ VASS ⟨r, y⟩ and also x ≤ y. These step relations are called integer semantics (-→ Z ), natural semantics (-→ N ), and VASS semantics (-→ VASS ). By * * -→ Z is replaced with * -→ N and * -→ VASS , respectively. Note that by definition of Reach N (S), we can only use transitions with non-negative weights. In addition, for * -→ VASS , this means for Reach VASS (S), we only consider runs where the counter value remains non-negative.