半线性集与 Parikh 自动机的可分离性复杂度

在‘可分离性问题’中，我们给定两个集合 $K$ 和 $L$ 来自某个类别 $\mathcal{C}$，我们希望决定是否存在来自类别 $\mathcal{S}$ 的集合 $S$ 使得 $K\subseteq S$ 且 $S\cap L=\emptyset$。在这种情况下，我们称之为$\mathcal{C}$ 中集合由 $\mathcal{S}$ 中的集合可分离。我们研究了两种类型的可分离性问题。首先，我们考虑由量词-free 单一 Presburger 公式（或等价地，可识别的 $\mathbb{N}^d$ 的子集）定义的半线性集的可分离性。此处，公式是单一的，如果每个原子最多使用一个变量。其次，我们考虑由 Parikh 自动机的语言由正则语言可分离。Parikh 自动机是一个能够访问计数器的机器，计数器只能递增，并且在运行结束时必须满足半线性约束。这两种可分离性问题已知是可判定的，具有初等复杂度。我们的主要结果是这两种问题都是 coNP-完整的。在半线性集的情况下，coNP-完整性成立，无论输入集是由存在性 Presburger 公式、量词-free 公式，还是半线性表示指定。我们的结果意味着可识别的 $\Sigma^*\times\mathbb{N}^d$ 的有理子集的可分离性（Choffrut 和 Grigorieff 已证明可判定）也是 coNP-完整的。另一个应用是确定性 Parikh 自动机的正则性（目标集是用量词-free Presburger 公式指定的）也是 coNP-完整的。