A Note on the Parameterised Complexity of Coverability in Vector Addition Systems

TL;DR

The paper investigates the parameterised complexity of the coverability problem for vector addition systems (VAS), focusing on two natural parameters: the dimension $d$ and the size of the input encoding of $V$. It leverages Rackoff-type analyses and unary encodings to relate coverability to complexity classes, establishing an $XNL$-complete result for the unary-dimension parameterisation and clarifying ETH-based lower bounds. It also highlights open questions, notably whether fixed-parameter tractability holds when parameterising by $|V|$. The findings illuminate the boundaries of efficient algorithms for VAS coverability and guide future work on which parameters yield tractable regimes.

Abstract

We investigate the parameterised complexity of the classic coverability problem for vector addition systems (VAS): given a finite set of vectors $V \subseteq\mathbb{Z}^d$, an initial configuration $s\in\mathbb{N}^d$, and a target configuration $t\in\mathbb{N}^d$, decide whether starting from $s$, one can iteratively add vectors from $V$ to ultimately arrive at a configuration that is larger than or equal to $t$ on every coordinate, while not observing any negative value on any coordinate along the way. We consider two natural parameters for the problem: the dimension $d$ and the size of $V$, defined as the total bitsize of its encoding. We present several results charting the complexity of those two parameterisations, among which the highlight is that coverability for VAS parameterised by the dimension and with all the numbers in the input encoded in unary is complete for the class XNL under PL-reductions. We also discuss open problems in the topic, most notably the question about fixed-parameter tractability for the parameterisation by the size of $V$.