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

Vector Addition Systems with States (VASS) are a long-studied model that are equivalent to Petri nets. The coverability problem asks whether there exists a run from a given initial configuration to a configuration that is at least a given target configuration. Coverability is in EXPSPACE (Rackoff '78) and is EXPSPACE-hard already under unary encodings (Lipton '76). Rackoff's upper bound is derived by considering the necessary length of runs that witness coverability. In this presentation, I will present an improved upper bound on the lengths of such runs. The run length bound can be used to obtain two algorithms: an optimal exponential space algorithm and a conditionally optimal double-exponential time algorithm. I aim to show the double-exponential time lower bound that is conditioned upon the Exponential Time Hypothesis (ETH). 
About joint work with Marvin Künnemann, Filip Mazowiecki, Lia Schütze, and Karol Węgrzycki (ICALP’23).

IRIF Verification Seminar, https://www.irif.fr/en/seminaires/verif/index

Henry Sinclair-Banks, 08/01/24, IRIF, Université Paris Cité (France).