Coverability in 2-VASS with One Unary Counter


We study a particular reachability problem for vector addition systems with states (VASS), a well-studied class of infinite-state systems. The central problems are: the reachability problem, given two configurations, to decide whether you can reach one from the other one; and its relaxation the coverability problem. We consider the variant of 2-VASS where one counter is encoded in binary and the other in unary. Our main result is that the coverability problem for 2-VASS with one binary counter and one unary counter is in NP, an improvement upon the naively inherited PSPACE upper bound from coverability in binary 2-VASS. For our main technical contribution, we prove that every witnessing path can be modified to a path in a certain succinct linear form, that can then be guessed in NP.

MOVEP 2022

Henry Sinclair-Banks, 15/06/22, Aalborg Universitet (Denmark).