The Tractability Border of Reachability in Simple Vector Addition Systems with States

TL;DR

The paper maps the tractability border for reachability in simple vector addition systems with states under unary encodings, identifying sharp NP-hardness results for unary $3$-SLPS and unitary $\alpha(k)$-SLPS, while delivering a polynomial-time algorithm for unary $2$-SLPS with binary-encoded endpoints. It introduces novel structural decompositions of runs and employs a controlling-counter framework to simulate zero tests, enabling SAT-based hardness reductions to be carried within restricted SLPS. The work also extends hardness results to ultraflat unary VASS and develops a polynomial-time DP algorithm for a key binary-encoded setting, thus advancing understanding of the intricate boundary between tractable and intractable reachability in Petri-net-like models. Overall, the paper contributes both hardness machinery and efficient algorithms that sharpen our view of how encoding and dimensional parameters impact reachability complexity in VASS-like systems.

Abstract

Vector Addition Systems with States (VASS), equivalent to Petri nets, are a well-established model of concurrency. The central algorithmic challenge in VASS is the reachability problem: is there a run from a given starting state and counter values to a given target state and counter values? When the input is encoded in binary, reachability is computationally intractable: even in dimension one, it is NP-hard. In this paper, we comprehensively characterise the tractability border of the problem when the input is encoded in unary. For our main result, we prove that reachability is NP-hard in unary encoded 3-VASS, even when structure is heavily restricted to be a simple linear path scheme. This improves upon a recent result of Czerwiński and Orlikowski (2022), in both the number of counters and expressiveness of the considered model, as well as answers open questions of Englert, Lazić, and Totzke (2016) and Leroux (2021). The underlying graph structure of a simple linear path scheme (SLPS) is just a path with self-loops at each node. We also study the exceedingly weak model of computation that is SPLS with counter updates in {-1,0,+1}. Here, we show that reachability is NP-hard when the dimension is bounded by O(α(k)), where αis the inverse Ackermann function and k bounds the size of the SLPS. We complement our result by presenting a polynomial-time algorithm that decides reachability in 2-SLPS when the initial and target configurations are specified in binary. To achieve this, we show that reachability in such instances is well-structured: all loops, except perhaps for a constant number, are taken either polynomially many times or almost maximally. This extends the main result of Englert, Lazić, and Totzke (2016) who showed the problem is in NL when the initial and target configurations are specified in unary.

Figures (16)

• Figure 1: The figure presents the schematic view of the structure of reachability runs for unary 2-SLPS with binary-encoded $s({\bf x})$ and $t({\bf y})$. The grey parts of the run (little curves) are of polynomial length. The first four cycles (straight arrows highlighted in red) are taken $m_i$ times, and one of the endpoints of each of them is within polynomial distance from the axes. The last three cycles (straight arrows highlighted in blue) can terminate at arbitrary points.
• Figure 2: An example 2-SLPS in which, from the initial state with initial values $(0, 0)$, the final state can only be reached with values $(0,2)$. On the left is a drawing of the 2-SLPS and on the right it is presented as a counter program.
• Figure 3: A simple linear path schemes SAT($\varphi$) with one counter $\mathsf{x}$ and non-divisibility checks; reachability from the initial state to the final state is equivalent to satisfiability of $\varphi$. Although only one counter $\mathsf{x}$ is explicitly presented, the non-divisibility assertions are implemented by the non-divisibility($\cdot$) gadgets that use ancillary counters (see \ref{['fig:unary-non-div']} for unary encoding and \ref{['fig:unitary-non-div']} for unitary encoding). Notation: $n$ is the number of variables in $\varphi$, $m$ is the number of clauses in $\varphi$, and $p_1, \ldots, p_n$ are pairwise coprime integers greater than $1$ (e.g., the first $n$ primes).
• Figure 4: The $\textup{non-divisibility(}$p$\textup{)}$ gadget implemented as a unary 2-SLPS with two zero tests for asserting that the initial value $v$ of counter $\mathsf{x}$ is not divisible by the fixed positive integer $p$. The construction, which has linear size in $p$, uses 2 counters, the primary $\mathsf{x}$ and its ancillary $\mathsf{y}$. From an initial configuration with $\mathsf{x} = v, \mathsf{y} = 0$, the final configuration with $\mathsf{x} = v, \mathsf{y} = 0$ can be reached if and only if $p$ does not divide $v$. Note that $\Delta\mathsf{x}$ is the change in the counter value of $\mathsf{x}$.
• Figure 5: A drawing of the SLPS $\mathcal{V} = \alpha_0 \beta_1^* \alpha_1 \cdots \alpha_{k-1} \beta_k^* \alpha_k$.

Theorems & Definitions (61)

• Theorem 1.1
• Theorem 1.2
• Theorem 1.3
• Theorem 2.1
• Lemma 2.2: Controlling Counter Technique, cf. CzerwinskiO21
• Lemma 3.1
• Claim 3.2
• proof : Proof of Theorem \ref{['thm:3-lps-hardness']}
• Lemma 3.3
• Claim 3.4