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同样困难（即Ackermann-hard），而零可达性与覆盖性则更易处理（分别为EXPSPACE完全和NP完全）。我们提供了关于一般可达性问题、零配置可达性以及在莫努斯语义下覆盖性的复杂性全面分析。我们在一般VASS、二维VASS和一维VASS中研究了这些问题，并考虑了计数器的单进和二进制更新方式。