We are happy to present Henry Sinclair-Banks’s talk titled “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 is PSPACE-complete with two binary encoded counters and NL-complete with two unary encoded counters.

Our NP upper bound is achieved using new techniques and one of these techniques is shown in this presentation. Coverability in any 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 if the initial and target counter values are instead encoded in binary, then coverability in four-dimensional unary VASS is NP-hard and coverability in eight-dimensional unary VASS is PSPACE-hard. 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.

Henry Sinclair-Banks is a PhD student at the University of Warwick under the supervision of Dr. Dmitry Chistikov and Dr. Marcin Jurdzinski. Within theoretical computer science, the main themes of his research are automata, complexity, and logic. More specifically, the questions he most enjoys are all about automata with counters such as vector addition systems with states and one-counter nets.