Monus semantics in vector addition systems with states

TL;DR

This paper introduces monus semantics for vector addition systems with states, allowing zero-valued counters to be decremented without changing their value, and analyzes the resulting decision problem complexities.

Contribution

It presents a novel overapproximation called monus semantics for VASS, maintaining decidability of reachability and characterizing its complexity across various cases.

Findings

Reachability under monus semantics is Ackermann-hard, same as classical VASS.

Zero-reachability is EXPSPACE-complete.

Coverability is NP-complete.

Abstract

Vector addition systems with states (VASS) are a popular model for concurrent systems. However, many decision problems have prohibitively high complexity. Therefore, it is sometimes useful to consider overapproximating semantics in which these problems can be decided more efficiently. We study an overapproximation, called monus semantics, that slightly relaxes the semantics of decrements: A key property of a vector addition systems is that in order to decrement a counter, this counter must have a positive value. In contrast, our semantics allows decrements of zero-valued counters: If such a transition is executed, the counter just remains zero. It turns out that if only a subset of transitions is used with monus semantics (and the others with classical semantics), then reachability is undecidable. However, we show that if monus semantics is used throughout, reachability remains decidable. In particular, we show that reachability for VASS with monus semantics is as hard as that of classical VASS (i.e. Ackermann-hard), while the zero-reachability and coverability are easier (i.e. EXPSPACE-complete and NP-complete, respectively). We provide a comprehensive account of the complexity of the general reachability problem, reachability of zero configurations, and coverability under monus semantics. We study these problems in general VASS, two-dimensional VASS, and one-dimensional VASS, with unary and binary counter updates.