Abstract
Seminal results establish that the coverability problem for Vector Addition Systems with States (VASS) is in EXPSPACE (Rackoff, '78) and is EXPSPACEhard 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^?(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 ddimensional unary VASS that are only witnessed by runs of length at least n^{2^Ω(d)}. Our first result closes this gap. We improve the upper bound by removing the twiceexponentiated log(d) factor, thus matching Lipton’s lower bound. This closes the corresponding gap for the exact space required to decide coverability. This also yields a deterministic n^{2^?(d)}time algorithm for coverability. Our second result is a matching lower bound, that there does not exist a deterministic n^{2^o(d)}time algorithm, conditioned upon the Exponential Time Hypothesis.
When analysing coverability, a standard proof technique is to consider VASS with bounded counters. Bounded VASS make for an interesting and popular model due to strong connections with timed automata. Withal, we study a natural setting where the counter bound is linear in the size of the VASS. Here the trivial exhaustive search algorithm runs in ?(n^{d+1})time. We give evidence to this being nearoptimal. We prove that in dimension one this trivial algorithm is conditionally optimal, by showing that n^{2o(1)}time is required under the kcycle hypothesis. In general fixed dimension d, we show that n^{d2o(1)}time is required under the 3uniform hyperclique hypothesis.
BibTeX  Entry
@InProceedings{kunnemann_et_al:LIPIcs.ICALP.2023.131,
author = {K\"{u}nnemann, Marvin and Mazowiecki, Filip and Sch\"{u}tze, Lia and SinclairBanks, Henry and W\k{e}grzycki, Karol},
title = {{Coverability in VASS Revisited: Improving Rackoff’s Bound to Obtain Conditional Optimality}},
booktitle = {50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
pages = {131:1131:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772785},
ISSN = {18688969},
year = {2023},
volume = {261},
editor = {Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18183},
URN = {urn:nbn:de:0030drops181834},
doi = {10.4230/LIPIcs.ICALP.2023.131},
annote = {Keywords: Vector Addition System, Coverability, Reachability, FineGrained Complexity, Exponential Time Hypothesis, kCycle Hypothesis, Hyperclique Hypothesis}
}
Keywords: 

Vector Addition System, Coverability, Reachability, FineGrained Complexity, Exponential Time Hypothesis, kCycle Hypothesis, Hyperclique Hypothesis 
Collection: 

50th International Colloquium on Automata, Languages, and Programming (ICALP 2023) 
Issue Date: 

2023 
Date of publication: 

05.07.2023 