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 that is the current node and the current non-negative counter value . A run in a 1-VASS is a sequence of configurations where for each , there is an edge from to with weight . Let 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 to in , where ; the input consists of a 1-VASS , an initial state , and a target state . There is a straightforward -time algorithm for coverability in 1-VASS. Is there an -time algorithm for coverability in 1-VASS?
