> Details

Künnemann, Marvin [Author]; Mazowiecki, Filip [Author]; Schütze, Lia [Author]; Sinclair-Banks, Henry [Author]; Węgrzycki, Karol [Author] ; Marvin Künnemann and Filip Mazowiecki and Lia Schütze and Henry Sinclair-Banks and Karol Węgrzycki [Contributor]

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

Reference
management

Bookmarks

Remove from
bookmarks

Share this on Whatsapp

Close

Bookmarks



You can manage bookmarks using lists, please log in to your user account for this.
  • Media type: Text; E-Article; Electronic Conference Proceeding
  • Title: Coverability in VASS Revisited: Improving Rackoff’s Bound to Obtain Conditional Optimality
  • Contributor: Künnemann, Marvin [Author]; Mazowiecki, Filip [Author]; Schütze, Lia [Author]; Sinclair-Banks, Henry [Author]; Węgrzycki, Karol [Author]
  • Published: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023
  • Language: English
  • DOI: https://doi.org/10.4230/LIPIcs.ICALP.2023.131
  • Keywords: k-Cycle Hypothesis ; Exponential Time Hypothesis ; Fine-Grained Complexity ; Vector Addition System ; Reachability ; Coverability ; Hyperclique Hypothesis
  • Origination:
  • Footnote: Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
  • Description: 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.
  • Access State: Open Access