Speaker
Description
Marvin Künnemann, Filip Mazowiecki, Lia Schütze, Henry Sinclair-Banks and Karol Węgrzycki
Best Paper Track B:
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^(O(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^(Omega(d))).
The remaining gap was stated as an open problem in '82 by Mayr and Meyer and remained open until now.
Our first result closes this gap.
We improve Rackoff's upper bound, 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^(O(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 O(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.