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).

LaBRI Formal Method Seminar (M2F), https://mf.labri.fr

Henry Sinclair-Banks, 07/11/23, Université de Bordeaux (France).