Coverability in VASS Revisited: Improving Rackoff’s Bounds to Obtain Conditional Optimality
Marvin Künnemann, Filip Mazowiecki, Lia Schütze, Henry Sinclair-Banks, Karol Węgrzycki · Journal of the ACM · 2025
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^{\mathcal {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)}}\) . 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^{\mathcal {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 \(\mathcal {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, for any fixed dimension d ≥ 4, we show that \(n^{d-2-o(1)}\) time is required under the 3-uniform hyperclique hypothesis.