The Complexity of Separability for Semilinear Sets and Parikh Automata

In a separability problem, we are given two sets $K$ and $L$ from a class $𝒞$, and we want to decide whether there exists a set $S$ from a class $𝒮$ such that $K\subseteq S$ and $S\cap L=\mathrm{\varnothing }$. Here, the sets in $𝒮$ are the admissible separators, and $S$ is said to separate the sets $K$ and $L$. In the case where $𝒞$ is a class of non-regular languages and $𝒮$ is the class of regular languages, then the problem is called regular separability (problem) for $𝒞$. While the problem turned out to be undecidable for context-free languages in the 1970s [47, 34], the last decade saw a significant amount of attention on regular separability for subclasses (or variants) of vector addition systems with states (VASS). Regular separability was studied for coverability languages of VASS (and, more generally, well-structured transition systems) [18, 38, 41], one-counter automata and one-dimensional VASS [17], Parikh automata [15], commutative VASS languages [16], concerning its relationship with the intersection problem [48], Büchi VASS [2, 3], and also for settings where one input language is an arbitrary VASS and the other is from some subclass [19]. Recently, this line of work culminated in the breakthrough result that regular separability for general VASS languages is decidable and Ackermann-complete [39]. However, for subclasses of VASS languages, the complexity landscape is far from understood.

An important example of such a subclass is the class of languages accepted by Parikh automata, which are non-deterministic automata equipped with counters that can only be incremented. Here, a run is accepting if the final counter values belong to a particular semilinear set. Languages of Parikh automata have received significant attention over many decades [35, 26, 1, 37, 9, 7, 10, 23, 5, 51, 12, 52], including a lot of work in recent years [20, 29, 22, 27, 11, 46]. This is because they are expressive enough to model non-trivial counting behavior, but still enjoy low complexity for many algorithmic tasks (e.g. the emptiness problem is $\mathrm{𝖼𝗈𝖭𝖯}$-complete). Example applications are monadic second-order logic with cardinalities [40] (this paper introduced the specific model of Parikh automata), solving subword constraints [33], and model-checking FIFO channel systems [8]. Moreover, these languages have other equivalent characterizations, such as reversal-bounded counter automata – a classic (and intensely studied) type of infinite-state systems with nice decidability properties [35, 5] – and automata with $\mathbb{Z}$-counters, also called $\mathbb{Z}$-VASS [26, 30]¹¹1See [1] for efficient translation among Parikh automata, reversal-bounded counter automata, and $\mathbb{Z}$-VASS..

Decidability of regular separability was shown by Clemente, Czerwiński, Lasota, and Paperman [15] in 2017 as one of the first decidability results for regular separability. Moreover, this result was a key ingredient in Keskin and Meyer’s algorithm to decide regular separability for general VASS [39]. However, despite the strong interest in Parikh automata and in regular separability, the complexity of this problem remained unknown. In [15, Section 7], the authors provide an elementary complexity upper bound.

One of the steps in the algorithm from [15] is to decide separability of sets defined in Presburger arithmetic, the first-order theory of $(\mathbb{N};+,\le ,0,1)$. Separators of logically defined sets can also be viewed as interpolants. If $\phi (𝒙,𝒚)$ and $\psi (𝒚,𝒛)$ are (first-order or propositional) formulas such that $\forall 𝒙\forall 𝒚\forall 𝒛(\phi (𝒙,𝒚)\to \psi (𝒚,𝒛))$ holds, then a formula $\chi (𝒚)$ is a Craig interpolant if $\forall 𝒙\forall 𝒚(\phi (𝒙,𝒚)\to \chi (𝒚))$ and $\forall 𝒚\forall 𝒛(\chi (𝒚)\to \psi (𝒚,𝒛))$ both hold. Here, $𝒙,𝒚,𝒛$ are each a vector of variables, meaning $\chi$ only mentions variables that occur both in $\phi$ and $\psi$. Equivalently, the set defined by $\chi$ is a separator of the sets defined by the existential formulas $\exists 𝒙:\phi (𝒙,𝒚)$ and $\exists 𝒛:\neg \psi (𝒚,𝒛)$. In Interpolation-Based Model Checking (ITP) [43, 50], Craig interpolants are used to safely overapproximate sets of states: If $\phi$ describes reachable states and $\psi$ describes the set of safe states, then $\chi$ overapproximates $\phi$ without adding unsafe states. Note that in Presburger logic there are implications that do not have a Craig interpolant (this is in contrast to propositional logic). So, before constructing an interpolant, a first step of ITP is to decide whether there even exists such an interpolant.

In the case of Presburger arithmetic, the definable sets are the semilinear sets. For many infinite-state systems, the step relation (or even the reachability relation) is semilinear, and thus, separators can play the role of Craig interpolants in infinite-state model checking. For the separators, a natural choice is the class of recognizable sets, which are those defined by monadic Presburger formulas, meaning each atom refers to at most one variable. Monadic formulas have recently received attention [49, 4, 32, 31] because of their applications in query optimization in constraint databases [28, 42] and symbolic automata [49]. Thus, deciding recognizable separability of semilinear sets can be viewed as synthesizing monadic Craig interpolants.

Recognizable separability was shown decidable by Choffrut and Grigorieff [14] (see [16] for an extension beyond semilinear sets). This was a key ingredient for separability of Parikh automata in [15]. Choffrut and Grigorieff’s algorithm has elementary complexity [15, Section 7], but the exact complexity of recognizable separability of semilinear sets remained unknown.

Our first main result is that for given existential Presburger formulas, recognizable separability (i.e. monadic separability) is $\mathrm{𝖼𝗈𝖭𝖯}$-complete. In particular, recognizable separability is $\mathrm{𝖼𝗈𝖭𝖯}$-complete for given semilinear representations. Moreover, our result implies that recognizable separability is $\mathrm{𝖼𝗈𝖭𝖯}$-complete for rational subsets of monoids ${\mathrm{\Sigma }}^{\ast }\times {\mathbb{N}}^d$ as considered by Choffrut and Grigorieff [14]. Building on the methods of the first result, our second main result is that regular separability for Parikh automata is $\mathrm{𝖼𝗈𝖭𝖯}$-complete.

Our first main result strengthens a recent result on monadic decomposability. A formula in Presburger arithmetic is monadically decomposable if it has a monadic equivalent. It was shown recently that (i) deciding whether a given quantifier-free formula is monadically decomposable (i.e. whether it has a monadic equivalent) is $\mathrm{𝖼𝗈𝖭𝖯}$-complete [32, Theorem 1] (see [4, Corollary 8.1] for an alternative proof; and see [13, Proposition 3] for improved bounds for the approach in [32]), whereas (ii) for existential formulas, the problem is $\mathrm{𝖼𝗈𝖭𝖤𝖷𝖯}$-complete [31, Corollary 3.6]. Our first main result strengthens (i): If $\phi (𝒙)$ is a quantifier-free formula, then the sets defined by $\phi (𝒙)$ and $\neg \phi (𝒙)$ are separable by a monadic formula if and only if $\phi (𝒙)$ is monadically decomposable. Perhaps surprisingly, our $\mathrm{𝖼𝗈𝖭𝖯}$ upper bound still holds for existential Presburger formulas, for which monadic decomposability is known to be $\mathrm{𝖼𝗈𝖭𝖤𝖷𝖯}$-complete²²2This is not a contradiction to the above reduction from monadic decomposability to recognizable separation, since this reduction would require complementing an existential formula..

Another consequence of our results is that regularity of deterministic Parikh automata, i.e. deciding whether a given deterministic Parikh automaton accepts a regular language, is $\mathrm{𝖼𝗈𝖭𝖯}$-complete: Given a deterministic Parikh automaton for a language $L\subseteq {\mathrm{\Sigma }}^{\ast }$, one can construct in polynomial time a Parikh automaton for $K={\mathrm{\Sigma }}^{\ast }\setminus L$. Then, $L$ is regular if and only if $L$ and $K$ are regularly separable. Here, we assume that the semilinear target set is given as a quantifier-free Presburger formula. Decidability of this problem has been shown by Cadilhac, Finkel, and McKenzie [10, Theorem 25] (even in the more general case of unambiguous constrained automata).

The existing elementary-complexity algorithm for recognizable separability of semilinear sets works with semilinear representations and distinguishes two cases: If in one component $j$, one of the input sets $S_1,S_2\subseteq {\mathbb{N}}^d$ is bounded by some $b\ge 0$, then it considers each $x\in [0,b]$ and recursively decides separability of $S_1[j\mapsto x]$ and $S_2[j\mapsto x]$, where $S_i[j\mapsto x]$ is just $S_i$ restricted to having $x$ in this bounded component. If, however, all components in both sets are unbounded, then it checks feasibility of a system of linear Diophantine equations. This approach leads to repeated intersection of semilinear sets, and thus exponential time. We provide a characterization (Proposition 4.5) that describes inseparability directly as the non-empty intersection of two semilinear sets ${\widehat{S}}_1,{\widehat{S}}_2\subseteq {\mathbb{N}}^d$ associated with $S_1,S_2$. This easily yields an $\mathrm{𝖭𝖯}$ procedure for inseparability, even if the input sets are given as existential Presburger formulas.

This characterization is then the first key ingredient for deciding regular separability of Parikh automata in $\mathrm{𝖼𝗈𝖭𝖯}$. This is because in [15], it is shown that, after some preprocessing, the languages of Parikh automata ${𝒜}_1$ and ${𝒜}_2$ are separable if and only if two semilinear sets $C_1,C_2\subseteq {\mathbb{N}}^d$ associated with ${𝒜}_1$ and ${𝒜}_2$ are separable by a recognizable set. These semilinear sets consist of vectors, each of which counts for some run of ${𝒜}_i$, how many times each simple cycles occurs in this run. Thus, our first result tells us that it suffices to decide whether ${\widehat{C}}_1$ and ${\widehat{C}}_2$ are disjoint. Unfortunately, the vectors of $C_1,C_2$ have exponential dimension $d$, since there are exponentially many simple cycles in each ${𝒜}_i$. Thus, applying our first result directly using existential Presburger arithmetic would only yield a $\mathrm{𝖼𝗈𝖭𝖤𝖷𝖯}$ upper bound.

To avoid this blowup, the second key idea is to encode the vectors in ${\widehat{C}}_1$ and ${\widehat{C}}_2$ as words, where the cycle occurrences appear as a concatenation in some order. By constructing $\mathbb{Z}$-VASS ${𝒲}_1,{𝒲}_2$ for the encodings of the vectors in ${\widehat{C}}_1,{\widehat{C}}_2$, we reduce separability to intersection emptiness of ${𝒲}_1$ and ${𝒲}_2$. The latter, in turn, easily reduces to non-reachability in a product $\mathbb{Z}$-VASS, which is in $\mathrm{𝖼𝗈𝖭𝖯}$.

A set $S\subseteq {\mathbb{N}}^d$ is linear if there is a vector $𝒖\in {\mathbb{N}}^d$ and a finite set $P\subseteq {\mathbb{N}}^d$ of so-called periods such that $S=𝒖+P^{\ast }$ holds. Here, for $P=\{{𝒖}_1,\mathrm{\dots },{𝒖}_n\}$, the set $P^{\ast }$ is defined as $P^{\ast }=\{{\lambda }_1{𝒖}_1+\mathrm{\cdots }+{\lambda }_n{𝒖}_n\mid {\lambda }_1,\mathrm{\dots },{\lambda }_n\in \mathbb{N}\}.$ A subset $S\subseteq {\mathbb{N}}^d$ is called semilinear if it is a finite union of linear sets. In case we specify $S$ by way of a finite union of linear sets, then we call this description a semilinear representation. The set $S\subseteq {\mathbb{N}}^d$ is called hyperlinear if there are finite sets $B,P\subseteq {\mathbb{N}}^d$ such that $S=B+P^{\ast }$ holds. It is well known that the semilinear sets are precisely those definable in Presburger arithmetic [25], the first-order theory of the structure $(\mathbb{N};+,\le ,0,1,{({\equiv }_m)}_{m\in \mathbb{N}\setminus \{0\}})$. Here ${\equiv }_m$ is the predicate where $x{\equiv }_{m}y$ if and only if $x-y$ is divisible by $m$. By quantifier elimination, every formula in Presburger arithmetic has a quantifier-free equivalent.

Intuitively, a Parikh automaton has finitely many control states and access to $d\ge 0$ counters. Upon reading a letter (or the empty word), it can add a vector $𝒖\in {\mathbb{N}}^d$ to its counters. Moreover, for each state $q\in Q$, it specifies a target set $C_q\subseteq {\mathbb{N}}^d$. An input word is accepted if at the end of the run, the accumulated counter values belong to $C_q$, where $q$ is the state at the end of the run. Formally, a Parikh automaton is a tuple $𝒜=(Q,\mathrm{\Sigma },T,q_0,{(C_q)}_{q\in Q})$, where $Q$ is a finite set of states, $T\subseteq Q\times (\mathrm{\Sigma }\cup \{\epsilon \})\times {\mathbb{N}}^d\times Q$ is its finite set of transitions, $q_0\in Q$ is the initial state, and $C_q\subseteq {\mathbb{N}}^d$ is the target set in state $q$, for each $q\in Q$. For an input word $w\in {\mathrm{\Sigma }}^{\ast }$, a run on $w$ is a sequence $(q_0,w_1,{𝒖}_1,q_1)\mathrm{\cdots }(q_{n-1},w_n,{𝒖}_n,q_n)$ of transitions in $T$ with $w=w_1\mathrm{\cdots }{w}_n$. The run is accepting if ${𝒖}_1+\mathrm{\cdots }+{𝒖}_n\in C_{q_n}$. The language of $𝒜$ is then the set of all words $w\in {\mathrm{\Sigma }}^{\ast }$ such that $𝒜$ has an accepting run on $w$.

A subset $L\subseteq M$ of a monoid $M$ is recognizable if there is a morphism $\phi :M\to F$ into some finite monoid $F$ such that ${\phi }^{-1}(\phi (L))=L$. The recognizable subsets of $M$ form a Boolean algebra [6, Chapter III, Prop. 1.1]. We say that sets $K,L\subseteq M$ are (recognizably) separable, denoted $K|L$, if there is a morphism $\phi :M\to F$ into some finite monoid $F$ such that $\phi (K)\cap \phi (L)=\mathrm{\varnothing }$. Equivalently, we have $K|L$ if and only if there is a recognizable $S\subseteq M$ with $K\subseteq S$ and $S\cap L=\mathrm{\varnothing }$. Here, $S$ is called a separator of $K$ and $L$. Clearly, we have $K|L$ if and only if $L|K$: if $S$ is a separator of $K$ and $L$ then $M\setminus S$ separates $L$ and $K$.

In the case $M={\mathrm{\Sigma }}^{\ast }$ for some alphabet $\mathrm{\Sigma }$, the recognizable sets in ${\mathrm{\Sigma }}^{\ast }$ are exactly the regular languages (cf. [44, Theorem II.2.1]), and thus we speak of regular separability. In the case $M={\mathbb{N}}^d$ for some $d\ge 0$, then the recognizable subsets of ${\mathbb{N}}^d$ are precisely the finite unions of cartesian products $U_1\times \mathrm{\cdots }\times U_d$, where each $U_i\subseteq \mathbb{N}$ is ultimately periodic [6, Theorem 5.1]. Here, a set $U\subseteq \mathbb{N}$ is ultimately periodic if there are $n_0,p\in \mathbb{N}\setminus \{0\}$ such that for all $n\ge n_0$, we have $n\in U$ if and only if $n+p\in U$. This implies that the recognizable subsets of ${\mathbb{N}}^d$ are precisely those definable by a monadic Presburger formula, i.e. one where every atom only refers to one variable [49]. For these reasons, in the case of $M={\mathbb{N}}^d$, we also sometimes speak of monadic separability.

In a recognizable separability problem, we are given two subsets $K$ and $L$ from a monoid $M$ as input, and we want to decide whether $K$ and $L$ are recognizably separable. Again, in the case of $M={\mathrm{\Sigma }}^{\ast }$, we also call this the regular separability problem.

Our first main result is the following.

The lower bound follows with a simple reduction from the emptiness problem for sets defined by existential Presburger formulas: If $\phi$ defines a subset $K\subseteq {\mathbb{N}}^d$, then $K|{\mathbb{N}}^d$ if and only if $K$ is empty. We prove the $\mathrm{𝖼𝗈𝖭𝖯}$ upper bound in Section 5. By the same argument, recognizable separability is $\mathrm{𝖼𝗈𝖭𝖯}$-hard for input sets given by quantifier-free formulas. Thus:

In particular, this re-proves the $\mathrm{𝖼𝗈𝖭𝖯}$ upper bound for monadic decomposability of quantifier-free formulas, as originally shown by Hague, Lin, Rümmer, and Wu [32, Theorem 1].

Since for a given semilinear representation of a set $S\subseteq {\mathbb{N}}^d$, it is easy to construct an existential Presburger formula defining $S$, Theorem 3.1 also implies the following.

In this case, the $\mathrm{𝖼𝗈𝖭𝖯}$ lower bound comes from the $\mathrm{𝖭𝖯}$-hard membership problem for semilinear sets (even if all numbers are written in unary) [36, Lemma 10]: For a semilinear subset $S\subseteq {\mathbb{N}}^d$ and a vector $𝒖\in {\mathbb{N}}^d$, we have $𝒖\notin S$ if and only if $S|\{𝒖\}$. Finally, Theorem 3.1 allows us to settle the complexity of recognizable separability of rational subsets of ${\mathrm{\Sigma }}^{\ast }\times {\mathbb{N}}^d$.

Decidability was first shown by Choffrut and Grigorieff [14, Theorem 1]. The $\mathrm{𝖼𝗈𝖭𝖯}$ upper bound follows because Choffrut and Grigorieff [14, Theorem 10] reduce recognizable separability of subsets of ${\mathrm{\Sigma }}^{\ast }\times {\mathbb{N}}^d$ to recognizable separability of rational subsets of ${\mathbb{N}}^{2d}$ (and their reduction is clearly in polynomial time). Moreover, for a given rational subset of ${\mathbb{N}}^{2d}$, one can construct in polynomial time an equivalent existential Presburger formula [45, Theorem 1]. Thus, the upper bound follows from Theorem 3.1. Since semilinear sets in ${\mathbb{N}}^d$ (given by a semilinear representation) can be viewed as rational subsets of ${\mathbb{N}}^d$ (and hence of ${\mathrm{\Sigma }}^{\ast }\times {\mathbb{N}}^d$), the $\mathrm{𝖼𝗈𝖭𝖯}$ lower bound is inherited from Corollary 3.4.

Our second main result is the following:

The $\mathrm{𝖼𝗈𝖭𝖯}$ lower bound comes via the $\mathrm{𝖼𝗈𝖭𝖯}$-complete emptiness problem: For a given Parikh automaton accepting a language $K\subseteq {\mathrm{\Sigma }}^{\ast }$, we have $K|{\mathrm{\Sigma }}^{\ast }$ if and only if $K=\mathrm{\varnothing }$. Thus, the interesting part is the upper bound, which we prove in Section 6. This is a significant improvement to the previously known elementary (or finitely iterated exponential time) complexity upper bound by Clemente, Czerwiński, Lasota, and Paperman [15].

Theorem 3.6 can also be applied to deciding regularity of deterministic Parikh automata.

Decidability of regularity was shown by Cadilhac, Finkel, and McKenzie [10, Theorem 25] (in the slightly more general setting of unambiguous constrained automata). For the $\mathrm{𝖼𝗈𝖭𝖯}$ upper bound, note that for a language $L\subseteq {\mathrm{\Sigma }}^{\ast }$ given by a deterministic Parikh automaton (with quantifier-free formulas for the target sets), one can in polynomial time construct the same type of automaton for the complement ${\mathrm{\Sigma }}^{\ast }\setminus L$. Since $L$ is regular if and only if $L$ and ${\mathrm{\Sigma }}^{\ast }\setminus L$ are separable by a regular language, we can invoke Theorem 3.6. The $\mathrm{𝖼𝗈𝖭𝖯}$ lower bound is inherited from monadic decomposability of quantifier-free formulas. Indeed, given a quantifier-free Presburger formula $\phi (x_1,\mathrm{\dots },x_n)$ with free variables $(x_1,\mathrm{\dots },x_n)$, one easily constructs a deterministic Parikh automaton (with quantifier-free target sets) for the language $L_{\phi }=\{a_1^{x_1}\mathrm{\cdots }{a}_n^{x_n}\mid \phi (x_1,\mathrm{\dots },x_n)\}$. As shown by Ginsburg and Spanier [24, Theorem 1.2], $L_{\phi }$ is regular if and only if $\phi$ is monadically decomposable. However, monadic decomposability for quantifier-free formulas is $\mathrm{𝖼𝗈𝖭𝖯}$-complete [32, Theorem 1].

For the $\mathrm{𝖼𝗈𝖭𝖯}$ upper bound in Corollary 3.7, we cannot drop the assumption that the formula be quantifier-free. This is because if the target sets can be existential Presburger formulas, then the regularity problem is $\mathrm{𝖼𝗈𝖭𝖤𝖷𝖯}$-hard. This follows by the same reduction from monadic decomposability: If we construct $L_{\phi }$ as above using an existential formula $\phi$, then again, $L_{\phi }$ is regular if and only if $\phi$ is monadically decomposable. Moreover, monadic decomposability for existential formulas is $\mathrm{𝖼𝗈𝖭𝖤𝖷𝖯}$-complete [31, Corollary 3.6].

Our notion applies, slightly more generally, to hyperlinear sets. Hence, let $R=A+U^{\ast }\subseteq {\mathbb{N}}^d$ and $S=B+V^{\ast }\subseteq {\mathbb{N}}^d$ be two hyperlinear sets where $A,B,U,V\subseteq {\mathbb{N}}^d$ are finite sets.

Hence, intuitively, twin-unbounded coordinates are those that can be made large/driven up in $R$ in the same way as in $S$. There is yet another characterization of twin-unbounded coordinates. Let $j\in [1,d]$. We say the $j$-th coordinate of the hyperlinear set $S=B+V^{\ast }$ is bounded if there is no period vector in $V$ with support on $j$, i.e., $j\notin \mathrm{supp}(𝒑)$ for all $𝒑\in V$. We say that a subset $J\subseteq [1,d]$ of coordinates is bounded in $S$ if each $j\in J$ is bounded in $S$. Consider the following process: Given two hyperlinear sets $R$ and $S$. We modify $R$ and $S$ by performing each of the following three steps for each coordinate $j\in [1,d]$ until the sets of remaining period vectors in $R$ and $S$ stabilize:

• $\mathrm{■}$

  If neither $R$ nor $S$ is bounded at $j$, we leave $S$ and $R$ untouched.

• $\mathrm{■}$

  If only $R$ is bounded at $j$, we remove all period vectors from $S$ which have support on $j$.

• $\mathrm{■}$

  If only $S$ is bounded at $j$, we remove all period vectors from $R$ which have support on $j$.

Then, the coordinates that remain unbounded are precisely the twin-unbounded ones.

For $J\subseteq [1,d]$, we write $U_J=\{𝒑\in U\mid \mathrm{supp}(𝒑)\subseteq J\}$ and $V_J=\{𝒒\in V\mid \mathrm{supp}(𝒒)\subseteq J\}$.

As observed in [14, 16], if all coordinates of two linear sets $L_1,L_2$ are unbounded, then separability holds if and only if the two sets can be separated by modulo constraints. This relies on the well known fact that finitely generated abelian groups are subgroup separable, i.e. that for every element $𝒖\in {\mathbb{Z}}^d$ that does not belong to a subgroup $A\subseteq {\mathbb{Z}}^d$, there exists a homomorphism $\phi :{\mathbb{Z}}^d\to 𝔽$ into a finite group $𝔽$ such that (i) $A$ is included in the kernel of $\phi$ and (ii) $\phi (𝒖)\ne 0$. In our characterization (Proposition 4.5) we will use similar arguments and therefore we will recall subgroup separability here. We include a short proof in the full version.

We will now characterize inseparability of hyperlinear sets $R,S$ via the intersection of two hyperlinear sets $\widehat{R}$ and $\widehat{S}$ associated with $R,S$. The proof will rely on an equivalence relation of vectors. For vectors $𝒖,𝒗\in {\mathbb{N}}^d$ and $k\in \mathbb{N}\setminus \{0\}$, we write $𝒖{\sim }_k𝒗$ if for every $i\in [1,d]$, we have

1. (1)

   $𝒖[i]=𝒗[i]\le k$ or

2. (2)

   $𝒖[i],𝒗[i]>k$ and $𝒖[i]\equiv 𝒗[i]modk$.

The following was shown in [16, Prop. 18].

Let $k,\mathrm{\ell }\in \mathbb{N}\setminus \{0\}$ be such that $k$ divides $\mathrm{\ell }$. We can observe that $𝒖{\sim }_{\mathrm{\ell }}𝒗$ implies $𝒖{\sim }_k𝒗$ in this case. Thus, to show recognizable inseparability of two sets $X,Y\subseteq {\mathbb{N}}^d$, it suffices to find ${𝒙}_k\in X$ and ${𝒚}_k\in Y$ for almost all numbers $k\in \mathbb{N}\setminus \{0\}$. We will use this fact in the proof of the following characterization of inseparability.

Suppose there is a vector $𝒙$ in the intersection (1). Then we can write $𝒙=𝒖-\overline{𝒖}$ and $𝒙=𝒗-\overline{𝒗}$ with $𝒖\in A+U^{\ast }$, $𝒗\in B+V^{\ast }$, $\overline{𝒖}\in U_J^{\ast }$, and $\overline{𝒗}\in V_J^{\ast }$. Since $J$ is twin-unbounded for $R$ and $S$, there are – by definition – ${𝒑}_j\in U^{\ast }$ and ${𝒒}_j\in V^{\ast }$ with $j\in \mathrm{supp}({𝒑}_j)=\mathrm{supp}({𝒒}_j)$ for each $j\in J$. Then for $𝒑:={\sum }_{j\in J}{𝒑}_j$ and $𝒒:={\sum }_{j\in J}{𝒒}_j$ we infer $J\subseteq \mathrm{supp}(𝒑)=\mathrm{supp}(𝒒)$. Now for each $k\in \mathbb{N}\setminus \{0\}$, consider the vectors

Then we have ${𝒖}_k,{𝒗}_k\in {\mathbb{N}}^d$ for each $k\in \mathbb{N}\setminus \{0\}$. We claim that ${𝒖}_k{\sim }_k{𝒗}_k$ for all $k$. Indeed, on coordinates $j\in [1,d]\setminus \mathrm{supp}(𝒑)$, the vectors ${𝒖}_k$ and ${𝒗}_k$ coincide with $𝒙$. Moreover, on coordinates $j\in \mathrm{supp}(𝒑)$, both vectors ${𝒖}_k$ and ${𝒗}_k$ are larger than $k$ and also congruent to $𝒙[j]modk$. Hence, ${𝒖}_k{\sim }_k{𝒗}_k$. Since clearly ${𝒖}_k=𝒖+2k\cdot 𝒑+(k-1)\cdot \overline{𝒖}\in R$ and ${𝒗}_k=𝒗+2k\cdot 𝒒+(k-1)\cdot \overline{𝒗}\in S$, Lemma 4.4 implies that $R$ and $S$ are not separable.

Conversely, suppose that $R$ and $S$ are not separable. Then by Lemma 4.4 there are ${𝒖}_k\in R$ and ${𝒗}_k\in S$ with ${𝒖}_k{\sim }_k{𝒗}_k$ for every $k\in \mathbb{N}\setminus \{0\}$. We claim that the sequences ${𝒖}_1,{𝒖}_2,\mathrm{\dots }$ and ${𝒗}_1,{𝒗}_2,\mathrm{\dots }$ have subsequences ${𝒖}_1^{\prime },{𝒖}_2^{\prime },\mathrm{\dots }$ and ${𝒗}_1^{\prime },{𝒗}_2^{\prime },\mathrm{\dots }$ such that for every $k\ge 1$, we have (i) ${𝒖}_{k+1}^{\prime }\in {𝒖}_k^{\prime }+U_J^{\ast }$, (ii) ${𝒗}_{k+1}^{\prime }\in {𝒗}_k^{\prime }+V_J^{\ast }$ and (iii) ${𝒖}_k^{\prime }{\sim }_k{𝒗}_k^{\prime }$.

The claim is easy to observe: Note that by picking subsequences, we may assume that even ${𝒖}_k{\sim }_{k!}{𝒗}_k$ for every $k\ge 1$. Moreover, the latter property is preserved by taking subsequences. Thus, since $A,B$ are finite, by picking subsequences again, we may assume that there are $𝒓\in A$ and $𝒔\in B$ such that ${𝒖}_k\in 𝒓+U^{\ast }$ and ${𝒖}_k\in 𝒔+V^{\ast }$ and ${𝒖}_k{\sim }_{k!}{𝒗}_k$ for $k\ge 1$. Then, by Dickson’s lemma, we may assume that in addition ${𝒖}_{k+1}\in {𝒖}_k+U^{\ast }$ and ${𝒗}_{k+1}\in {𝒗}_k+V^{\ast }$ for every $k\ge 1$ (here, we apply Dickson’s lemma to the $|U|$-dimensional vectors of coefficients at period vectors in $U$ and similarly for $V$). Now since ${𝒖}_k{\sim }_{k!}{𝒗}_k$ for every $k$, it follows that the sequences ${𝒖}_1,{𝒖}_2,\mathrm{\dots }$ and ${𝒗}_1,{𝒗}_2,\mathrm{\dots }$ are unbounded on the same set $J\subseteq [1,d]$ of coordinates. Then clearly, $J$ is twin-unbounded for $R$ and $S$. This means, for all but finitely many $k$, we have ${𝒖}_{k+1}\in {𝒖}_k+U_J^{\ast }$ and ${𝒗}_{k+1}\in {𝒗}_k+V_J^{\ast }$. Hence, by picking another subsequence, we may assume that the latter holds for every $k\ge 1$. Then, ${𝒖}_1,{𝒖}_2,\mathrm{\dots }$ and ${𝒗}_1,{𝒗}_2,\mathrm{\dots }$ satisfy the properties (i–iii) above, establishing our claim.

We now claim that ${𝒖}_1-{𝒗}_1$ belongs to the group $⟨U_J\cup V_J⟩$ generated by $U_J\cup V_J$. Towards a contradiction, suppose ${𝒖}_1-{𝒗}_1$ does not belong to $⟨U_J\cup V_J⟩$. By Lemma 4.3, there must be an $s\in \mathbb{N}$, $s>0$, and a morphism $\phi :{\mathbb{Z}}^d\to \mathbb{Z}/s\mathbb{Z}$ such that $\phi (⟨U_J\cup V_J⟩)=0$ and $\phi ({𝒖}_1-{𝒗}_1)\ne 0$. However, the vector

belongs to $⟨U_J\cup V_J⟩$, but also agrees with ${𝒖}_1-{𝒗}_1$ under $\phi$ (since all components of ${𝒖}_s-{𝒗}_s$ are divisible by $s$), contradicting Lemma 4.3. Hence ${𝒖}_1-{𝒗}_1\in ⟨U_J\cup V_J⟩$.

This means, we can write ${𝒖}_1-{𝒗}_1=𝒗-\overline{𝒗}-(𝒖-\overline{𝒖})$ with $𝒖,\overline{𝒖}\in U_J^{\ast }$ and $𝒗,\overline{𝒗}\in V_J^{\ast }$. But then the vector ${𝒖}_1+𝒖-\overline{𝒖}={𝒗}_1+𝒗-\overline{𝒗}$ belongs to the intersection (1). $◀$

With Proposition 4.5, we have now characterized inseparability of subsets of ${\mathbb{N}}^d$ via a particular intersection of two sets in ${\mathbb{Z}}^d$. It will later be more convenient to work with intersections of sets in ${\mathbb{N}}^d$, which motivates the following reformulation of Proposition 4.5.

Direct consequence of Proposition 4.5, since clearly $A+U^{\ast }-U_J^{\ast }$ intersects $B+V^{\ast }-V_J^{\ast }$ if and only if $A+U^{\ast }+V_J^{\ast }$ intersects $B+V^{\ast }+U_J^{\ast }$. $◀$

Let us first see that we can reduce the problem to the case where both input sets are given as projections of solution sets of linear Diophantine equations. We may assume that the input formulas are of the form $\exists 𝒙:\kappa (𝒙,𝒚)$, where $\kappa$ is a formula consisting of conjunction and disjunction (i.e. no negation) of atoms of the form $t\ge a$, where $t$ is a linear combination of variables $𝒙=(x_1,\mathrm{\dots },x_n),𝒚=(y_1,\mathrm{\dots },y_m)$ and integer coefficients, and $a$ is a constant.

Let $\phi$ be a formula as described above. It is a well known fact that $\phi$ can be transformed into disjunctive normal form. This means, $\phi$ is equivalent to a formula ${\phi }_1\vee \mathrm{\cdots }\vee {\phi }_k$, where each ${\phi }_i$ (a so-called clause) has the form $\exists 𝒙:\xi (𝒙,𝒚)$ such that $\xi$ is a conjunction of atoms appearing in $\phi$. In general, the number of clauses of $\phi$ is exponential.

Now, let $\phi$ and $\psi$ be the input formulas of the algorithm and let ${\phi }_1\vee \mathrm{\cdots }\vee {\phi }_k$ and ${\psi }_1\vee \mathrm{\cdots }\vee {\psi }_{\mathrm{\ell }}$ be their equivalent formulas in disjunctive normal form. Since the number of clauses is exponential, we cannot compute all clauses for $\phi$ and $\psi$. However, the solution sets of $\phi$ and $\psi$ are recognizably inseparable if, and only if, for some pair $i,j$, the solution sets of the formulas ${\phi }_i$ and ${\psi }_j$ are recognizably inseparable. This is due to the following fact, which follows standard ideas (see the full version for a proof in this particular setting).

Thus, for deciding the inseparability of the solution sets of $\phi$ and $\psi$ in $\mathrm{𝖭𝖯}$ it is sufficient to guess (in polynomial time) clauses ${\phi }_i$ and ${\psi }_j$ and show that inseparability of the solution sets of these two formulas is decidable in $\mathrm{𝖭𝖯}$. Therefore, from now on we can assume that the input formulas are (existentially quantified) conjunctions of atoms of the form $t\ge a$.

In particular, each of the two input sets is a projection of the solution set of a system of linear Diophantine inequalities. By introducing slack variables (which will also be projected away), we can turn inequalities into equations. Thus, we have as input sets $K,L\subseteq {\mathbb{N}}^d$ with

where $\pi :{\mathbb{Z}}^r\to {\mathbb{Z}}^d$ is the projection to the first $d$ components, $A,C\in {\mathbb{Z}}^{s\times r}$ are integer matrices, and $𝒃,𝒅\in {\mathbb{Z}}^s$ are integer vectors. Note that here, assuming that the numbers $r$ of columns and the number $s$ of rows is the same for $K$ and $L$ means no loss of generality.

In the second step, we will reduce recognizable inseparability of $K$ and $L$ to satisfiability of an existential Presburger formula. To this end, we use the fact that the solution sets to $A𝒙=𝒃$ (resp. $C𝒙=𝒅$) are hyperlinear sets, which allows us to apply Theorem 4.6.

We apply Theorem 4.6. To this end, we use the standard hyperlinear representation for solution sets of systems of linear Diophantine equalities. Let $A_0\subseteq {\mathbb{N}}^r$ be the set of all (component-wise) minimal solutions to $A𝒙=𝒃$, and let $U\subseteq {\mathbb{N}}^r$ be the set of all minimal solutions to $A𝒙=\mathrm{𝟎}$. Then it is well known that $A_0$ and $U$ are finite and also $K=\pi (A_0+U^{\ast })=\pi (A_0)+\pi {(U)}^{\ast }$. In the same way, we obtain a hyperlinear representation $L=\pi (B_0+V^{\ast })=\pi (B_0)+\pi {(V)}^{\ast }$. Then, we can show the Proposition using Theorem 4.6. For a full proof, see the full version.$◀$

Finally, Proposition 5.2 can be used to complete the proof of our first main result:

Let $\phi$ and $\psi$ be two existential Presburger formulas without negation and using only atoms of the form $t\ge 0$, where $t$ is a linear combination of variables and integer coefficients. We give an $\mathrm{𝖭𝖯}$ algorithm deciding inseparability by a recognizable set.

Since the solution sets of $\phi$ and $\psi$ are inseparable if, and only if, their disjunctive normal forms have at least one pair of inseparable clauses, we guess such a pair of these clauses ${\phi }_i$ and ${\psi }_j$ (cf. Lemma 5.1). We can transform ${\phi }_i$ and ${\psi }_j$ into Diophantine equations $A𝒙=𝒃$ and $C𝒙=𝒅$. Using Proposition 5.2 we obtain in polynomial time an existential Presburger formula that is satisfiable if, and only if, the solution sets of $A𝒙=𝒃$ and $C𝒙=𝒅$ are inseparable if, and only if, ${\phi }_i$ and ${\psi }_j$ are inseparable. Finally, the result follows from $\mathrm{𝖭𝖯}$-completeness of the existential fragment of Presburger arithmetic. $◀$

A ($d$-dimensional) integer vector addition system with states ($\mathbb{Z}$-VASS, for short) is a quintuple $𝒱=(Q,\mathrm{\Sigma },T,\iota ,f)$ where $Q$ is a finite set of states, $\mathrm{\Sigma }$ is an alphabet, $T\subseteq Q\times {\mathrm{\Sigma }}_{\epsilon }\times {\mathbb{Z}}^d\times Q$ is a finite set of transitions, and $\iota ,f\in Q$ are its source and target state, respectively. Here, ${\mathrm{\Sigma }}_{\epsilon }=\mathrm{\Sigma }\cup \{\epsilon \}$. A $\mathbb{Z}$-VASS $𝒱=(Q,\mathrm{\Sigma },T,\iota ,f)$ is called deterministic if $𝒱$ has no $\epsilon$-labeled transitions and for each $p\in Q$ and $a\in \mathrm{\Sigma }$ there is at most one transition of the form $(p,a,𝒗,q)\in T$ (where $𝒗\in {\mathbb{Z}}^d$ and $q\in Q$).

A configuration of $𝒱$ is a tuple from $Q\times {\mathbb{Z}}^d$. For two configurations $(p,𝒖),(q,𝒗)$ and a word $w\in {\mathrm{\Sigma }}^{\ast }$ we write $(p,𝒖){\stackrel{𝑤}{\to }}_{𝒱}(q,𝒗)$ if there are states $q_0,q_1,\mathrm{\dots },q_{\mathrm{\ell }}\in Q$, vectors ${𝒗}_0,{𝒗}_1,\mathrm{\dots },{𝒗}_{\mathrm{\ell }}\in {\mathbb{Z}}^d$, and letters $a_1,\mathrm{\dots },a_{\mathrm{\ell }}\in {\mathrm{\Sigma }}_{\epsilon }$ such that $w=a_1{a}_2\mathrm{\cdots }{a}_{\mathrm{\ell }}$, $(p,𝒖)=(q_0,{𝒗}_0)$, $(q,𝒗)=(q_{\mathrm{\ell }},{𝒗}_{\mathrm{\ell }})$, and for each $1\le i\le \mathrm{\ell }$ we have a transition $t_i=(q_{i-1},a_i,{𝒙}_i,q_i)\in T$ with ${𝒗}_i={𝒗}_{i-1}+{𝒙}_i$. In this case, the sequence $t_1{t}_2\mathrm{\cdots }{t}_{\mathrm{\ell }}$ is called a ($w$-labeled) run of $𝒱$. The accepted language of $𝒱$ is $L(𝒱)=\{w\in {\mathrm{\Sigma }}^{\ast }\mid (\iota ,\mathrm{𝟎}){\stackrel{𝑤}{\to }}_{𝒱}(f,\mathrm{𝟎})\}$.

Let $I\subseteq [1,d]$ be a set of indices. Then we can generalize the acceptance behavior of the $\mathbb{Z}$-VASS $𝒱$ as follows:

Note that $L(𝒱,[1,d])=L(𝒱)$ holds.

The remaining part of this section is dedicated to the proof of our second main result, Theorem 3.6. The first few steps (Lemmas 6.1, 6.2, 6.3, and 6.5) are essentially the same as in [15], for which we briefly give an overview: The authors reduce regular separability to recognizable separability of semilinear sets in ${\mathbb{N}}^d$ (for some dimension $d$). Concretely, instead of asking for the regular separability in two given $\mathbb{Z}$-VASS we are counting the cycles within runs of these $\mathbb{Z}$-VASS. Accordingly, the dimension $d$ corresponds to the number of (simple) cycles. Unfortunately, this number is exponential in the size of the input and therefore we cannot just use our first main result (Theorem 3.1) to prove the $\mathrm{𝖼𝗈𝖭𝖯}$ upper complexity bound. Instead we will construct two $\mathbb{Z}$-VASS (of polynomial dimension) accepting sequences of cycles such that their language intersection corresponds to the intersection (2) from Theorem 4.6 (which is non-empty if, and only if, the $\mathbb{Z}$-VASS from the input are regularly inseparable). Intersection for $\mathbb{Z}$-VASS is known to be in $\mathrm{𝖭𝖯}$ implying also the $\mathrm{𝖭𝖯}$ upper complexity bound for the regular inseparability problem resp. the $\mathrm{𝖼𝗈𝖭𝖯}$ upper bound for the separability problem of $\mathbb{Z}$-VASS.

As announced, we will first follow the reduction from [15]. In the first step, the regular separability problem of nondeterministic $\mathbb{Z}$-VASS can be reduced to the same problem in deterministic $\mathbb{Z}$-VASS. This reduction is possible in polynomial time which is a bit surprising at first glance since determinization typically requires at least an exponential blowup. However, in this reduction we determinize the $\mathbb{Z}$-VASS “up to some homomorphic preimage”, i.e., from two given $\mathbb{Z}$-VASS ${𝒱}_1$ and ${𝒱}_2$ one constructs two deterministic $\mathbb{Z}$-VASS ${𝒲}_1$ and ${𝒲}_2$ with (i) $L({𝒲}_i)=h^{-1}(L({𝒱}_i))$ where $h:{\mathrm{\Gamma }}^{\ast }\to {\mathrm{\Sigma }}^{\ast }$ is a homomorphism and (ii) $L({𝒱}_1)|L({𝒱}_2)$ if, and only if, $L({𝒲}_1)|L({𝒲}_2)$ holds. Since our setting is technically slightly different, we include a proof in the full version.

Next, we reduce regular separability for deterministic $\mathbb{Z}$-VASS to regular separability of two languages accepted by the same deterministic $\mathbb{Z}$-VASS, but with different sets of counters. To this end, given $d$-dim. $\mathbb{Z}$-VASS ${𝒱}_1$ and ${𝒱}_2$ we construct one $2d$-dim. $\mathbb{Z}$-VASS $𝒱$ (using product construction) and two index sets $I_1,I_2\subseteq [1,2d]$ such that $L({𝒱}_i)=L(𝒱,I_i)$. We include a detailed proof for our setting in the full version.

Therefore, we now fix a $\mathbb{Z}$-VASS $𝒱=(Q,\mathrm{\Sigma },T,\iota ,f)$.

Now, we want to further simplify the regular separability problem. Concretely, we want to consider only runs in $𝒱$ that are in some sense similar. We consider some base paths – so called skeletons – in $𝒱$. Two runs in $𝒱$ are similar if they follow the same base path and only differ in the order and repetition of some cycles. We define the function $\mathrm{skel}:T^{\ast }\to T^{\ast }$ such that $\mathrm{skel}(r)=\rho$ for a path $r\in T^{\ast }$ in $𝒱$ such that $\rho$ is a sub-path of the original path $r$ in which we keep the same set of visited states while removing all cycles that do not increase the set of visited states. Here, $\rho$ is called the skeleton of $r$.

Let $t_1\mathrm{\cdots }{t}_{\mathrm{\ell }}\in T^{\ast }$ be a path in $𝒱$, i.e., we have $t_i=(q_{i-1},a_i,{𝒙}_i,q_i)\in T$ for each $1\le i\le \mathrm{\ell }$. The map $\mathrm{skel}$ is defined inductively as follows: $\mathrm{skel}(\epsilon )=\epsilon$ and $\mathrm{skel}(t_1)=t_1$. For assume that $\mathrm{skel}(t_1\mathrm{\cdots }{t}_i)=s_1\mathrm{\cdots }{s}_j$ is already constructed and that $s_1\mathrm{\cdots }{s}_j$ is a path ending in $q_i$. Now we consider the transition $t_{i+1}$. If there is no transition $s_k$ (with $0\le k\le j$) such that this transition ends in the state $q_{i+1}$, we set $\mathrm{skel}(t_1\mathrm{\cdots }{t}_i{t}_{i+1})=s_1\mathrm{\cdots }{s}_j{t}_{i+1}$. Note that $s_1\mathrm{\cdots }{s}_j{t}_{i+1}$ is a path ending in the state $q_{i+1}$.

Otherwise, let $0\le k\le j$ be maximal such that $s_k$ ends in $q_{i+1}$. Then $s_{k+1}\mathrm{\cdots }{s}_j{t}_{i+1}$ is a cycle in $𝒱$ (note that $s_{k+1}$ starts with $q_{i+1}$ since $s_1\mathrm{\cdots }{s}_j$ is a path). If all states occurring in the cycle $s_{k+1}\mathrm{\cdots }{s}_j{t}_{i+1}$ also occur in the path $s_1\mathrm{\cdots }{s}_k$, then we set $\mathrm{skel}(t_1\mathrm{\cdots }{t}_i{t}_{i+1})=s_1\mathrm{\cdots }{s}_k$, i.e., we omit the cycle $s_{k+1}\mathrm{\cdots }{s}_j{t}_{i+1}$ in the skeleton. Note that the skeleton $s_1\mathrm{\cdots }{s}_k$ is a path ending in $q_{i+1}$. Otherwise at least one state in the cycle does not occur in the path $s_1\mathrm{\cdots }{s}_k$. In this case, we simply add $t_{i+1}$ resulting in $\mathrm{skel}(t_1\mathrm{\cdots }{t}_i{t}_{i+1})=s_1\mathrm{\cdots }{s}_j{t}_{i+1}$ where $s_1\mathrm{\cdots }{s}_j{t}_{i+1}$ is also a path ending in $q_{i+1}$. Note that any skeleton of $𝒱$ has length at most quadratic in the number of transitions $|T|$ as shown in [15, Lemma 10].

Let $\rho$ be a skeleton. A $\rho$-cycle is a cycle that only visits states occurring in $\rho$; a $\rho$-run is a run $r\in T^{\ast }$ with skeleton $\mathrm{skel}(r)=\rho$ (i.e., $r$ is obtained from $\rho$ by inserting $\rho$-cycles). We write $L(𝒱,I,\rho )$ for the set of all words in $L(𝒱,I)$ accepted via $\rho$-runs.

Although this was essentially shown in [15, Lemma 11], our setting is strictly speaking slightly different (e.g. we have all short rather than only simple cycles), so we include a detailed proof in the full version. Thus, it suffices to show that for a given skeleton $\rho$, one can decide regular inseparability of $L(𝒱,I_1,\rho )$ and $L(𝒱,I_2,\rho )$ in $\mathrm{𝖭𝖯}$. So, from now on, we fix a skeleton $\rho$ and simply write $L(I_i)$ for $L(𝒱,I_i,\rho )$. Since we only consider runs that visit states that occur in $\rho$, we may also assume that $𝒱$ consists only of the states occurring on $\rho$. In particular, we only say cycle instead of “$\rho$-cycle”.

We now phrase a characterization of regular separability from [15] in our setting. It says that regular separability of the languages $L(I_1)$ and $L(I_2)$ is equivalent to recognizable separability of vectors that count cycles. Here, we only count short cycles of length at most $|Q|$. This is possible since each cycle can be decomposed into short cycles. In the following, we fix the set $S\subseteq T^{\le |Q|}$ of all short cycles in $𝒱$.⁴⁴4Although Lemmas 6.1, 6.2, 6.3, and 6.5 are essentially the same as in [15], we are working with short cycles, whereas [15] uses simple cycles. This will be crucial later, because short cycles can be guessed on-the-fly in a finite automaton without storing the whole cycle.

For $I\subseteq [1,d]$, we define: if $t=(p,a,𝒙,q)\in T$ is a transition then the effect ${\mathrm{\Delta }}_I(t)$ of $t$ to the components in $I$ is ${\mathrm{\Delta }}_I(t)={\pi }_I(𝒙)$, i.e. the projection of the counter update $𝒙$ to $I$. If $r=t_1{t}_2\mathrm{\cdots }{t}_{\mathrm{\ell }}\in T^{\ast }$ is a path, then the effect ${\mathrm{\Delta }}_I(r)$ of $r$ to the components in $I$ is the sum of the effects of all transitions on this path, i.e. ${\mathrm{\Delta }}_I(r)={\sum }_{i=1}^{\mathrm{\ell }}{\mathrm{\Delta }}_I(t_i)$. Now, let $𝒖\in {\mathbb{N}}^S$ be a multiset of short cycles. Then the effect of $𝒖$ to the components in $I$ is ${\mathrm{\Delta }}_I(𝒖)={\sum }_{c\in S}𝒖[c]\cdot {\mathrm{\Delta }}_I(c)$. If $𝒗\in {\mathbb{N}}^T$ is a multiset of transitions, then the effect of $𝒗$ to the components in $I$ is ${\mathrm{\Delta }}_I(𝒗)={\sum }_{t\in T}𝒗[t]\cdot {\mathrm{\Delta }}_I(t)$. In case of $I=[1,d]$ we will also write $\mathrm{\Delta }$ instead of ${\mathrm{\Delta }}_I$. Finally, we define

Hence, $M(I)$ is the set of multisets of short cycles such that inserting them into $\rho$ would lead to an accepting run with acceptance condition $I\subseteq [1,d]$. Since $M(I)$ is the solution set of linear Diophantine equations, it is hyperlinear (see the full version for a proof).

The following equivalence between regular separability of the languages $L(I_i)$ and recognizable separability of the (hyperlinear) sets $M(I_i)$ was shown in [15, Lemma 12]. It is straightforward to adapt it to our situation (see the full version).

At this point, our proof deviates from the approach of [15]. According to Lemma 6.5, it remains to decide whether $M(I_1)|M(I_2)$, where $M(I_1)$ and $M(I_2)$ are sets of vectors of dimension $|S|$, which is exponential. In Theorem 4.6, we saw that recognizable separability of vector sets $A+U^{\ast }$ and $B+V^{\ast }$ reduces to intersection emptiness of $A+U^{\ast }+V_J^{\ast }$ and $B+V^{\ast }+U_J^{\ast }$, where $J$ is a subset of the twin-unbounded components. However, the exponential dimension of $M(I_1),M(I_2)$ means a direct translation into existential Presburger arithmetic would incur an exponential blowup.