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.

翻译：带状态向量加法系统（VASS）是并发系统中的一种常用模型，然而许多决策问题因复杂性过高而难以处理。因此，考虑采用可更高效求解这些问题的过度近似语义学具有实用价值。本研究提出一种称为减量语义学的过度近似方法，该语义学对减量操作进行适度松弛：原向量加法系统的核心特征在于——执行减量操作时计数器必须为正值，而本文提出的语义学允许对零值计数器执行减量操作（执行后计数器保持零值）。研究发现，当仅对部分转移采用减量语义学（其余转移保持经典语义学）时，可达性问题将不可判定。但若全程采用减量语义学，可达性仍保持可判定性。具体而言，采用减量语义学的VASS可达性问题难度与经典VASS相同（即阿克曼级难度），而零配置可达性与覆盖性问题则复杂度降低（分别达到EXPSPACE完全与NP完全）。本文系统分析了减量语义学下一般可达性、零配置可达性及覆盖性问题的复杂度，涵盖一般VASS、二维VASS及一维VASS场景，并考虑了计数器的单元更新与二进制更新两种情况。