The Complexity of Coverability in Fixed Dimension VASS with Various Encodings

This presentation is about the coverability problem for Vector Addition Systems with States (VASS). We have lately shown that coverability in two-dimensional VASS with one binary encoded counter and one unary encoded counter is in NP. For contrast, coverability in two-dimensional VASS with two binary encoded counters is PSPACE-complete. Our NP upper bound is achieved using new techniques and one of these techniques is shown in this presentation. Regardless of the dimension, coverability in fixed dimension unary VASS, that is when the counter updates are encoded in unary, is long-known to be NL-complete. In this variation of the problem, the initial and target counter values are also encoded in unary, this turns out to be of great importance. We have recently found that coverability in four-dimensional unary VASS is NP-hard and coverability in eight-dimensional unary VASS is PSPACE-hard, if the initial and target counter values are instead encoded in binary. These lower bounds are corollaries of recent results of the hardness of reachability in fixed dimension unary VASS, and this presentation will feature the technique used in the reductions to coverability.

OFCOURSE 2022

Henry Sinclair-Banks, 17/11/22, Max Planck Institute for Software Systems in Technische Universität Kaiserslautern (Germany).