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). 
91¸ŁŔű 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).