Coverability in VASS Revisited: Improving Rackoff’s Bounds to Obtain Conditional Optimaility

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 double-exponential length that is at least n^(2^[Omega(d)]). In this presentation, I will outline how to carefully strengthen Rackoff's approach to improve the upper bound to show that if coverability holds then there exists a run of length at most n^(2^[O(d)]). Moreover, we therefore obtain an optimal 2^(O[d])*log(n)-space algorithm for coverability. This closes a forty-one-year-old gap that was stated as an open problem by Mayr and Meyer. Furthermore, we obtain a deterministic n^(2^[O(d)])-time algorithm for coverability in unary d-VASS. We show that this is optimal under the Exponential Time Hypothesis, in particular by leveraging the time required to detect a clique in a graph. I also plan to present the approach and techniques used in our reduction from finding cliques in graphs to coverability in unary VASS. Ultimately, this yields a conditional matching lower bound that coverability in unary d-VASS requires n^(2^[Omega(d)])-time. This presentation concerns ongoing joint work with Marvin Künnemann, Filip Mazowiecki, Lia Schütze, and Karol Węgrzycki.

Highlights of Logic, Games and Automata 2023

Henry Sinclair-Banks, 26/07/23, Universität Kassel (Germany).