The Library
Coverability in VASS revisited : improving Rackoff's Bound to Obtain Conditional Optimality
Tools
Künnemann, Marvin, Mazowiecki, Filip, Schütze, Lia, Sinclair-Banks, Henry and Wegrzycki, Karol (2023) Coverability in VASS revisited : improving Rackoff's Bound to Obtain Conditional Optimality. In: ICALP 2023 : 50th EATCS International Colloquium on Automata, Languages and Programming, Paderborn, Germany, 10-14 Jul 2023. Published in: Proceedings of ICALP 2023, 261 131:1-131:20. ISBN 9783959772785. doi:10.4230/LIPIcs.ICALP.2023.131 ISSN 1868-8969.
|
PDF
LIPIcs-ICALP-2023-131.pdf - Published Version - Requires a PDF viewer. Available under License Creative Commons Attribution 4.0. Download (1030Kb) | Preview |
|
PDF
WRAP-Coverability-VASS-revisited-improving-Rackoffs-bound-obtain-conditional-optimality-23.pdf - Accepted Version Embargoed item. Restricted access to Repository staff only - Requires a PDF viewer. Download (992Kb) |
Official URL: https://doi.org/10.4230/LIPIcs.ICALP.2023.131
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 n2O(dlogd), 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 n2Ω(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 n2O(d)-time algorithm for coverability. Our second result is a matching lower bound, that there does not exist a deterministic n2o(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 O(nd+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 n2−o(1)-time is required under the k-cycle hypothesis. In general fixed dimension d, we show that nd−2−o(1)-time is required under the 3-uniform hyperclique hypothesis.
Item Type: | Conference Item (Paper) | ||||||
---|---|---|---|---|---|---|---|
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||||
Journal or Publication Title: | Proceedings of ICALP 2023 | ||||||
Publisher: | Dagstuhl | ||||||
ISBN: | 9783959772785 | ||||||
ISSN: | 1868-8969 | ||||||
Official Date: | 2023 | ||||||
Dates: |
|
||||||
Volume: | 261 | ||||||
Page Range: | 131:1-131:20 | ||||||
DOI: | 10.4230/LIPIcs.ICALP.2023.131 | ||||||
Status: | Peer Reviewed | ||||||
Publication Status: | Published | ||||||
Access rights to Published version: | Open Access (Creative Commons) | ||||||
Date of first compliant deposit: | 17 May 2023 | ||||||
Date of first compliant Open Access: | 19 October 2023 | ||||||
Conference Paper Type: | Paper | ||||||
Title of Event: | ICALP 2023 : 50th EATCS International Colloquium on Automata, Languages and Programming | ||||||
Type of Event: | Conference | ||||||
Location of Event: | Paderborn, Germany | ||||||
Date(s) of Event: | 10-14 Jul 2023 | ||||||
Open Access Version: |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |
Downloads
Downloads per month over past year