The complexity of separability for semilinear sets and Parikh automata

In a \emph{separability problem}, we are given two sets $K$ and $L$ from a class $\mathcal{C}$, and we want to decide whether there exists a set $S$ from a class $\mathcal{S}$ such that $K\subseteq S$ and $S\cap L=\emptyset$. In this case, we speak of \emph{separability of sets in $\mathcal{C}$ by sets in $\mathcal{S}$}. We study two types of separability problems. First, we consider separability of semilinear sets (i.e. subsets of $\mathbb{N}^d$ for some $d$) by sets definable by quantifier-free monadic Presburger formulas (or equivalently, the recognizable subsets of $\mathbb{N}^d$). Here, a formula is monadic if each atom uses at most one variable. Second, we consider separability of languages of Parikh automata by regular languages. A Parikh automaton is a machine with access to counters that can only be incremented, and have to meet a semilinear constraint at the end of the run. Both of these separability problems are known to be decidable with elementary complexity. Our main results are that both problems are coNP-complete. In the case of semilinear sets, coNP-completeness holds regardless of whether the input sets are specified by existential Presburger formulas, quantifier-free formulas, or semilinear representations. Our results imply that recognizable separability of rational subsets of $\Sigma^*\times\mathbb{N}^d$ (shown decidable by Choffrut and Grigorieff) is coNP-complete as well. Another application is that regularity of deterministic Parikh automata (where the target set is specified using a quantifier-free Presburger formula) is coNP-complete as well.