带不相等测试的一计数器自动机的不变量

我们研究了带不相等测试的一计数器自动机的可达性问题，其中不相等测试是一种禁止指定计数器值的守卫。已知该可达性问题属于NP难且属于PSPACE，其计算复杂度的刻画被Almagor、Cohen、P\'erez、Shirmohammadi和Worrell（2020）留作一个具有挑战性的开放问题。我们缩小了复杂度差距，将该问题置于多项式层次结构的第二层，即类$\mathsf{coNP}^{\mathsf{NP}}$。在同时存在相等和不相等测试的情况下，我们的上界位于第三层，即类$\mathsf{P}^{\mathsf{NP}^{\mathsf{NP}}}$。为了证明这一结果，我们表明不可达性可以由一对不变量（前向和后向）来证明。这些不变量几乎是归纳的。它们旨在仅近似可达性集合的“核心”而非整个集合。这些不变量也是“泄漏的”：有可能逃出该集合。我们通过单独的检查来补充这一点，因为泄漏只能以受控方式发生。