The Tractability Border of Reachability in Simple Vector Addition Systems with States.
Dmitry Chistikov, Wojciech Czerwiński, Filip Mazowiecki, Łukasz Orlikowski, Henry Sinclair-Banks, and Karol Węgrzycki.
In FOCS'24.
DOI: https://doi.org/10.1109/FOCS61266.2024.00086
Full version: https://arxiv.org/abs/2412.16612

Abstract: Vector Addition Systems with States (VASS), equivalent to Petri nets, are a well-established model of concurrency. A d-VASS can be seen as directed graph whose edges are labelled by d-dimensional integer vectors. While following a path, the values of d nonnegative integer counters are updated according to the integer labels. The central algorithmic challenge in VASS is the reachability problem: is there a run from a given starting node and counter values to a given target node 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 [LICS 2022], in both the number of counters and expressiveness of the considered model, as well as answers open questions of Englert, Lazić, and Totzke [LICS 2016] and Leroux [PETRI NETS 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 [LICS 2016] who showed the problem is in NL when the initial and target configurations are specified in unary.