Henry Sinclair-Banks

Highlights Conference 2025 Conference Abstract

Which Semilinear Target Sets Make Reachability in 1-VASS Easy?

• Henry Sinclair-Banks

FOCS Conference 2024 Conference Paper

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

• Dmitry Chistikov 0001
• Wojciech Czerwinski
• Filip Mazowiecki
• Lukasz Orlikowski
• Henry Sinclair-Banks
• Karol Wegrzycki

Vector Addition Systems with States (VASS), equiv-alent 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(a(k)), where $a$ 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.

Highlights Conference 2024 Conference Abstract

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

• Henry Sinclair-Banks

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. This presentation concerns work with Dmitry Chistikov, Wojciech Czerwiński, Filip Mazowiecki, Łukasz Orlikowski, and Karol Węgrzycki that will appear in FOCS'24.

Highlights Conference 2023 Conference Abstract

Coverability in VASS Revisited: Improving Rackoff’s Bounds to Obtain Conditional Optimaility

• Henry Sinclair-Banks

Seminal results establish that the coverability problem for Vector Addition Systems with States (VASS) is in EXPSPACE (Rackoff, '78) and is EXPSPACE-hard already under unary encodings (Lipton, '76). More precisely, Rosier and Yen later utilise Rackoff's bounding technique to show that if coverability holds then there is a run of length at most n^(2^(O(d*log(d))), where d is the dimension and n is the size of the given unary VASS. Earlier, Lipton showed that there exist instances of coverability in d-dimensional unary VASS that are only witnessed by runs of double-exponential length that is at least n^(2^(Omega(d))). In this presentation, I will outline how to carefully strengthen Rackoff's approach to improve the upper bound to show that if coverability holds then there exists a run of length at most n^(2^(O(d))). Moreover, we therefore obtain an optimal 2^(O(d))*log(n)-space algorithm for coverability. This closes a forty-one-year-old gap that was stated as an open problem by Mayr and Meyer. Furthermore, we obtain a deterministic n^(2^(O(d)))-time algorithm for coverability in unary d-VASS. We show that this is optimal under the Exponential Time Hypothesis, in particular by leveraging the time required to detect a clique in a graph. I also plan to present the approach and techniques used in our reduction from finding cliques in graphs to coverability in unary VASS. Ultimately, this yields a conditional matching lower bound that coverability in unary d-VASS requires n^(2^(Omega(d)))-time. This presentation concerns ongoing joint work with Marvin Künnemann, Filip Mazowiecki, Lia Schütze, and Karol Węgrzycki. Please see the attached extended abstract for greater overview of our recent work. Contributed talk given by Henry Sinclair-Banks

Highlights Conference 2022 Conference Abstract

Coverability in 2-VASS with One Unary Counter

• Henry Sinclair-Banks

We study a particular reachability problem for vector addition systems with states (VASS), a well-studied class of infinite-state systems. The central problems are: the reachability problem, given two configurations, to decide whether you can reach one from the other one; and its relaxation the coverability problem. We consider the variant of 2-VASS where one counter is encoded in binary and the other in unary. Our main result is that the coverability problem for 2-VASS with one binary counter and one unary counter is in NP, an improvement upon the naively inherited PSPACE upper bound from coverability in binary 2-VASS. For our main technical contribution, we prove that every witnessing path can be modified to a path in a certain succinct linear form, that can then be guessed in NP.