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

TL;DR

This paper explores the parameterised complexity of the coverability problem in vector addition systems, revealing its complexity classification under various parameters and highlighting open questions about fixed-parameter tractability.

Contribution

It provides a detailed complexity analysis of coverability in VAS based on dimension and input size, including new completeness results for certain parameterisations.

Findings

Coverability with fixed dimension and unary encoding is XNL-complete.

The complexity varies significantly with parameters, highlighting the nuanced nature of the problem.

Open problems include fixed-parameter tractability for the size of V.

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