单计数自动机中半线性目标集合的复杂度二分图

在许多无限状态系统中，覆盖可达性问题的复杂度显著低于可达性问题。为了描绘计算难度在覆盖可达性与可达性之间的边界，我们提出将这些问题置于更一般的上下文中，以便证明复杂度二分图。更一般的设置源于以下情况：对于覆盖问题，我们给定向量$t$，询问是否存在满足关系$x\ge t$的可达向量$x$。而对于可达性，我们希望满足关系$x=t$。在更一般的设置中，存在一个 Presburger 公式$\varphi(t,x)$，我们给定$t$，询问是否存在满足$\varphi(t,x)$的可达向量$x$。我们研究单计数系统和二进制更新的情形：（i）整数 VASS，（ii）Parikh 自动机，（iii）标准（非负）VASS。在每种情况下，可达性是 NP 完整的，但覆盖可达性已知在多项式时间内。在每种情况下，我们都给出三个二分图定理。我们显示，对于每个公式，问题要么是 NP 完整的，要么属于$\mathsf{AC}^1$，这是多项式时间内的电路复杂度类。我们还表明，给定公式落在二分图的哪一侧是可判定的。