Coverability in VASS Revisited: Improving Rackoff’s Bound to Obtain Conditional Optimality

Medientyp: Sonstige Veröffentlichung; E-Artikel; Elektronischer Konferenzbericht

Titel: Coverability in VASS Revisited: Improving Rackoff’s Bound to Obtain Conditional Optimality

Beteiligte: Künnemann, Marvin [Verfasser:in]; Mazowiecki, Filip [Verfasser:in]; Schütze, Lia [Verfasser:in]; Sinclair-Banks, Henry [Verfasser:in]; Węgrzycki, Karol [Verfasser:in]

Erschienen: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023

Sprache: Englisch

DOI: https://doi.org/10.4230/LIPIcs.ICALP.2023.131

Schlagwörter: k-Cycle Hypothesis ; Exponential Time Hypothesis ; Fine-Grained Complexity ; Vector Addition System ; Reachability ; Coverability ; Hyperclique Hypothesis

Entstehung:

Anmerkungen: Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.

Beschreibung: 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.

Zugangsstatus: Freier Zugang

Nur in Feld suchen:

Zuletzt gesuchte Begriffe: