@unpublished{warwick189757,
    year = {2024},
    school = {University of Warwick},
    note = {Unpublished},
    title = {On the complexity of reachability problems in counter systems},
    month = {June},
    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 a 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 of the traversed edges. In this thesis, we examine two important decision problems for VASS: reachability which asks if there is a run to a target configuration, and coverability which asks if there is a run to a configuration that exceeds the target. These two decision problems can express various verification problems including liveness and safety of concurrent systems.

We examine the complexity of reachability and coverability in VASS with a host of extensions and restrictions. One of the main results in this thesis is an optimal double-exponential upper bound on the length of runs for coverability, which resolves an open problem stated by Mayr and Meyer in 1982. This bound yield an exponential space algorithm that is optimal up to multiplicative constants in the exponent. We also prove that reachability in unary three-dimensional linear path schemes is NP-complete; this closes a line of research on reachability in flat VASS and answers open questions asked by Englert, Lazi{\'c}, and Totzke in 2016 and Leroux in 2021. Furthermore, we improve the upper bounds for reachability in binary 1-VASS with disequality tests and coverability in 2-VASS with one unary counter.

In the latter parts of this thesis we study reachability and coverability in Petri nets that are extended to have resets but are restricted to being acyclic. In addition to studying reachability problems, we also study properties pertaining to languages of counter nets, the automata analogue of VASS.},
    url = {http://webcat.warwick.ac.uk/record=b4079247},
    author = {Sinclair-Banks, Henry},
    date-added = {2026-3-15 9:45:29 +0100}
}

We examine the complexity of reachability and coverability in VASS with a host of extensions and restrictions. One of the main results in this thesis is an optimal double-exponential upper bound on the length of runs for coverability, which resolves an open problem stated by Mayr and Meyer in 1982. This bound yield an exponential space algorithm that is optimal up to multiplicative constants in the exponent. We also prove that reachability in unary three-dimensional linear path schemes is NP-complete; this closes a line of research on reachability in flat VASS and answers open questions asked by Englert, Lazi{\'c}, and Totzke in 2016 and Leroux in 2021. Furthermore, we improve the upper bounds for reachability in binary 1-VASS with disequality tests and coverability in 2-VASS with one unary counter.

In the latter parts of this thesis we study reachability and coverability in Petri nets that are extended to have resets but are restricted to being acyclic. In addition to studying reachability problems, we also study properties pertaining to languages of counter nets, the automata analogue of VASS.},
    url = {http://webcat.warwick.ac.uk/record=b4079247},
    author = {Sinclair-Banks, Henry},
    date-added = {2026-3-15 9:45:29 +0100}
}</bib>