23.7 The time-complexity of coverability in unary 1-VASS

A 1-dimensional Vector Addition System with States (1-VASS) can be seen as an directed and integer weighted graph that is equipped with a non-negative integer counter. A configuration of a 1-VASS is a pair \((q, x)\) that is the current node \(q\) and the current non-negative counter value \(x\). A run in a 1-VASS is a sequence of configurations \((q_0, x_0), (q_1, x_1), \ldots, (q_k, x_k)\) where for each \(i \in \{ 1, \ldots, k\}\), there is an edge from \(x_{i-1}\) to \(x_i\) with weight \(x_i - x_{i-1}\). Let \(n\) the size of a 1-VASS, encoded in unary, that is the number of states plus the absolute value of all weights. The coverability problem asks whether there is a run from \((p, 0)\) to \((q, x)\) in \(\mathcal{V}\), where \(x \geq 0\); the input consists of a 1-VASS \(\mathcal{V}\), an initial state \(p\), and a target state \(q\). There is a straightforward \(\mathcal{O}(n^2)\)-time algorithm for coverability in 1-VASS.

Is there an \(o(n^2)\)-time algorithm for coverability in 1-VASS?