License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2023.131
URN: urn:nbn:de:0030-drops-181834
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18183/
Künnemann, Marvin ;
Mazowiecki, Filip ;
Schütze, Lia ;
Sinclair-Banks, Henry ;
Węgrzycki, Karol
Coverability in VASS Revisited: Improving Rackoff’s Bound to Obtain Conditional Optimality
Abstract
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^?(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 length at least n^{2^Ω(d)}. Our first result closes this gap. We improve the upper bound by removing the twice-exponentiated 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 near-optimal. We prove that in dimension one this trivial algorithm is conditionally optimal, by showing that n^{2-o(1)}-time is required under the k-cycle hypothesis. In general fixed dimension d, we show that n^{d-2-o(1)}-time is required under the 3-uniform 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 Sinclair-Banks, 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:1--131:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-278-5},
ISSN = {1868-8969},
year = {2023},
volume = {261},
editor = {Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18183},
URN = {urn:nbn:de:0030-drops-181834},
doi = {10.4230/LIPIcs.ICALP.2023.131},
annote = {Keywords: Vector Addition System, Coverability, Reachability, Fine-Grained Complexity, Exponential Time Hypothesis, k-Cycle Hypothesis, Hyperclique Hypothesis}
}
|
Keywords: |
|
Vector Addition System, Coverability, Reachability, Fine-Grained Complexity, Exponential Time Hypothesis, k-Cycle Hypothesis, Hyperclique Hypothesis |
|
Collection: |
|
50th International Colloquium on Automata, Languages, and Programming (ICALP 2023) |
|
Issue Date: |
|
2023 |
|
Date of publication: |
|
05.07.2023 |
