The Tractability of Reachability in Simple Vector Addition Systems with States

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 reachability problem asks whether there is a run from a given starting configuration to a given target configuration. When the input is encoded in binary, reachability is computationally intractable: even in dimension one, it is NP-hard. This presentation with detail the tractability border of the problem when the input is encoded in unary. As a 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 (SLPS). The underlying graph structure of an SLPS is just a path with self-loops at each node. This lower bound improves upon a recent result of Czerwiński and Orlikowski [LICS 2022], in both the number of counters and expressiveness of the considered model. It also answers open questions of Englert, Lazić, and Totzke [LICS 2016] and Leroux [PETRI NETS 2021]. This presentation will also showcase an 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. To further trace the tractability border, the presentation will also touch on a neighbouring upper bound. Extending upon the main result of Englert, Lazić, and Totzke [LICS 2016], we present a polynomial-time algorithm for reachability in unary 2-SLPS when the initial and target configurations are specified in binary.

Based on work with Dmitry Chistikov, Wojciech Czerwiński, Filip Mazowiecki, Łukasz Orlikowski, and Karol Węgrzycki to appear in FOCS'24.

Oxford Verification Seminar 
University of Oxford, UK
Henry Sinclair-Banks, 17/10/24