Coverability in 2-VASS with One Unary Counter is in NP

TL;DR

This paper proves that the coverability problem in 2-VASS with one unary counter can be decided in NP, significantly improving the previous PSPACE upper bound and enabling more practical verification applications.

Contribution

The paper introduces a new NP algorithm for coverability in 2-VASS with one unary counter, advancing the understanding of restricted VASS models.

Findings

Coverability in 2-VASS with one unary counter is in NP.

Runs can be represented in a compressed linear form for decision procedures.

This result improves the complexity bound from PSPACE to NP.

Abstract

Coverability in Petri nets finds applications in verification of safety properties of reactive systems. We study coverability in the equivalent model: Vector Addition Systems with States (VASS). A k-VASS can be seen as k counters and a finite automaton whose transitions are labelled with k integers. Counter values are updated by adding the respective transition labels. A configuration in this system consists of a state and k counter values. Importantly, the counters are never allowed to take negative values. The coverability problem asks whether one can traverse the k-VASS from the initial configuration to a configuration with at least the counter values of the target. In a well-established line of work on k-VASS, coverability in 2-VASS is already PSPACE-hard when the integer updates are encoded in binary. This lower bound limits the practicality of applications, so it is natural to focus on restrictions. In this paper we initiate the study of 2-VASS with one unary counter. Here, one counter receives binary encoded updates and the other receives unary encoded updates. Our main result is that coverability in 2-VASS with one unary counter is in NP. This improves upon the inherited state-of-the-art PSPACE upper bound. Our main technical contribution is that one only needs to consider runs in a certain compressed linear form.