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

Speaker(s)

Filip Mazowiecki

Affiliation

University of Warsaw

Date

Oct. 4, 2023, 2:15 p.m.

Room

room 5050

Seminar

Seminar Automata Theory

---

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^{\Oh(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^{\Oh(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. There's also other stuff in the paper that I will not discuss. Joint work with Marvin Künnemann, Lia Schütze, Henry Sinclair-Banks, and Karol Węgrzycki <3.

---