LaBRI, Bordeaux University, France and
<EMAIL_ADDRESS>Bordeaux University,
France and<EMAIL_ADDRESS>T. Place and M.
Zeitoun [500]Theory of computation Formal languages and automata theory
[500]Theory of computation Regular languages John Q. Open and Joan R. Access 2
42nd Conference on Very Important Topics (CVIT 2016) CVIT 2016 CVIT 2016
December 24–27, 2016 Little Whinging, United Kingdom 42 23

# New Separation Algorithms for Level 1 in Group-based Concatenation
Hierarchies

Thomas Place  Marc Zeitoun

# A generic polynomial time approach to separation by first-order logic
without quantifier alternation

Thomas Place  Marc Zeitoun

###### Abstract

We look at classes of languages associated to the fragment of first-order
logic $\mathcal{B}\Sigma_{1}$, in which quantifier alternations are
disallowed. Each class is defined by choosing the set of predicates on
positions that may be used. Two key such fragments are those equipped with the
linear ordering and possibly the successor relation. Simon and Knast proved
that these two variants have decidable _membership_ : “does an input regular
language belong to the class ?”. We rely on a characterization of
$\mathcal{B}\Sigma_{1}$ by the operator $\mathit{BPol}$: given an input class
$\mathcal{C}$, it outputs a class $\mathit{BPol}(\mathcal{C})$ that
corresponds to a variant of $\mathcal{B}\Sigma_{1}$ equipped with special
predicates associated to $\mathcal{C}$. We extend the above results in two
orthogonal directions. First, we use two kinds of inputs: classes
$\mathcal{G}$ of _group languages_ (_i.e._ , recognized by a DFA in which each
letter induces a permutation of the states) and extensions thereof, written
$\mathcal{G}^{+}$. The classes $\mathit{BPol}(\mathcal{G})$ and
$\mathit{BPol}(\mathcal{G}^{+})$ capture many natural variants of
$\mathcal{B}\Sigma_{1}$ which use predicates such as the linear ordering, the
successor, the modular predicates or the alphabetic modular predicates.

Second, instead of membership, we explore the more general separation problem:
decide if two regular languages can be separated by a language from the class
under study. We show that separation is decidable for
$\mathit{BPol}(\mathcal{G})$ and $\mathit{BPol}(\mathcal{G}^{+})$ when this is
the case for $\mathcal{G}$. This was known for $\mathit{BPol}(\mathcal{G})$
and for two particular classes of the form $\mathit{BPol}(\mathcal{G}^{+})$.
Yet, the algorithms were indirect and relied on involved frameworks, yielding
poor upper complexity bounds. In contrast, the approach of the paper is
direct. We work only with elementary concepts (mainly, finite automata). Our
main contribution consists in polynomial time Turing reductions from both
$\mathit{BPol}(\mathcal{G})$\- and $\mathit{BPol}(\mathcal{G}^{+})$-separation
to $\mathcal{G}$-separation. This yields polynomial algorithms for many key
variants of $\mathcal{B}\Sigma_{1}$, including those equipped with the linear
ordering and possibly the successor and/or the modular predicates.

###### keywords:

Automata, Separation, Covering, Concatenation hierarchies, Group languages

###### category:

##  1 Introduction

An important question in automata theory is to precisely understand the
prominent classes of regular languages of finite words. We are interested in
the classes associated to a piece of syntax (such as regular expressions or
logic), whose purpose is to specify the languages of such classes. In the
paper, we formalize the goal of “understanding a given class $\mathcal{C}$” by
looking at a decision problem: $\mathcal{C}$-separation. It takes two regular
languages $L_{1},L_{2}$ as input and asks whether there exists
$K\in\mathcal{C}$ such that $L_{1}\subseteq K$ and $K\cap L_{2}=\emptyset$.
The key idea is that obtaining an algorithm for $\mathcal{C}$-separation
requires a solid understanding of $\mathcal{C}$.

We investigate a family of classes associated to a fragment of first-order
logic written $\mathcal{B}\Sigma_{1}$. The sentences of
$\mathcal{B}\Sigma_{1}$ are Boolean combinations of _existential_ formulas,
_i.e._ , whose prenex normal form has the shape $\exists x_{1}\exists
x_{2}\cdots\exists x_{k}\varphi$, with $\varphi$ quantifier-free. Several
classes are associated to $\mathcal{B}\Sigma_{1}$, each determined by the
predicates on positions that we allow. In the literature, standard examples of
predicates include the linear order “$<$” [26], the successor relation “$+1$”
[9] or modular predicates “$\mathit{MOD}$” [5]. Thus, a generic approach is
desirable.

We tackle languages associated to $\mathcal{B}\Sigma_{1}$ through the operator
$\mathcal{C}\mapsto\mathit{BPol}(\mathcal{C})$ defined on classes of
languages. It is the composition of the polynomial closure
$\mathcal{C}\mapsto\mathit{Pol}(\mathcal{C})$ and the Boolean closure
$\mathcal{C}\mapsto\mathit{Bool}(\mathcal{C})$ operators:
$\mathit{BPol}(\mathcal{C})=\mathit{Bool}(\mathit{Pol}(\mathcal{C}))$. Recall
that the polynomial closure of a class $\mathcal{C}$ consists of all finite
unions of languages of the form $L_{0}a_{1}L_{1}\cdots a_{n}L_{n}$, where
$n\geq 0$, each $a_{i}$ is a letter and each $L_{i}$ belongs to $\mathcal{C}$.
Indeed, many classes associated to $\mathcal{B}\Sigma_{1}$ are of the form
$\mathit{BPol}(\mathcal{C})$ [33, 20]. In this paper, we look at specific
input classes $\mathcal{C}$.

The _group languages_ are those recognized by a finite group, or equivalently
by a permutation automaton [32] (_i.e._ , which is complete, deterministic
_and_ co-deterministic). We consider input classes that are either a class
$\mathcal{G}$ consisting of group languages, or a well-suited extension
thereof, $\mathcal{G}^{+}$ (roughly, $\mathcal{G}^{+}$ is the least Boolean
algebra containing $\mathcal{G}$ and the singleton $\\{\varepsilon\\}$). It is
known [20] that if $\mathcal{G}$ is a class of group languages, then
$\mathit{BPol}(\mathcal{G})=\mathcal{B}\Sigma_{1}(<,\mathbb{P}_{\mathcal{G}})$
and
$\mathit{BPol}(\mathcal{G}^{+})=\mathcal{B}\Sigma_{1}(<,+1,\mathbb{P}_{\mathcal{G}})$.
Here, $\mathbb{P}_{\mathcal{G}}$ is a set of predicates associated to
$\mathcal{G}$: each language $L$ in $\mathcal{G}$ gives rise to a predicate
$P_{L}(x)$, which selects all positions $x$ in a word $w$ such that the prefix
of $w$ up to position $x$ (excluded) belongs to $L$. This captures most of the
natural examples. In particular, we get signatures including the
aforementioned predicates, such as $\\{<\\}$, $\\{<,+1\\}$,
$\\{<,\mathit{MOD}\\}$ and $\\{<,+1,\mathit{MOD}\\}$ (we provide some more
examples in the paper).

State of the art. Historically, $\mathit{BPol}(\mathcal{G})$ and
$\mathit{BPol}(\mathcal{G}^{+})$ were first investigated for particular input
classes. A prominent example is the class of piecewise testable languages
[26], _i.e._ , the class $\mathit{BPol}(\textup{ST})=\mathcal{B}\Sigma_{1}(<)$
where $\textup{ST}=\\{\emptyset,A^{*}\\}$. It was shown that
$\mathit{BPol}(\textup{ST})$-separation is decidable in [1] using technical
algebraic arguments. Simpler polynomial time algorithms were discovered later
[17, 6]. There also exists an involved specialized separation algorithm [35]
for $\mathit{BPol}(\textup{MOD})=\mathcal{B}\Sigma_{1}(<,\mathit{MOD})$, where
MOD is the class of modulo languages. Decidability can be lifted to
$\mathit{BPol}(\textup{ST}^{+})=\mathcal{B}\Sigma_{1}(<,+1)$ (the languages of
dot-depth one [9]) and to
$\mathit{BPol}(\textup{MOD}^{+})=\mathcal{B}\Sigma_{1}(<,+1,\mathit{MOD})$ via
transfer results [22, 16]. Unfortunately, this approach yields an exponential
complexity blow-up. Recently, a generic approach was developed for
$\mathit{BPol}(\mathcal{G})$. It is proved in [21] that if $\mathcal{G}$ is a
class of group languages with mild hypotheses,
$\mathit{BPol}(\mathcal{G})$-separation is decidable when
$\mathcal{G}$-separation is decidable. Yet, this generic approach is indirect
and considers a more general problem: _covering_. Because of this, the
algorithms and their proofs are complex and rely on an intricate framework
[19], yielding poor upper complexity bounds. This contrasts with the simple
polynomial time procedures presented in [17, 6] for
$\mathit{BPol}(\textup{ST})$. No generic result of this kind is known for the
classes $\mathit{BPol}(\mathcal{G}^{+})$.

Contributions. We give _generic polynomial time Turing reductions_ from
$\mathit{BPol}(\mathcal{G})$\- and $\mathit{BPol}(\mathcal{G}^{+})$-separation
to $\mathcal{G}$-separation, where $\mathcal{G}$ is a class of group languages
with mild properties. We present them as greatest fixpoint procedures which
use an oracle for $\mathcal{G}$-separation at each step and run in _polynomial
time_ (for input languages represented by nondeterministic finite automata).
While the proofs are involved, they are self-contained and based exclusively
on elementary concepts from automata theory. No particular knowledge on group
theory is required to follow them: we only use immediate consequences of the
definition of a group.

For $\mathit{BPol}(\mathcal{G})$, this new approach is a significant
improvement on the results of [21]. While we do reuse some ideas of [21], we
complement them with new ones and the presentation is independent. We get a
simpler algorithm, which requires only basic notions from automata theory. In
particular, one direction of the proof describes a generic construction for
building separators in $\mathit{BPol}(\mathcal{G})$ (when they exist). This
serves our main objective: understanding classes of languages. In addition, we
obtain much better complexity upper bounds on
$\mathit{BPol}(\mathcal{G})$-separation. Finally, our techniques can handle
$\mathit{BPol}(\mathcal{G}^{+})$ as well. This was not the case in [21]: the
generic reduction from $\mathit{BPol}(\mathcal{G}^{+})$-separation to
$\mathcal{G}$-separation is a new result.

These results apply to several key classes. Separation is decidable in
polynomial time for $\textup{ST}=\\{\emptyset,A^{*}\\}$, for the class MOD of
modulo languages and for the class GR of _all_ group languages [25]. Hence,
the problem is also decidable in polynomial time for
$\mathit{BPol}(\textup{ST})$ (_i.e._ , $\mathcal{B}\Sigma_{1}(<)$),
$\mathit{BPol}(\textup{ST}^{+})$ (_i.e._ , $\mathcal{B}\Sigma_{1}(<,+1)$),
$\mathit{BPol}(\textup{MOD})$ (_i.e._ ,
$\mathcal{B}\Sigma_{1}(<,\mathit{MOD})$), $\mathit{BPol}(\textup{MOD}^{+})$
(_i.e._ , $\mathcal{B}\Sigma_{1}(<,+1,\mathit{MOD})$),
$\mathit{BPol}(\textup{GR})$ and $\mathit{BPol}(\textup{GR}^{+})$ (the logical
characterization of the last two classes is not standard, yet they are quite
prominent as well [11, 8]). This reproves a known result for
$\mathit{BPol}(\textup{ST})$ (in fact, we essentially reprove the algorithm of
[6]). The polynomial time upper bounds are new for all other classes. Another
application is the class AMT of alphabet modulo testable languages (which are
recognized by commutative groups): $\mathit{BPol}(\textup{AMT})$ and
$\mathit{BPol}(\textup{AMT}^{+})$ correspond to
$\mathcal{B}\Sigma_{1}(<,\mathit{AMOD})$ and
$\mathcal{B}\Sigma_{1}(<,+1,\mathit{AMOD})$ where “$\mathit{AMOD}$” is the set
of _alphabetic modular predicates_. We obtain the decidability of separation
for these classes (this is a new result for
$\mathit{BPol}(\textup{AMT}^{+})$). However, we do not get a polynomial time
upper bound: this is because AMT-separation is co-NP-complete (see [25]).

Important remark. Eilenberg’s theorem [7] connects some classes of regular
languages (the “varieties of languages”) with _varieties of finite monoids_.
It raised the hope to solve decision problems on languages (such as
membership) by translating them in terms of monoids and solving the resulting
purely algebraic questions—without referring to languages anymore. In
particular, Margolis and Pin [11, 13] characterized the algebraic counterpart
of $\mathit{BPol}(\mathcal{G})$ in Eilenberg’s correspondence (when
$\mathcal{G}$ is a variety) as the “ _semidirect product_ ”
$\mathsf{J}*\mathsf{G}$, where $\mathsf{J}$ is the variety of monoids
corresponding to $\mathcal{B}\Sigma_{1}(<)$ and $\mathsf{G}$ is the one
corresponding to $\mathcal{G}$. The new purely algebraic question is then:
“decide membership of a monoid in $\mathsf{J}*\mathsf{G}$”. Tilson [34]
developed an involved framework to reformulate membership in semidirect
products in terms of categories, which was successfully exploited to handle
$(\mathsf{J}*\mathsf{G})$-membership [8, 27].

Our results are completely independent from this algebraic approach. To
clarify, we do use combinatorics on monoids. Yet, our motivations and
techniques are disconnected from the theory of varieties of monoids, which is
a distinct field. We avoid it by choice: while the above approach highlights
an interesting connection between two fields, it is not necessarily desirable
when looking back at our primary goal, understanding _classes of languages_.
Indeed, a detour via varieties of monoids would obfuscate the intuition at the
language level. Fortunately, this paper shows that this detour can be
bypassed, while getting _stronger_ results. First, our results are more
general: they apply to _separation_ , and not only membership. It is not clear
at all that this can be obtained in the context of monoid varieties, as we
rely strongly on the definition of $\mathit{BPol}$: we work with languages of
the form $L_{0}a_{1}L_{1}\cdots a_{n}L_{n}$, for $L_{i}\in\mathcal{G}$.
Second, we can handle $\mathit{BPol}(\mathcal{G}^{+})$, thus capturing the
successor relation on the logical side. As far as we know, the only class of
this kind captured by the above framework is $\mathit{BPol}(\textup{ST}^{+})$
(these are the well-known dot-depth one languages [29]). Third, using the
above approach requires _varieties_ of languages as input classes. This, for
example, excludes the class $\mathit{BPol}(\textup{MOD})$. This does not mean
that this class cannot be handled by algebraic techniques: this was actually
done by Straubing [30, 15], who rebuilt the whole theory to be able to handle
such classes. In contrast, our result applies _uniformly_ to MOD.

Organization of the paper. We present the objects that we investigate and the
required terminology in Section 2. We introduce separation and the techniques
that we use to handle it in Section 3. Finally, we present our results for
$\mathit{BPol}(\mathcal{G})$\- and $\mathit{BPol}(\mathcal{G}^{+})$-separation
in Section 4. Due to space limitations, some proofs are presented in the
appendix only.

##  2 Preliminaries

###  2.1 Words, regular languages and classes

We fix a finite _alphabet_ $A$ for the paper. As usual, $A^{*}$ denotes the
set of all finite words over $A$, including the empty word $\varepsilon$. We
let $A^{+}=A^{*}\setminus\\{\varepsilon\\}$. For $u,v\in A^{*}$, we let $uv$
be the word obtained by concatenating $u$ and $v$. A _language_ is a subset of
$A^{*}$. We denote the singleton language $\\{u\\}$ by $u$. We lift
concatenation to languages: for $K,L\subseteq A^{*}$, we let $KL=\\{uv\mid
u\in K\text{ and }v\in L\\}$. We shall consider _marked products_ : given
languages $L_{0},\dots,L_{n}\subseteq A^{*}$, a marked product of
$L_{0},\dots,L_{n}$ is a product of the form $L_{0}a_{1}L_{1}\cdots
a_{n}L_{n}$ where $a_{1},\dots,a_{n}\in A$ (note that “$L_{0}$” is a marked
product: this is the case $n=0$).

Regular languages. In the paper, we consider _regular_ languages. A
nondeterministic finite automaton (NFA) is a pair $\mathcal{A}=(Q,\delta)$
where $Q$ is a finite set of states, and $\delta\subseteq Q\times A\times Q$
is a set of transitions. We now define the languages recognized by
$\mathcal{A}$. Given $q,r\in Q$ and $w\in A^{*}$, we say that there exists a
_run labeled by $w$ from $q$ to $r$_ (in $\mathcal{A}$) if there exist
$q_{0},\dots,q_{n}\in Q$ and $a_{1},\dots,a_{n}\in A$ such that $w=a_{1}\cdots
a_{n}$, $q_{0}=q$, $q_{n}=r$ and $(q_{i-1},a_{i},q_{i})\in\delta$ for every
$1\leq i\leq n$. Given two sets $I,F\subseteq Q$, we write
$L_{\mathcal{A}}(I,F)\subseteq A^{*}$ for the language of all words $w\in
A^{*}$ such that there exist $q\in I$, $r\in F$, and a run labeled by $w$ from
$q$ to $r$ in $\mathcal{A}$. We say that a language $L\subseteq A^{*}$ is
_recognized_ by $\mathcal{A}$ if and only if there exist $I,F\subseteq Q$ such
that $L=L_{\mathcal{A}}(I,F)$. The regular languages are those which can be
recognized by an NFA.

We also use NFAs with _$\varepsilon$ -transitions_. In such an NFA
$\mathcal{A}=(Q,\delta)$, a transition may also be labeled by the empty word
“$\varepsilon$” (that is, $\delta\subseteq
Q\times(A\cup\\{\varepsilon\\})\times Q$). We use the standard semantics: an
$\varepsilon$-transition can be taken without consuming an input letter. Note
that unless otherwise specified, the NFAs that we consider are assumed to be
_without_ $\varepsilon$-transitions.

Classes. A _class_ of languages is a set of languages. A _lattice_ is a class
containing $\emptyset$ and $A^{*}$ and closed under both union and
intersection. Moreover, a _Boolean algebra_ is a lattice closed under
complement. Finally, a class $\mathcal{C}$ is _quotient-closed_ when for all
$L\in\mathcal{C}$ and all $v\in A^{*}$, the languages $v^{-1}L=\\{w\in
A^{*}\mid vw\in L\\}$ and $Lv^{-1}=\\{w\in A^{*}\mid wv\in L\\}$ both belong
to $\mathcal{C}$ as well. A _positive prevariety_ (resp. a  _prevariety_) is a
quotient-closed lattice (resp. a quotient-closed Boolean algebra) containing
_regular languages only_.

Group languages. A _monoid_ is a set $M$ equipped with a multiplication
$s,t\mapsto st$, which is associative and has a neutral element denoted by
“$1_{M}$”. Observe that $A^{*}$ endowed with concatenation is a monoid
($\varepsilon$ is the neutral element). It is well-known that a language $L$
is regular if and only if it is _recognized_ by a morphism $\alpha:A^{*}\to M$
into a _finite_ monoid $M$, _i.e._ , there exists $F\subseteq M$ such that
$L=\alpha^{-1}(F)$. We now restrict this definition: a monoid $G$ is a _group_
if every element $g\in G$ has an inverse $g^{-1}\in G$, _i.e._ , such that
$gg^{-1}=g^{-1}g=1_{G}$. A “ _group language_ ” is a language recognized by a
morphism into a _finite group_.

We consider classes $\mathcal{G}$ that are group prevarieties (_i.e._ ,
containing group languages only). We let GR be the class of _all_ group
languages. Another important example is the class AMT of _alphabet modulo
testable languages_. For every $w\in A^{*}$ and every $a\in A$, we write
$\\#_{a}(w)\in{\rm Nature}$ for the number of occurrences of “$a$” in $w$. The
class AMT consists in all finite Boolean combinations of languages $\\{w\in
A^{*}\mid\\#_{a}(w)\equiv k\bmod m\\}$ where $a\in A$ and $k,m\in{\rm Nature}$
are such that $k<m$. One may verify that these are exactly the languages
recognized by commutative groups. We also consider the class MOD, which
consists in all finite Boolean combinations of languages $\\{w\in
A^{*}\mid|w|\equiv k\bmod m\\}$ with $k,m\in{\rm Nature}$ such that $k<m$.
Finally, we write ST for the trivial class
$\textup{ST}=\\{\emptyset,A^{*}\\}$. One may verify that GR, AMT, MOD and ST
are all group prevarieties.

One may verify that $\\{\varepsilon\\}$ and $A^{+}$ are _not_ group languages.
This motivates the next definition: the _well-suited extension of a class
$\mathcal{C}$_, denoted by $\mathcal{C}^{+}$, consists of all languages of the
form $L\cap A^{+}$ or $L\cup\\{\varepsilon\\}$ where $L\in\mathcal{C}$. The
next lemma follows from the definition.

######  Lemma 2.1.

Let $\mathcal{C}$ be a prevariety. Then, $\mathcal{C}^{+}$ is a prevariety
containing $\\{\varepsilon\\}$ and $A^{+}$.

###  2.2 Polynomial and Boolean closure

We investigate two operators that one may apply to a class $\mathcal{C}$. The
_Boolean closure_ of $\mathcal{C}$, written $\mathit{Bool}(\mathcal{C})$, is
the least Boolean algebra containing $\mathcal{C}$. The _polynomial closure_
of $\mathcal{C}$, denoted by $\mathit{Pol}(\mathcal{C})$, consists of all
finite unions of marked products $L_{0}a_{1}L_{1}\cdots a_{n}L_{n}$ where
$L_{0},\dots,L_{n}\in\mathcal{C}$ and $a_{1},\dots,a_{n}\in A$. Finally, we
write $\mathit{BPol}(\mathcal{C})$ for
$\mathit{Bool}(\mathit{Pol}(\mathcal{C}))$. If $\mathcal{C}$ is a prevariety,
then $\mathit{Pol}(\mathcal{C})$ is a positive prevariety and
$\mathit{BPol}(\mathcal{C})$ is a prevariety. Proving that
$\mathit{Pol}(\mathcal{C})$ is closed under intersection is not immediate. It
was shown by Arfi [2] (see also [14, 20]).

######  Theorem 2.2.

If $\mathcal{C}$ is a prevariety, $\mathit{Pol}(\mathcal{C})$ is a positive
prevariety and $\mathit{BPol}(\mathcal{C})$ is a prevariety.

The two operators $\mathit{Pol}$ and $\mathit{Bool}$ induce standard
classifications called concatenation hierarchies: for a prevariety
$\mathcal{C}$, the _concatenation hierarchy of basis $\mathcal{C}$_ is built
from $\mathcal{C}$ by alternatively applying the operators $\mathit{Pol}$ and
$\mathit{Bool}$. We are interested in $\mathit{BPol}(\mathcal{C})$, which is
level _one_ in the concatenation hierarchy of basis $\mathcal{C}$. We look at
bases that are either a group prevariety $\mathcal{G}$ or its well-suited
extension $\mathcal{G}^{+}$. Most of the prominent concatenation hierarchies
in the literature use such bases. This is in part motivated by the logical
characterization of concatenation hierarchies, due to Thomas [33]. We briefly
recall it for the level one.

Consider a word $w=a_{1}\cdots a_{|w|}\in A^{*}$. We view $w$ as a linearly
ordered set of $|w|+2$ positions $\\{0,1,\dots,|w|,|w|+1\\}$ such that each
position $1\leq i\leq|w|$ carries the label $a_{i}\in A$ (on the other hand,
$0$ and $|w|+1$ are artificial unlabeled leftmost and rightmost positions). We
use first-order logic to describe properties of words: a sentence can quantify
over the positions of a word and use a predetermined set of predicates to test
properties of these positions. We also allow two constants “$min$” and “$max$”
interpreted as the artificial unlabeled positions $0$ and $|w|+1$ in a given
word $w$. A first-order sentence $\varphi$ defines the language of all words
satisfying the property stated by $\varphi$. We use several kinds of
predicates. For each $a\in A$, we associate a unary predicate (also denoted by
$a$), which selects the positions labeled by “$a$”. We also use two binary
predicates: the (strict) linear order “$<$” and the successor relation “$+1$”.
Finally, we associate a set of predicates $\mathbb{P}_{\mathcal{G}}$ to each
group prevariety $\mathcal{G}$. Every $L\in\mathcal{G}$ yields a unary
predicate $P_{L}$ in $\mathbb{P}_{\mathcal{G}}$, which is interpreted as
follows. Let $w=a_{1}\cdots a_{|w|}\in A^{*}$. The unary predicate $P_{L}$
selects all positions $i\in\\{0,\dots,|w|+1\\}$ such that $i\neq 0$ and
$a_{1}\cdots a_{i-1}\in L$.

######  Example 2.3.

The sentence “$\exists x\exists y\ (x<y)\wedge a(x)\wedge b(y)$” defines the
language $A^{*}aA^{*}bA^{*}$. The sentence “$\exists x\exists y\ a(x)\wedge
c(y)\wedge(y+1=max)$” defines $A^{*}aA^{*}c$. Finally, if
$L=(AA)^{*}\in\textup{MOD}$ (the words of even length), the sentence “$\exists
x\ a(x)\wedge P_{L}(x)$” defines the language $(AA)^{*}aA^{*}$.

The fragment of first-order logic containing exactly the Boolean combinations
of existential first-order sentences is denoted by “$\mathcal{B}\Sigma_{1}$”.
Let $\mathcal{G}$ be a group prevariety. We write
$\mathcal{B}\Sigma_{1}(<,\mathbb{P}_{\mathcal{G}})$ for the class of all
languages defined by a sentence of $\mathcal{B}\Sigma_{1}$ using only the
label predicates, the linear order “$<$” and those in
$\mathbb{P}_{\mathcal{G}}$. Moreover, we write
$\mathcal{B}\Sigma_{1}(<,+1,\mathbb{P}_{\mathcal{G}})$ for the class of all
languages defined by a sentence of $\mathcal{B}\Sigma_{1}$, which additionally
allows the successor predicate “$+1$”. The following proposition follows from
the results of [20, 24].

######  Proposition 2.4.

Let $\mathcal{G}$ be a group prevariety. We have
$\mathit{BPol}(\mathcal{G})=\mathcal{B}\Sigma_{1}(<,\mathbb{P}_{\mathcal{G}})$
and
$\mathit{BPol}(\mathcal{G}^{+})=\mathcal{B}\Sigma_{1}(<,+1,\mathbb{P}_{\mathcal{G}})$.

Key examples. The basis $\textup{ST}=\\{\emptyset,A^{*}\\}$ yields the
_Straubing-Thérien hierarchy_ [28, 31] (hence the notation of this basis). Its
level one is the class of piecewise testable languages [26]. Its well-suited
extension $\textup{ST}^{+}$ induces the _dot-depth hierarchy_ [3]. In
particular, $\mathit{BPol}(\textup{ST})$ and $\mathit{BPol}(\textup{ST}^{+})$
correspond to $\mathcal{B}\Sigma_{1}(<)$ and $\mathcal{B}\Sigma_{1}(<,+1)$, as
all predicates in $\mathbb{P}_{\textup{ST}}$ are trivial. The hierarchies of
bases MOD and $\textup{MOD}^{+}$ are also prominent (see for example [5, 10,
35]). The classes $\mathit{BPol}(\textup{MOD})$ and
$\mathit{BPol}(\textup{MOD}^{+})$ correspond to
$\mathcal{B}\Sigma_{1}(<,\mathit{MOD})$ and
$\mathcal{B}\Sigma_{1}(<,+1,\mathit{MOD})$ where “$\mathit{MOD}$” is the set
of _modular predicates_ (for all $r,q\in{\rm Nature}$ such that $r<q$, it
contains a unary predicate $M_{r,q}$ selecting the positions $i$ such that
$i\equiv r\bmod q$). Similarly, $\mathit{BPol}(\textup{AMT})$ and
$\mathit{BPol}(\textup{AMT}^{+})$ correspond to
$\mathcal{B}\Sigma_{1}(<,\mathit{AMOD})$ and
$\mathcal{B}\Sigma_{1}(<,+1,\mathit{AMOD})$ where “$\mathit{AMOD}$” is the set
of _alphabetic modular predicates_ (for all $a\in A$ and $r,q\in{\rm Nature}$
such that $r<q$, it contains a unary predicate $M^{a}_{r,q}$ selecting the
positions $i$ such the that number of positions $j<i$ with label $a$ is
congruent to $r$ modulo $q$). Finally, the group hierarchy, whose basis is GR
is also prominent [11, 8], though its logical characterization is not
standard.

Properties. We present a key ingredient [23, Lemma 3.6] (we provide a proof in
Appendix A). It describes a concatenation principle for the classes
$\mathit{BPol}(\mathcal{C})$ based on the notion of “cover”. Given a language
$L$, a cover of $L$ is a _finite_ set $\mathbf{K}$ of languages satisfying
$L\subseteq\bigcup_{K\in\mathbf{K}}K$. If $\mathcal{D}$ is a class, a
$\mathcal{D}$-cover of $L$ is a cover $\mathbf{K}$ of $L$ such that
$\mathbf{K}\subseteq\mathcal{D}$.

######  Proposition 2.5.

Let $\mathcal{C}$ be a prevariety, $n\in{\rm Nature}$,
$L_{0},\dots,L_{n}\in\mathit{Pol}(\mathcal{C})$ and $a_{1},\dots,a_{n}\in A$.
If $\mathbf{H}_{i}$ is a $\mathit{BPol}(\mathcal{C})$-cover of $L_{i}$ for all
$i\leq n$, then there is a $\mathit{BPol}(\mathcal{C})$-cover $\mathbf{K}$ of
$L_{0}a_{1}L_{1}\cdots a_{n}L_{n}$ such that for all $K\in\mathbf{K}$, there
exists $H_{i}\in\mathbf{H}_{i}$ for each $i\leq n$ satisfying $K\subseteq
H_{0}a_{1}H_{1}\cdots a_{n}H_{n}$.

For applying Proposition 2.5, we need a language $L_{0}a_{1}L_{1}\cdots
a_{n}L_{n}$ with $L_{0},\dots,L_{n}\in\mathit{Pol}(\mathcal{C})$. The next
tailored statements build such languages when $\mathcal{C}=\mathcal{G}$ or
$\mathcal{G}^{+}$ for a group prevariety $\mathcal{G}$ (see App. A for
proofs). While simple, these results are central: this is the unique place
where we use the fact that $\mathcal{G}$ contains only _group languages_. Let
$L\subseteq A^{*}$. With every word $w=a_{1}\cdots a_{n}\in A^{*}$, we
associate the language $\mathord{\uparrow}_{L}w=La_{1}L\cdots a_{n}L\subseteq
A^{*}$ (we let $\mathord{\uparrow}_{L}\varepsilon=L$). We first present the
statement for the case $\mathcal{C}=\mathcal{G}$, which can also be found in
[4, Prop. 3.11].

######  Proposition 2.6.

Let $H\subseteq A^{*}$ be a language and $L\subseteq A^{*}$ be a group
language containing $\varepsilon$. There exists a cover $\mathbf{K}$ of $H$
such that every $K\in\mathbf{K}$ is of the form $K=\mathord{\uparrow}_{L}w$
for some $w\in H$.

The next statement, useful for the case $\mathcal{C}=\mathcal{G}^{+}$, is a
corollary of Proposition 2.6. Let $\mathcal{A}=(Q,\delta)$ be an NFA.
Moreover, let $w,z\in A^{*}$. We say that $z$ is a _left $\mathcal{A}$-loop_
for $w$ if for every $q,r\in Q$ such that $w\in L_{\mathcal{A}}(q,r)$, there
exists $s\in Q$ such that $z\in L_{\mathcal{A}}(q,s)\cap L_{\mathcal{A}}(s,s)$
and $zw\in L_{\mathcal{A}}(s,r)$ (in particular, $zz^{*}zw\subseteq
L_{\mathcal{A}}(q,r)$). Symmetrically, we say that $z$ is a _right
$\mathcal{A}$-loop_ for $w$ if for every $q,r\in Q$ such that $w\in
L_{\mathcal{A}}(q,r)$, there exists $s\in Q$ such that $wz\in
L_{\mathcal{A}}(q,s)$ and $z\in L_{\mathcal{A}}(s,s)\cap L_{\mathcal{A}}(s,r)$
(in particular, $wzz^{*}z\subseteq L_{\mathcal{A}}(q,r)$).

Now, given an arbitrary word $w\in A^{*}$, an _$\mathcal{A}$ -guarded
decomposition of $w$_ is a tuple $(w_{1},\dots,w_{n+1})$ for some $n\in{\rm
Nature}$ where $w_{1}\in A^{*}$ and $w_{i}\in A^{+}$ for $2\leq i\leq n+1$,
and such that $w=w_{1}\cdots w_{n+1}$ and, if $n\geq 1$, then for every $i$
satisfying $1\leq i\leq n$, there exists a _nonempty_ word $z_{i}\in A^{+}$
which is a right $\mathcal{A}$-loop for $w_{i}$ and a left $\mathcal{A}$-loop
for $w_{i+1}$.

######  Proposition 2.7.

Let $H\subseteq A^{*}$ be a language, $\mathcal{A}$ be an NFA and $L\subseteq
A^{*}$ be a group language containing $\varepsilon$. There exists a cover
$\mathbf{K}$ of $H$ such that for each $K\in\mathbf{K}$, there exist a word
$w\in H$ and an $\mathcal{A}$-guarded decomposition $(w_{1},\dots,w_{n+1})$ of
$w$ for some $n\in{\rm Nature}$ such that $K=w_{1}L\cdots w_{n}Lw_{n+1}$ (if
$n=0$, then $K=\\{w_{1}\\}$).

##  3 Separation framework

In order to investigate a given class $\mathcal{C}$, we rely on a generic
decision problem that one may associate to it: _$\mathcal{C}$ -separation_. We
first define it and then present a variant, “tuple separation”, that we shall
require as a proof ingredient. The missing proofs are presented in Appendix B.

###  3.1 The separation problem

Consider two languages $L_{0},L_{1}\subseteq A^{*}$. We say that a third
language $K\subseteq A^{*}$ _separates_ $L_{0}$ from $L_{1}$ when
$L_{0}\subseteq K$ and $K\cap L_{1}=\emptyset$. Then, given an arbitrary class
$\mathcal{C}$, we say that $L_{0}$ is _$\mathcal{C}$ -separable_ from $L_{1}$
when there exists $K\in\mathcal{C}$ that separates $L_{0}$ from $L_{1}$. For
every class $\mathcal{C}$, the _$\mathcal{C}$ -separation problem_ takes _two_
regular languages $L_{0}$ and $L_{1}$ as input (in the paper, they are
represented by NFAs) and asks whether $L_{0}$ is $\mathcal{C}$-separable from
$L_{1}$. We complete the definition with a useful result, which holds when
$\mathcal{C}$ is a positive prevariety.

######  Lemma 3.1.

Let $\mathcal{C}$ be a positive prevariety and
$L_{0},L_{1},H_{0},H_{1}\subseteq A^{*}$. If $L_{0}$ is not
$\mathcal{C}$-separable from $L_{1}$ and $H_{0}$ is not
$\mathcal{C}$-separable from $H_{1}$ then $L_{0}H_{0}$ is not
$\mathcal{C}$-separable from $L_{1}H_{1}$.

In the paper, we look at $\mathcal{C}$-separation when
$\mathcal{C}=\mathit{BPol}(\mathcal{G})$ or $\mathit{BPol}(\mathcal{G}^{+})$
for a group prevariety $\mathcal{G}$. We prove that in these two cases, there
are polynomial time (Turing) reductions to $\mathcal{G}$-separation. We now
introduce terminology that we shall use to present the algorithms.

Framework. Consider a class $\mathcal{C}$ and an NFA $\mathcal{A}=(Q,\delta)$.
We associate a set $\mathcal{I}_{\mathcal{C}}[\mathcal{A}]\subseteq Q^{4}$:
the _inseparable $\mathcal{C}$-quadruples_ associated to $\mathcal{A}$. We
define,

$\mathcal{I}_{\mathcal{C}}[\mathcal{A}]=\big{\\{}(q,r,s,t)\in Q^{4}\mid
L_{\mathcal{A}}(q,r)\text{ is \text@underline{not} $\mathcal{C}$-separable
from }L_{\mathcal{A}}(s,t)\big{\\}}.$

The next easy result connects $\mathcal{C}$-separation to this set, for input
languages given by NFAs.

######  Proposition 3.2.

Let $\mathcal{C}$ be a lattice. Consider an NFA $\mathcal{A}=(Q,\delta)$ and
four sets of states $I_{1},F_{1},I_{2},F_{2}\subseteq Q$. The two following
conditions are equivalent:

  1. 1.

$L_{\mathcal{A}}(I_{1},F_{1})$ is $\mathcal{C}$-separable from
$L_{\mathcal{A}}(I_{2},F_{2})$.

  2. 2.

$\left(I_{1}\times F_{1}\times I_{2}\times
F_{2}\right)\cap\mathcal{I}_{\mathcal{C}}[\mathcal{A}]=\emptyset$.

Clearly, given as input two regular languages recognized by NFAs, one may
compute in polynomial time a single NFA recognizing both languages. Hence,
Proposition 3.2 yields a polynomial time reduction from
$\mathcal{C}$-separation to the problem of computing
$\mathcal{I}_{\mathcal{C}}[\mathcal{A}]$ from an input NFA. Naturally, this
does not necessarily mean that there exists a polynomial time algorithm for
$\mathcal{C}$-separation: depending on $\mathcal{C}$, computing
$\mathcal{I}_{\mathcal{C}}[\mathcal{A}]$ may or may not be costly.

We introduce a key definition for manipulating
$\mathcal{I}_{\mathcal{C}}[\mathcal{A}]$, for an NFA $\mathcal{A}=(Q,\delta)$.
Let $S\subseteq Q^{4}$ and $\mathbf{K}$ be a finite set of languages. We say
that _$\mathbf{K}$ is separating for $S$_ when for every $(q,r,s,t)\in Q^{4}$
and every $K\in\mathbf{K}$, if $K$ intersects both $L_{\mathcal{A}}(q,r)$ and
$L_{\mathcal{A}}(s,t)$, then $(q,r,s,t)\in S$. Then,
$\mathcal{I}_{\mathcal{C}}[\mathcal{A}]$ is the smallest set of 4-tuples
admitting a $\mathcal{C}$-cover of $A^{*}$ which is separating for it.

######  Lemma 3.3.

Let $\mathcal{C}$ be a Boolean algebra and $\mathcal{A}=(Q,\delta)$ be an NFA.
Then the following holds:

  * •

There exists a $\mathcal{C}$-cover $\mathbf{K}$ of $A^{*}$ which is separating
for $\mathcal{I}_{\mathcal{C}}[\mathcal{A}]$.

  * •

Let $S\subseteq Q^{4}$. If there exists a $\mathcal{C}$-cover $\mathbf{K}$ of
$A^{*}$ which is separating for $S$, then
$\mathcal{I}_{\mathcal{C}}[\mathcal{A}]\subseteq S$.

Controlled separation. We present additional terminology tailored to the
classes built from a group prevariety. Consider two classes $\mathcal{C}$ and
$\mathcal{D}$ (in practice, $\mathcal{D}$ will be a group prevariety
$\mathcal{G}$ and $\mathcal{C}$ will be either $\mathit{BPol}(\mathcal{G})$ or
$\mathit{BPol}(\mathcal{G}^{+})$). Let $L_{0},L_{1}\subseteq A^{*}$. We say
that $L_{0}$ is $\mathcal{C}$-separable from $L_{1}$ _under
$\mathcal{D}$-control_ if there exists $H\in\mathcal{D}$ such that
$\varepsilon\in H$ and $L_{0}\cap H$ is $\mathcal{C}$-separable from
$L_{1}\cap H$. Given an NFA $\mathcal{A}=(Q,\delta)$, we associate a set
$\mathcal{I}_{\mathcal{C}}[\mathcal{D},\mathcal{A}]\subseteq Q^{4}$:

$\mathcal{I}_{\mathcal{C}}[\mathcal{D},\mathcal{A}]=\big{\\{}(q,r,s,t)\in
Q^{4}\mid L_{\mathcal{A}}(q,r)\text{ is \text@underline{not}
$\mathcal{C}$-separable from }L_{\mathcal{A}}(s,t)\text{ under
$\mathcal{D}$-control}\big{\\}}.$

Clearly, we have
$\mathcal{I}_{\mathcal{C}}[\mathcal{D},\mathcal{A}]\subseteq\mathcal{I}_{\mathcal{C}}[\mathcal{A}]$.
Let us connect this new definition to the notion of separating cover presented
above. In this case as well, this will be useful in proof arguments.

######  Lemma 3.4.

Let $\mathcal{C}$ and $\mathcal{D}$ be Boolean algebras such that
$\mathcal{D}\subseteq\mathcal{C}$ and let $\mathcal{A}=(Q,\delta)$ be an NFA.
The following properties hold:

  * •

There exists $L\in\mathcal{D}$ with $\varepsilon\in L$, and a
$\mathcal{C}$-cover $\mathbf{K}$ of $L$ which is separating for
$\mathcal{I}_{\mathcal{C}}[\mathcal{D},\mathcal{A}]$.

  * •

Let $S\subseteq Q^{4}$. If there exist $L\in\mathcal{D}$ with $\varepsilon\in
L$, and a $\mathcal{C}$-cover $\mathbf{K}$ of $L$ which is separating for $S$,
then $\mathcal{I}_{\mathcal{C}}[\mathcal{D},\mathcal{A}]\subseteq S$.

This notion is only useful if $\\{\varepsilon\\}\not\in\mathcal{D}$. If
$\\{\varepsilon\\}\in\mathcal{D}$, then $L_{0}$ is $\mathcal{C}$-separable
from $L_{1}$ under $\mathcal{D}$-control if and only if either
$\varepsilon\not\in L_{0}$ or $\varepsilon\not\in L_{1}$. This is why the
notion is designed for group prevarieties: if $\mathcal{G}$ is such a class,
then $\\{\varepsilon\\}\not\in\mathcal{G}$. In this case, if
$\mathcal{C}\in\\{\mathcal{G},\mathcal{G}^{+}\\}$, then the set
$\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{G},\mathcal{A}]$ carries
more information than $\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{A}]$.
This is useful for the computation: rather than computing
$\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{A}]$ directly, our
procedures first compute
$\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{G},\mathcal{A}]$. The proof
is based on Propositions 2.5 and 2.6 (the latter requires $\mathcal{G}$ to
consist of group languages).

######  Proposition 3.5.

Let $\mathcal{G}$ be a group prevariety, let $\mathcal{C}$ be a prevariety
such that $\mathcal{G}\subseteq\mathcal{C}$ and let $\mathcal{A}=(Q,\delta)$
be an NFA. Then, $\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{A}]$ is
the least set $S\subseteq Q^{4}$ that contains
$\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{G},\mathcal{A}]$ and
satisfies the two following conditions:

  1. 1.

For all $q,r,s,t\in Q$ and $a\in A$, if $(q,a,r),(s,a,t)\in\delta$, then
$(q,r,s,t)\in S$.

  2. 2.

For all $(q_{1},r_{1},s_{1},t_{1}),(q_{2},r_{2},s_{2},t_{2})\in S$, if
$r_{1}=q_{2}$ and $t_{1}=s_{2}$, then $(q_{1},r_{2},s_{1},t_{2})\in S$.

######  Proof 3.6.

Let $S\subseteq Q^{4}$ be the least set containing
$\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{G},\mathcal{A}]$ and
satisfying both conditions. We prove that
$S=\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{A}]$. For
$S\subseteq\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{A}]$, since
$\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{G},\mathcal{A}]\subseteq\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{A}]$
by definition, it suffices to prove that
$\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{A}]$ satisfies both
conditions in the proposition. First, consider $a\in A$ and $q,r,s,t\in Q$
such that $(q,a,r),(s,a,t)\in\delta$. We have $a\in L_{\mathcal{A}}(q,r)$ and
$a\in L_{\mathcal{A}}(s,t)$. Hence, they are not
$\mathit{BPol}(\mathcal{C})$-separable and
$(q,r,s,t)\in\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{A}]$. Now, let
$(q_{1},r_{1},s_{1},t_{1}),(q_{2},r_{2},s_{2},t_{2})\in\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{A}]$
such that $r_{1}=q_{2}$ and $t_{1}=s_{2}$. For $i\in\\{1,2\\}$, we know that
$L_{\mathcal{A}}(q_{i},r_{i})$ is not $\mathit{BPol}(\mathcal{C})$-separable
from $L_{\mathcal{A}}(s_{i},t_{i})$. Since $\mathit{BPol}(\mathcal{C})$ is a
prevariety by Theorem 2.2, it follows from Lemma 3.1 that
$L_{\mathcal{A}}(q_{1},r_{1})L_{\mathcal{A}}(q_{2},r_{2})$ is not
$\mathit{BPol}(\mathcal{C})$ separable from
$L_{\mathcal{A}}(s_{1},t_{1})L_{\mathcal{A}}(s_{2},t_{2})$. Since
$r_{1}=q_{2}$ and $t_{1}=s_{2}$, it is immediate that
$L_{\mathcal{A}}(q_{1},r_{1})L_{\mathcal{A}}(q_{2},r_{2})\subseteq
L_{\mathcal{A}}(q_{1},r_{2})$ and
$L_{\mathcal{A}}(s_{1},t_{1})L_{\mathcal{A}}(s_{2},t_{2})\subseteq
L_{\mathcal{A}}(s_{1},t_{2})$. Hence, $L_{\mathcal{A}}(q_{1},r_{2})$ is not
$\mathit{BPol}(\mathcal{C})$-separable from $L_{\mathcal{A}}(s_{1},t_{2})$ and
we get
$(q_{1},r_{2},s_{1},t_{2})\in\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{A}]$
as desired.

We turn to the inclusion
$\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{A}]\subseteq S$. By Lemma
3.4, there exists $L\in\mathcal{G}$ such that $\varepsilon\in L$ and a
$\mathit{BPol}(\mathcal{C})$-cover $\mathbf{V}$ of $L$ which is separating for
$\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{G},\mathcal{A}]$. By
hypothesis, $L$ is a group language and $\varepsilon\in L$. Hence, Proposition
2.6 yields a cover $\mathbf{P}$ of $A^{*}$ such that every $P\in\mathbf{P}$ is
of the form $P=\mathord{\uparrow}_{L}w_{P}$ for some word $w_{P}\in A^{*}$.
Let $P\in\mathbf{P}$ and $a_{1},\dots,a_{n}\in A$ be the letters such that
$w_{P}=a_{1}\cdots a_{n}$. We have $P=La_{1}L\cdots a_{n}L$ by definition (if
$w_{P}=\varepsilon$, then $P=L$). By definition,
$L\in\mathcal{G}\subseteq\mathit{Pol}(\mathcal{C})$. Hence, since $\mathbf{V}$
is a $\mathit{BPol}(\mathcal{C})$-cover of $L$, Proposition 2.5 yields a
$\mathit{BPol}(\mathcal{C})$-cover $\mathbf{K}_{P}$ of $P$ such that for every
$K\in\mathbf{K}_{P}$, there are $V_{0},\dots,V_{n}\in\mathbf{V}$ such that
$K\subseteq V_{0}a_{1}V_{1}\cdots a_{n}V_{n}$. We let
$\mathbf{K}=\bigcup_{P\in\mathbf{P}}\mathbf{K}_{P}$. Since $\mathbf{P}$ is a
cover of $A^{*}$ and $\mathbf{K}_{P}$ is a $\mathit{BPol}(\mathcal{C})$-cover
of $P$ for each $P\in\mathbf{P}$, $\mathbf{K}$ is a
$\mathit{BPol}(\mathcal{C})$-cover of $A^{*}$. We show that $\mathbf{K}$ is
separating for $S$ which implies that
$\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{A}]\subseteq S$ by Lemma
3.3.

Let $(q,r,s,t)\in Q^{4}$ and $K\in\mathbf{K}$ such that we have $x\in K\cap
L_{\mathcal{A}}(q,r)$ and $y\in K\cap L_{\mathcal{A}}(s,t)$. We show that
$(q,r,s,t)\in S$. We have $K\in\mathbf{K}_{P}$ for some $P\in\mathbf{P}$. Let
$a_{1},\dots,a_{n}\in A$ such that $w_{P}=a_{1}\cdots a_{n}$. By definition,
there are $V_{0},\dots,V_{n}\in\mathbf{V}$ such that $K\subseteq
V_{0}a_{1}V_{1}\cdots a_{n}V_{n}$. Since $x,y\in K$, we get $x_{i},y_{i}\in
V_{i}$ for $0\leq i\leq n$ such that $x=x_{0}a_{1}x_{1}\cdots a_{n}x_{n}$ and
$y=y_{0}a_{1}y_{1}\cdots a_{n}y_{n}$. Since $x\in L_{\mathcal{A}}(q,r)$, we
get $q_{i},r_{i}\in Q$ for $0\leq i\leq n$ such that $q_{0}=q$, $r_{n}=r$,
$x_{i}\in L_{\mathcal{A}}(q_{i},r_{i})$ for $0\leq i\leq n$ and
$(r_{i-1},a_{i},q_{i})\in\delta$ for $1\leq i\leq n$. Finally, since $y\in
L_{\mathcal{A}}(s,t)$, we get $s_{i},t_{i}\in Q$ for $0\leq i\leq n$ such that
$s_{0}=s$, $t_{n}=t$, $y_{i}\in L_{\mathcal{A}}(s_{i},t_{i})$ for $0\leq i\leq
n$ and $(t_{i-1},a_{i},s_{i})\in\delta$ for $1\leq i\leq n$. Since $S$
satisfies Condition 1 in the proposition, we get
$(r_{i-1},q_{i},t_{i-1},s_{i})\in S$ for $1\leq i\leq n$. Since
$V_{i}\in\mathbf{V}$ which is separating for
$\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{G},\mathcal{A}]$ and
$x_{i},y_{i}\in V_{i}$, we also get
$(q_{i},r_{i},q_{i},t_{i})\in\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{G},\mathcal{A}]$
for $0\leq i\leq n$. Thus, Condition 2 in the proposition yields
$(q_{0},r_{0},s_{n},t_{n})\in S$, _i.e._ $(q,r,s,t)\in S$ as desired.

Proposition 3.5 provides a least fixpoint algorithm for computing the set
$\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{A}]$ from
$\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{G},\mathcal{A}]$. Combined
with Proposition 3.2, this yields a polynomial time reduction from
$\mathit{BPol}(\mathcal{C})$-separation to computing
$\mathcal{I}_{\mathit{BPol}(\mathcal{C})}[\mathcal{G},\mathcal{A}]$ from an
NFA. We shall prove that when
$\mathcal{C}\in\\{\mathcal{G},\mathcal{G}^{+}\\}$, there are polynomial time
reductions of the latter problem to $\mathcal{G}$-separation.

###  3.2 Tuple separation

This generalized variant of separation is taken from [18]. We shall use it as
a proof ingredient: for every lattice $\mathcal{C}$, it is connected to the
classical separation problem for $\mathit{Bool}(\mathcal{C})$. For every
$n\geq 1$, we call “ _$n$ -tuple_” a tuple of $n$ languages
$(L_{1},\dots,L_{n})$. In the sequel, given another language $K$, we shall
write $(L_{1},\dots,L_{n})\cap K$ for the $n$-tuple $(L_{1}\cap
K,\dots,L_{n}\cap K)$. Let $\mathcal{C}$ be a lattice, we use induction on $n$
to define the _$\mathcal{C}$ -separable $n$-tuples_:

  * •

If $n=1$, a $1$-tuple $(L_{1})$ is $\mathcal{C}$-separable when
$L_{1}=\emptyset$.

  * •

If $n\geq 2$, an $n$-tuple $(L_{1},\dots,L_{n})$ is $\mathcal{C}$-separable
when there exists $K\in\mathcal{C}$ such that $L_{1}\subseteq K$ and
$(L_{2},\dots,L_{n})\cap K$ is $\mathcal{C}$-separable. We call $K$ a
_separator_ of $(L_{1},\dots,L_{n})$.

One may verify that classical separation is the special case $n=2$. We
generalize $\mathcal{D}$-controlled separation to this setting. For a class
$\mathcal{D}$, we say that an $n$-tuple $(L_{1},\dots,L_{n})$ is
$\mathcal{C}$-separable under $\mathcal{D}$-control if there exists
$H\in\mathcal{D}$ such that $\varepsilon\in H$ and $(L_{1},\dots,L_{n})\cap H$
is $\mathcal{C}$-separable.

We complete the definition with two simple properties of tuple separation (see
Appendix B for the proofs). The second one is based on closure under quotients
and generalizes Lemma 3.1.

######  Lemma 3.7.

Let $\mathcal{C}$ be a lattice and let
$(L_{1},\dots,L_{n}),(H_{1},\dots,H_{n})$ be two $n$-tuples. If
$L_{1}\cap\cdots\cap L_{n}\neq\emptyset$, then $(L_{1},\dots,L_{n})$ is not
$\mathcal{C}$-separable. Moreover, if $L_{i}\subseteq H_{i}$ for every $i\leq
n$ and $(L_{1},\dots,L_{n})$ is not $\mathcal{C}$-separable, then
$(H_{1},\dots,H_{n})$ is not $\mathcal{C}$-separable either.

######  Lemma 3.8.

Let $\mathcal{C}$ be a positive prevariety, $n\geq 1$ and let
$(L_{1},\dots,L_{n}),(H_{1},\dots,H_{n})$ be two $n$-tuples, which are not
$\mathcal{C}$-separable. Then, $(L_{1}H_{1},\dots,L_{n}H_{n})$ is not
$\mathcal{C}$-separable either.

A theorem of [18] connects tuple $\mathcal{C}$-separation for a lattice
$\mathcal{C}$ to $\mathit{Bool}(\mathcal{C})$-separation: $L_{0}$ is
$\mathit{Bool}(\mathcal{C})$-separable from $L_{1}$ if and only if
$(L_{0},L_{1})^{p}$ is $\mathcal{C}$-separable for some $p\geq 1$. Here,
$(L_{0},L_{1})^{p}$ denotes the $2p$-tuple obtained by concatenating $p$
copies of $(L_{0},L_{1})$. For example,
$(L_{0},L_{1})^{3}=(L_{0},L_{1},L_{0},L_{1},L_{0},L_{1})$. We use a corollary
applying to $\mathcal{D}$-controlled separation. Proofs for both the original
theorem of [18] and the corollary are available in Appendix B.

######  Corollary 3.9.

Let $\mathcal{C}$ and $\mathcal{D}$ be two lattices such that
$\mathcal{D}\subseteq\mathcal{C}$ and let $L_{0},L_{1}\subseteq A^{*}$. The
following properties are equivalent:

  1. 1.

$L_{0}$ is $\mathit{Bool}(\mathcal{C})$-separable from $L_{1}$ under
$\mathcal{D}$-control.

  2. 2.

There exists $p\geq 1$ such that $(L_{0},L_{1})^{p}$ is
$\mathcal{C}$-separable under $\mathcal{D}$-control.

We only use the contrapositive of $1)\Rightarrow 2)$ in Corollary 3.9. We
complete the presentation with two important lemmas about tuple separation for
$\mathit{Pol}(\mathcal{D})$ and $\mathit{Pol}(\mathcal{D}^{+})$. We use them
to prove that tuples are not separable (see Appendix B for the proofs). Note
that in practice, $\mathcal{D}$ will be a group prevariety $\mathcal{G}$. Yet,
the results are true regardless of this hypothesis.

######  Lemma 3.10.

Let $\mathcal{D}$ be a prevariety and $(L_{1},\dots,L_{n})$ an $n$-tuple which
is not $\mathit{Pol}(\mathcal{D})$-separable under $\mathcal{D}$-control.
Then, $(\\{\varepsilon\\},L_{1},\dots,L_{n})$ is not
$\mathit{Pol}(\mathcal{D})$-separable.

######  Lemma 3.11.

Let $\mathcal{D}$ be a prevariety and $w\in A^{+}$. If $(L_{1},\dots,L_{n})$
is not $\mathit{Pol}(\mathcal{D}^{+})$-separable under $\mathcal{D}$-control,
then $(w^{+},w^{+}L_{1}w^{+},\dots,w^{+}L_{n}w^{+})$ is not
$\mathit{Pol}(\mathcal{D}^{+})$-separable.

##  4 Separation Algorithms for $\mathit{BPol}(\mathcal{G})$ and
$\mathit{BPol}(\mathcal{G}^{+})$

For a group prevariety $\mathcal{G}$, we now consider
$\mathit{BPol}(\mathcal{G})$\- and
$\mathit{BPol}(\mathcal{G}^{+})$-separation. We rely on the notions of Section
3: given an arbitrary NFA $\mathcal{A}=(Q,\delta)$, we present a generic
characterization of the inseparable $\mathit{BPol}(\mathcal{G})$\- and
$\mathit{BPol}(\mathcal{G}^{+})$-quadruples under $\mathcal{G}$ control
associated to $\mathcal{A}$, _i.e._ , of the subsets
$\mathcal{I}_{\mathit{BPol}(\mathcal{G})}[\mathcal{G},\mathcal{A}]$ and
$\mathcal{I}_{\mathit{BPol}(\mathcal{G}^{+})}[\mathcal{G},\mathcal{A}]$ of
$Q^{4}$. Thanks to Proposition 3.5, this also yields characterizations of
$\mathcal{I}_{\mathit{BPol}(\mathcal{G})}[\mathcal{A}]$ and of
$\mathcal{I}_{\mathit{BPol}(\mathcal{G}^{+})}[\mathcal{A}]$, which in turn, in
view of Proposition 3.2, yield reductions from both
$\mathit{BPol}(\mathcal{G})$\- and $\mathit{BPol}(\mathcal{G}^{+})$-separation
to $\mathcal{G}$-separation. These polynomial time reductions are therefore
_effective_ when $\mathcal{G}$-separation is decidable.

###  4.1 Statements

Let $\mathcal{G}$ be a group prevariety and let $\mathcal{A}=(Q,\delta)$ be an
NFA. We present characterizations of
$\mathcal{I}_{\mathit{BPol}(\mathcal{G})}[\mathcal{G},\mathcal{A}]$ and
$\mathcal{I}_{\mathit{BPol}(\mathcal{G}^{+})}[\mathcal{G},\mathcal{A}]$. They
follow the same pattern, but each of them depends on a specific function from
$2^{{Q^{4}}}$ to $2^{{Q^{4}}}$, which we first describe.

Characterization of
$\mathcal{I}_{\mathit{BPol}(\mathcal{G})}[\mathcal{G},\mathcal{A}]$. We use a
function $\tau_{\mathcal{A},\mathcal{G}}:2^{{Q^{4}}}\to 2^{{Q^{4}}}$. For
$S\subseteq Q^{4}$, we define the set
$\tau_{\mathcal{A},\mathcal{G}}(S)\subseteq Q^{4}$. The definition is based on
an auxiliary NFA $\mathcal{B}_{S}=(Q^{3},\gamma_{S})$ _with
$\varepsilon$-transitions_, which depends on $S$. Its states are triples in
$Q^{3}$. The set $\gamma_{S}\subseteq
Q^{3}\times(A\cup\\{\varepsilon\\})\times Q^{3}$ includes two kinds of
transitions. First, given $a\in A$ and
$s_{1},s_{2},s_{3},\,t_{1},t_{2},t_{3}\in Q$, we let
$\big{(}(s_{1},s_{2},s_{3}),a,(t_{1},t_{2},t_{3})\big{)}\in\gamma_{S}$ if and
only if $(s_{1},a,t_{1})\in\delta$, $(s_{2},a,t_{2})\in\delta$ and
$(s_{3},a,t_{3})\in\delta$. Second, for every state $q_{1}\in Q$ and every
$(q_{2},r_{2},q_{3},r_{3})\in S$, we add the following
$\varepsilon$-transition:
$((q_{1},q_{2},q_{3}),\varepsilon,(q_{1},r_{2},r_{3}))\in\gamma_{S}$. We
represent this construction process graphically in Figure 1.

$s_{1}$$t_{1}$$s_{2}$$t_{2}$$s_{3}$$t_{3}$$a$$a$$a$Transitions in
$\mathcal{A}$ $(s_{1},s_{2},s_{3})$$(t_{1},t_{2},t_{3})$$a$Produced transition
in $\mathcal{B}_{S}$$q_{1}\in Q$ and $(q_{2},r_{2},q_{3},r_{3})\in
S$$s_{1}$$t_{1}$$s_{2}$$t_{2}$$s_{3}$$t_{3}$$a$$a$$a$Single state and
quadruple in $S$$q_{1}\in Q\ $ and $\ (q_{2},r_{2},q_{3},r_{3})\in
S$$(q_{1},q_{2},q_{3})$$(q_{1},r_{2},r_{3})$$\varepsilon$Produced
$\varepsilon$-transition in $\mathcal{B}_{S}$ Figure 1: Construction of the
transitions in the auxiliary automaton $\mathcal{B}_{S}$

######  Remark 4.1.

The NFA $\mathcal{B}_{S}$ and its counterpart $\mathcal{B}_{S}^{+}$ (which we
define below as a means to handle $\mathit{BPol}(\mathcal{G}^{+})$) are the
_only_ NFAs with $\varepsilon$-transitions considered in the paper. In
particular, the original input NFA $\mathcal{A}$ is assumed to be _without_
$\varepsilon$-transitions.

We are ready to define $\tau_{\mathcal{A},\mathcal{G}}(S)\subseteq Q^{4}$. For
every $(q,r,s,t)\in Q^{4}$, we let
$(q,r,s,t)\in\tau_{\mathcal{A},\mathcal{G}}(S)$ if and only if the two
following conditions hold:

$\begin{array}[]{l}\text{$\\{\varepsilon\\}$ is \emph{not}
$\mathcal{G}$-separable from $L_{\mathcal{B}_{S}}((s,q,s),(t,r,t))$, and}\\\
\text{$\\{\varepsilon\\}$ is \emph{not} $\mathcal{G}$-separable from
$L_{\mathcal{B}_{S}}((q,s,q),(r,t,r))$}.\end{array}$ (1)

A set $S\subseteq Q^{4}$ is _$(\mathit{BPol},*)$ -sound_ for $\mathcal{G}$ and
$\mathcal{A}$ if it is a fixpoint for $\tau_{\mathcal{A},\mathcal{G}}$, _i.e._
$\tau_{\mathcal{A},\mathcal{G}}(S)=S$. We have the following simple lemma
which can be verified from the definition (see Appendix C for the proof). It
states that $\tau_{\mathcal{A},\mathcal{G}}:2^{{Q^{4}}}\to 2^{{Q^{4}}}$ is
_increasing_ (for inclusion). In particular, this implies that it has a
_greatest fixpoint_ , _i.e._ , there is a _greatest $(\mathit{BPol},*)$-sound
set_.

######  Lemma 4.2.

Let $\mathcal{G}$ be a group prevariety and let $\mathcal{A}=(Q,\delta)$ be an
NFA. For every $S,S^{\prime}\subseteq Q^{4}$, we have $S\subseteq
S^{\prime}\Rightarrow\tau_{\mathcal{A},\mathcal{G}}(S)\subseteq\tau_{\mathcal{A},\mathcal{G}}(S^{\prime})$.

We may now state the first key theorem of the paper. It applies to
$\mathit{BPol}(\mathcal{G})$-separation.

######  Theorem 4.3.

Let $\mathcal{G}$ be a group prevariety and $\mathcal{A}=(Q,\delta)$ an NFA.
Then, $\mathcal{I}_{\mathit{BPol}(\mathcal{G})}[\mathcal{G},\mathcal{A}]$ is
the greatest $(\mathit{BPol},*)$-sound subset of $Q^{4}$ for $\mathcal{G}$ and
$\mathcal{A}$.

Characterization of
$\mathcal{I}_{\mathit{BPol}(\mathcal{G}^{+})}[\mathcal{G},\mathcal{A}]$. The
characterization of
$\mathcal{I}_{\mathit{BPol}(\mathcal{G}^{+})}[\mathcal{G},\mathcal{A}]$ is
analogous. Roughly, the only difference is that we modify the definition of
the auxiliary automaton $\mathcal{B}_{S}$. Let $\mathcal{G}$ be a group
prevariety and $\mathcal{A}=(Q,\delta)$ be an NFA. We define a new function
$\tau^{+}_{\mathcal{A},\mathcal{G}}:2^{Q^{4}}\to 2^{Q^{4}}$. For $S\subseteq
Q^{4}$, we define $\tau^{+}_{\mathcal{A},\mathcal{G}}(S)\subseteq Q^{4}$ using
another auxiliary NFA $\mathcal{B}^{+}_{S}=(Q^{3},\gamma^{+}_{S})$ _with
$\varepsilon$-transitions_. Its states are triples in $Q^{3}$ and
$\gamma^{+}_{S}\subseteq Q^{3}\times(A\cup\\{\varepsilon\\})\times Q^{3}$
contains two kinds of transitions. First, for $a\in A$ and
$s_{1},s_{2},s_{3},t_{1},t_{2},t_{3}\in Q$, we let
$\big{(}(s_{1},s_{2},s_{3}),a,(t_{1},t_{2},t_{3})\big{)}\in\gamma^{+}_{S}$ if
and only if $(s_{1},a,t_{1})\in\delta$, $(s_{2},a,t_{2})\in\delta$ and
$(s_{3},a,t_{3})\in\delta$. Second, for all $q_{1}\in Q$ and all
$(q_{2},r_{2},q_{3},r_{3})\in S$, if $A^{+}\cap
L_{\mathcal{A}}(q_{1},q_{1})\cap L_{\mathcal{A}}(q_{2},q_{2})\cap
L_{\mathcal{A}}(q_{3},q_{3})\cap L_{\mathcal{A}}(r_{2},r_{2})\cap
L_{\mathcal{A}}(r_{3},r_{3})\neq\emptyset$, then we add the following
$\varepsilon$-transition:
$((q_{1},q_{2},q_{3}),\varepsilon,(q_{1},r_{2},r_{3}))\in\gamma^{+}_{S}$. We
represent this construction in Figure 2.

$s_{1}$$t_{1}$$s_{2}$$t_{2}$$s_{3}$$t_{3}$$a$$a$$a$Transitions in
$\mathcal{A}$ $(s_{1},s_{2},s_{3})$$(t_{1},t_{2},t_{3})$$a$Produced transition
in
$\mathcal{B}^{+}_{S}$$s_{1}$$t_{1}$$s_{2}$$t_{2}$$s_{3}$$t_{3}$$a$$a$$a$$q_{1}\in
Q,(q_{2},r_{2},q_{3},r_{3})\in S$ and $z\in A^{+}$such
that$q_{1}$$z$$q_{2}$$z$$r_{2}$$z$$q_{3}$$z$$r_{3}$$z$Single state and
quadruple in
$S$$(q_{1},q_{2},q_{3})$$(q_{1},r_{2},r_{3})$$\varepsilon$Produced
$\varepsilon$-transition in $\mathcal{B}^{+}_{S}$ Figure 2: Construction of
the transitions in the auxiliary automaton $\mathcal{B}^{+}_{S}$

We are ready to define $\tau^{+}_{\mathcal{A},\mathcal{G}}(S)\subseteq Q^{4}$.
For every $(q,r,s,t)\in Q^{4}$, we let
$(q,r,s,t)\in\tau^{+}_{\mathcal{A},\mathcal{G}}(S)$ if and only if the two
following conditions hold:

$\begin{array}[]{l}\text{$\\{\varepsilon\\}$ is \emph{not}
$\mathcal{G}$-separable from $L_{\mathcal{B}^{+}_{S}}((s,q,s),(t,r,t))$,
and}\\\ \text{$\\{\varepsilon\\}$ is \emph{not} $\mathcal{G}$-separable from
$L_{\mathcal{B}^{+}_{S}}((q,s,q),(r,t,r))$}.\end{array}$ (2)

A set $S\subseteq Q^{4}$ is _$(\mathit{BPol},+)$ -sound_ for $\mathcal{G}$ and
$\mathcal{A}$ if it is a fixpoint for $\tau^{+}_{\mathcal{A},\mathcal{G}}$,
_i.e._ $\tau^{+}_{\mathcal{A},\mathcal{G}}(S)=S$. The following monotonicity
lemma implies that there is a _greatest $(\mathit{BPol},+)$-sound set_ (see
Appendix C).

######  Lemma 4.4.

Let $\mathcal{G}$ be a group prevariety and $\mathcal{A}=(Q,\delta)$ an NFA.
For every $S,S^{\prime}\subseteq Q^{4}$, we have $S\subseteq
S^{\prime}\Rightarrow\tau^{+}_{\mathcal{A},\mathcal{G}}(S)\subseteq\tau^{+}_{\mathcal{A},\mathcal{G}}(S^{\prime})$.

We may now state our second key theorem. It applies to
$\mathit{BPol}(\mathcal{G}^{+})$-separation.

######  Theorem 4.5.

Let $\mathcal{G}$ be a group prevariety and $\mathcal{A}=(Q,\delta)$ an NFA.
Then, $\mathcal{I}_{\mathit{BPol}(\mathcal{G}^{+})}[\mathcal{G},\mathcal{A}]$
is the greatest $(\mathit{BPol},+)$-sound subset of $Q^{4}$ for $\mathcal{G}$
and $\mathcal{A}$.

Let us discuss the consequences of Theorems 4.3 and 4.5. Since
$\mathcal{B}_{S}$ and $\mathcal{B}^{+}_{S}$ can be computed from $\mathcal{A}$
and $S$, one can compute $\tau_{\mathcal{A},\mathcal{G}}(S)$ and
$\tau^{+}_{\mathcal{A},\mathcal{G}}(S)$ from $S$ provided that
$\mathcal{G}$-separation is decidable. Hence, if $\mathcal{G}$-separation is
decidable, Theorem 4.3 (resp. Theorem 4.5) yields a _greatest_ fixpoint
procedure for computing
$\mathcal{I}_{\mathit{BPol}(\mathcal{G})}[\mathcal{G},\mathcal{A}]$ (resp.
$\mathcal{I}_{\mathit{BPol}(\mathcal{G}^{+})}[\mathcal{G},\mathcal{A}]$).
Indeed, consider the sequence of subsets defined by $S_{0}=Q^{4}$, and
$S_{n}=\tau_{\mathcal{A},\mathcal{G}}(S_{n-1})$ for $n\geq 1$. By definition,
computing $S_{n}$ from $S_{n-1}$ boils down to deciding
$\mathcal{G}$-separation. Since $\tau_{\mathcal{A},\mathcal{G}}$ is increasing
by Lemma 4.2, we get a decreasing sequence $Q^{4}=S_{0}\supseteq
S_{1}\supseteq S_{2}\cdots$. Moreover, since $Q^{4}$ is finite, this sequence
stabilizes at some point: there exists $n\in{\rm Nature}$ such that
$S_{n}=S_{j}$ for all $j\geq n$. One may verify that $S_{n}$ is the greatest
$(\mathit{BPol},*)$-sound subset of $Q^{4}$. By Theorem 4.3, it follows that
$S_{n}=\mathcal{I}_{\mathit{BPol}(\mathcal{G})}[\mathcal{G},\mathcal{A}]$.
Likewise, the sequence $T_{n}$ defined by $T_{0}=Q^{4}$ and
$T_{n}=\tau^{+}_{\mathcal{A},\mathcal{G}}(T_{n-1})$ is computable when
$\mathcal{G}$-separation is decidable, and, since it is decreasing, it
stabilizes. By Theorem 4.5, its stabilization value is
$\mathcal{I}_{\mathit{BPol}(\mathcal{G}^{+})}[\mathcal{G},\mathcal{A}]$.

By Proposition 3.5, $\mathcal{I}_{\mathit{BPol}(\mathcal{G})}[\mathcal{A}]$
(resp. $\mathcal{I}_{\mathit{BPol}(\mathcal{G}^{+})}[\mathcal{A}]$) can be
computed from
$\mathcal{I}_{\mathit{BPol}(\mathcal{G})}[\mathcal{G},\mathcal{A}]$ (resp.
$\mathcal{I}_{\mathit{BPol}(\mathcal{G}^{+})}[\mathcal{G},\mathcal{A}]$) via a
_least_ fixpoint procedure. Altogether, by Proposition 3.2, we get reductions
from $\mathit{BPol}(\mathcal{G})$\- and
$\mathit{BPol}(\mathcal{G}^{+})$-separation to $\mathcal{G}$-separation. One
may verify that these are polynomial time reductions (we mean “reduction” in
the Turing sense: $\mathit{BPol}(\mathcal{G})$\- and
$\mathit{BPol}(\mathcal{G}^{+})$-separation can be decided in polynomial time
using an oracle for $\mathcal{G}$-separation).

Now, it is known that separation can be decided in polynomial time for the
classes ST, MOD and GR (this is trivial for ST, see [25] for MOD and GR).
Hence, we obtain from Theorem 4.3 that separation is decidable in polynomial
time for $\mathit{BPol}(\textup{ST})$ (_i.e._ , $\mathcal{B}\Sigma_{1}(<)$),
$\mathit{BPol}(\textup{MOD})$ (_i.e._ ,
$\mathcal{B}\Sigma_{1}(<,\mathit{MOD})$) and $\mathit{BPol}(\textup{GR})$.
This was well-know for $\mathit{BPol}(\textup{ST})$ (the class of piecewise
testable languages, see [6, 17]). For the other two, decidability was known
[35, 21] but not the polynomial time upper bound. Using Theorem 4.5, we also
obtain that separation is decidable in polynomial time for
$\mathit{BPol}(\textup{ST}^{+})$ (_i.e._ , the languages of dot-depth one or
equivalently $\mathcal{B}\Sigma_{1}(<,+1)$), $\mathit{BPol}(\textup{MOD}^{+})$
(_i.e._ , $\mathcal{B}\Sigma_{1}(<,+1,\mathit{MOD})$) and
$\mathit{BPol}(\textup{GR}^{+})$. Decidability was already known for
$\mathit{BPol}(\textup{ST}^{+})$ and $\mathit{BPol}(\textup{MOD}^{+})$: the
results can be obtained indirectly by reduction to
$\mathit{BPol}(\textup{ST})$-separation using transfer theorems [22, 16]. Yet,
the polynomial time upper bounds are new as the transfer theorems have a
built-in exponential blow-up. Moreover, decidability of separation is a new
result for $\mathit{BPol}(\textup{GR}^{+})$.

Finally, the statement applies to $\mathit{BPol}(\textup{AMT})$ and
$\mathit{BPol}(\textup{AMT}^{+})$ (_i.e._ ,
$\mathcal{B}\Sigma_{1}(<,\mathit{AMOD})$ and
$\mathcal{B}\Sigma_{1}(<,+1,\mathit{AMOD})$). This is a new result for
$\mathit{BPol}(\textup{AMT}^{+})$. Yet, since AMT-separation is co-NP-complete
when the alphabet is part of the input [25] (the problem being in P for a
fixed alphabet), the complexity analysis is not entirely immediate. However,
one may verify that the procedures yield co-NP algorithms for both
$\mathit{BPol}(\textup{AMT})$\- and
$\mathit{BPol}(\textup{AMT}^{+})$-separation. We summarize the upper bounds in
Figure 3.

Input class $\mathcal{G}$ ST MOD AMT GR $\mathit{BPol}(\mathcal{G})$\- and
$\mathit{BPol}(\mathcal{G}^{+})$-separation P P co-NP P Figure 3: Complexity
of separation (for input languages represented by NFAs).

###  4.2 Proof of Theorem 4.3

We now concentrate on the proof of Theorem 4.3. The key ingredients in this
argument are Proposition 2.6 and Lemma 3.10. On the other hand, the proof of
Theorem 4.5 is postponed to Appendix C. It is based on similar ideas. Roughly,
we replace Proposition 2.6 and Lemma 3.10 (which are tailored to classes
$\mathit{BPol}(\mathcal{G})$) by their counterparts for
$\mathit{BPol}(\mathcal{G}^{+})$: Proposition 2.7 and Lemma 3.11. However,
note that proving Theorem 4.5 is technically more involved as manipulating the
automaton $\mathcal{B}_{S}^{+}$ in the definition of
$\tau^{+}_{\mathcal{A},\mathcal{G}}$ requires more work.

We fix a group prevariety $\mathcal{G}$ and an NFA $\mathcal{A}=(Q,\delta)$.
Let $S\subseteq Q^{4}$ be the greatest $(\mathit{BPol},*)$-sound subset for
$\mathcal{G}$ and $\mathcal{A}$. We prove that
$S=\mathcal{I}_{\mathit{BPol}(\mathcal{G})}[\mathcal{G},\mathcal{A}]$.

First part:
$S\subseteq\mathcal{I}_{\mathit{BPol}(\mathcal{G})}[\mathcal{G},\mathcal{A}]$.
We use _tuple separation_ and Lemma 3.10. Let us start with some terminology.
For every $n\geq 1$ and $(q_{1},r_{1},q_{2},r_{2})\in Q^{4}$, we associate an
$n$-tuple of languages, written $T_{n}(q_{1},r_{1},q_{2},r_{2})$. We use
induction on $n$ and tuple concatenation to present the definition. If $n=1$
then,
$T_{1}(q_{1},r_{1},q_{2},r_{2})=\big{(}L_{\mathcal{A}}(q_{2},r_{2})\big{)}$.
If $n>1$, then,

$T_{n}(q_{1},r_{1},q_{2},r_{2})=\left\\{\begin{array}[]{ll}(L_{\mathcal{A}}(q_{2},r_{2}))\cdot
T_{n-1}(q_{1},r_{1},q_{2},r_{2})&\text{if $n$ is odd}\\\
(L_{\mathcal{A}}(q_{1},r_{1}))\cdot T_{n-1}(q_{1},r_{1},q_{2},r_{2})&\text{if
$n$ is even.}\end{array}\right.$

For example, we have
$T_{3}(q_{1},r_{1},q_{2},r_{2})=(L_{\mathcal{A}}(q_{2},r_{2}),L_{\mathcal{A}}(q_{1},r_{1}),L_{\mathcal{A}}(q_{2},r_{2}))$.

######  Proposition 4.6.

For every $n\geq 1$ and $(q_{1},r_{1},q_{2},r_{2})\in S$, the $n$-tuple
$T_{n}(q_{1},r_{1},q_{2},r_{2})$ is not $\mathit{Pol}(\mathcal{G})$-separable
under $\mathcal{G}$-control.

By definition, Proposition 4.6 implies that for all $p\geq 1$ and
$(q_{1},r_{1},q_{2},r_{2})\in S$, the $2p$-tuple
$(L_{\mathcal{A}}(q_{1},r_{1}),L_{\mathcal{A}}(q_{2},r_{2}))^{p}$ is not
$\mathit{Pol}(\mathcal{G})$-separable under $\mathcal{G}$-control. By
Corollary 3.9, it follows that $L_{\mathcal{A}}(q_{1},r_{1})$ is not
$\mathit{BPol}(\mathcal{G})$-separable from $L_{\mathcal{A}}(q_{2},r_{2})$
under $\mathcal{G}$-control, _i.e._ , that
$(q_{1},r_{1},q_{2},r_{2})\in\mathcal{I}_{\mathit{BPol}(\mathcal{G})}[\mathcal{G},\mathcal{A}]$.
We get
$S\subseteq\mathcal{I}_{\mathit{BPol}(\mathcal{G})}[\mathcal{G},\mathcal{A}]$
as desired.

We prove Proposition 4.6 by induction on $n$. We fix $n\geq 1$ for the proof.
In order to exploit the hypothesis that $S$ is $(\mathit{BPol},*)$-sound, we
need a property of the NFA $\mathcal{B}_{S}=(Q^{3},\gamma_{S})$ used to define
$\tau_{\mathcal{A},\mathcal{G}}$. When $n\geq 2$, this is where we use
induction on $n$ and Lemma 3.10.

######  Lemma 4.7.

Let $(s_{1},s_{2},s_{3}),(t_{1},t_{2},t_{3})\in Q^{3}$ and $w\in
L_{\mathcal{B}_{S}}((s_{1},s_{2},s_{3}),(t_{1},t_{2},t_{3}))$. Then, $w\in
L_{\mathcal{A}}(s_{1},t_{1})$ and, if $n\geq 2$, the $n$-tuple $(\\{w\\})\cdot
T_{n-1}(s_{2},t_{2},s_{3},t_{3})$ is not
$\mathit{Pol}(\mathcal{G})$-separable.

######  Proof 4.8.

Since $w\in L_{\mathcal{B}_{S}}((s_{1},s_{2},s_{3}),(t_{1},t_{2},t_{3}))$,
there exists a run labeled by $w$ from $(s_{1},s_{2},s_{3})$ to
$(t_{1},t_{2},t_{3})$ in $\mathcal{B}_{S}$. We use a sub-induction on the
number of transitions involved in that run. First, assume that no transitions
are used: we have $w=\varepsilon$ and
$(s_{1},s_{2},s_{3})=(t_{1},t_{2},t_{3})$. Clearly, $\varepsilon\in
L_{\mathcal{A}}(s_{1},s_{1})$ and, if $n\geq 2$, the $n$-tuple
$(\\{\varepsilon\\})\cdot T_{n-1}(s_{2},s_{2},s_{3},s_{3})$ is not
$\mathit{Pol}(\mathcal{G})$-separable by Lemma 3.7 since $\varepsilon\in
L_{\mathcal{A}}(s_{2},s_{2})\cap L_{\mathcal{A}}(s_{3},s_{3})$. We now assume
that at least one transition is used and consider the last one: we have
$(q_{1},q_{2},q_{3})\in Q^{3}$, $w^{\prime}\in A^{*}$ and $x\in
A\cup\\{\varepsilon\\}$ such that $w=w^{\prime}x$, $w^{\prime}\in
L_{\mathcal{B}_{S}}((s_{1},s_{2},s_{3}),(q_{1},q_{2},q_{3}))$ and
$((q_{1},q_{2},q_{3}),x,(t_{1},t_{2},t_{3}))\in\gamma_{S}$. By induction, we
have $w^{\prime}\in L_{\mathcal{A}}(s_{1},q_{1})$ and, if $n\geq 2$, the
$n$-tuple $(\\{w^{\prime}\\})\cdot T_{n-1}(s_{2},q_{2},s_{3},q_{3})$ is not
$\mathit{Pol}(\mathcal{G})$-separable. We prove that $x\in
L_{\mathcal{A}}(q_{1},t_{1})$ and, if $n\geq 2$, the $n$-tuple $(\\{x\\})\cdot
T_{n-1}(q_{2},t_{2},q_{3},t_{3})$ is not
$\mathit{Pol}(\mathcal{G})$-separable. It will then be immediate that
$w=w^{\prime}x\in L_{\mathcal{A}}(s_{1},t_{1})$ and, if $n\geq 2$, Lemma 3.8
implies that $(\\{w\\})\cdot T_{n-1}(s_{2},t_{2},s_{3},t_{3})$ is not
$\mathit{Pol}(\mathcal{G})$-separable.

We consider two cases depending on whether $x\in A$ or $x=\varepsilon$. First,
if $x=a\in A$, then $(q_{i},a,t_{i})\in\delta$ for $i=\\{1,2,3\\}$. Clearly,
this implies that $a\in L_{\mathcal{A}}(q_{1},t_{1})$ and, if $n\geq 2$, then
$(\\{a\\})\cdot T_{n-1}(q_{2},t_{2},q_{3},t_{3})$ is not
$\mathit{Pol}(\mathcal{G})$-separable by Lemma 3.7 since $a\in
L_{\mathcal{A}}(q_{2},t_{2})\cap L_{\mathcal{A}}(q_{3},t_{3})$. Assume now
that $x=\varepsilon$: we are dealing with an $\varepsilon$-transition. By
definition of $\gamma_{S}$, we have $q_{1}=t_{1}$ and
$(q_{2},t_{2},q_{3},t_{3})\in S$. The former yields $\varepsilon\in
L_{\mathcal{A}}(q_{1},t_{1})$. Moreover, if $n\geq 2$, since
$(q_{2},t_{2},q_{3},t_{3})\in S$, it follows from induction on $n$ in
Proposition 4.6 that the $(n-1)$-tuple $T_{n-1}(q_{2},t_{2},q_{3},t_{3})$ is
not $\mathit{Pol}(\mathcal{G})$-separable under $\mathcal{G}$-control.
Combined with Lemma 3.10, this yields that $(\\{\varepsilon\\})\cdot
T_{n-1}(q_{2},t_{2},q_{3},t_{3})$ is not
$\mathit{Pol}(\mathcal{G})$-separable, as desired.

We may now complete the proof of Proposition 4.6. By symmetry, we only treat
the case when $n$ is odd and leave the case when it is even to the reader. Let
$(q_{1},r_{1},q_{2},r_{2})\in S$, we have to prove that
$T_{n}(q_{1},r_{1},q_{2},r_{2})$ is not $\mathit{Pol}(\mathcal{G})$-separable
under $\mathcal{G}$-control. Hence, we fix $H\in\mathcal{G}$ such that
$\varepsilon\in H$ and prove $H\cap T_{n}(q_{1},r_{1},q_{2},r_{2})$ is not
$\mathit{Pol}(\mathcal{G})$-separable. Since $S$ is $(\mathit{BPol},*)$-sound,
we have $\tau_{\mathcal{A},\mathcal{G}}(S)=S$, which implies that
$(q_{1},r_{1},q_{2},r_{2})\in\tau_{\mathcal{A},\mathcal{G}}(S)$. Hence, it
follows from (1) that $\\{\varepsilon\\}$ is not $\mathcal{G}$-separable from
$L_{\mathcal{B}_{S}}((q_{2},q_{1},q_{2}),(r_{2},r_{1},r_{2}))$. Since
$H\in\mathcal{G}$ and $\varepsilon\in H$, we get a word $w\in H\cap
L_{\mathcal{B}_{S}}((q_{2},q_{1},q_{2}),(r_{2},r_{1},r_{2}))$. By Lemma 4.7,
we have $w\in H\cap L_{\mathcal{A}}(q_{2},r_{2})$. This completes the proof
when $n=1$. Indeed, in that case we have
$T_{1}(q_{1},r_{1},q_{2},r_{2})=(L_{\mathcal{A}}(q_{2},r_{2}))$ and since
$H\cap L_{\mathcal{A}}(q_{2},r_{2})\neq\emptyset$, it follows that $H\cap
T_{1}(q_{1},r_{1},q_{2},r_{2})$ is not $\mathit{Pol}(\mathcal{G})$-separable,
as desired. If $n\geq 2$, then Lemma 4.7 also implies that $(\\{w\\})\cdot
T_{n-1}(q_{1},r_{1},q_{2},r_{2})$ is not
$\mathit{Pol}(\mathcal{G})$-separable. Since $w\in H\cap
L_{\mathcal{A}}(q_{2},r_{2})$, Lemma 3.7 yields that $(H\cap
L_{\mathcal{A}}(q_{2},r_{2}))\cdot T_{n-1}(q_{1},r_{1},q_{2},r_{2})$ is not
$\mathit{Pol}(\mathcal{G})$-separable. Thus, since
$H\in\mathcal{G}\subseteq\mathit{Pol}(\mathcal{G})$, one may verify that the
$n$-tuple $(H\cap L_{\mathcal{A}}(q_{2},r_{2}))\cdot(H\cap
T_{n-1}(q_{1},r_{1},q_{2},r_{2}))$ is not
$\mathit{Pol}(\mathcal{G})$-separable. By definition, this exactly says that
$H\cap T_{n}(q_{1},r_{1},q_{2},r_{2})$ is not
$\mathit{Pol}(\mathcal{G})$-separable, completing the proof.

Second part:
$\mathcal{I}_{\mathit{BPol}(\mathcal{G})}[\mathcal{G},\mathcal{A}]\subseteq
S$. In the sequel, we say that an arbitrary set $R\subseteq Q^{4}$ is _good_
if there exists $L\in\mathcal{G}$ such $\varepsilon\in L$ and a
$\mathit{BPol}(\mathcal{G})$-cover $\mathbf{K}$ of $L$ which is separating for
$R$.

######  Proposition 4.9.

Let $R\subseteq Q^{4}$. If $R$ is good, then
$\tau_{\mathcal{A},\mathcal{G}}(R)$ is good as well.

We use Proposition 4.9 to complete the proof. Let $S_{0}=Q^{4}$ and
$S_{i}=\tau_{\mathcal{A},\mathcal{G}}(S_{i-1})$ for $i\geq 1$. By Lemma 4.2,
we have $S_{0}\supseteq S_{1}\subseteq S_{2}\supseteq\cdots$ and there is
$n\in{\rm Nature}$ such that $S_{n}$ is the greatest $(\mathit{BPol},*)$-sound
subset for $\mathcal{G}$ and $\mathcal{A}$, _i.e._ , such that $S_{n}=S$.
Since $S_{0}$ is good ($\\{A^{*}\\}$ is a $\mathit{BPol}(\mathcal{G})$-cover
of $A^{*}\in\mathcal{G}$ which is separating for $S_{0}=Q^{4}$), Proposition
4.9 implies that $S_{i}$ is good for all $i\in{\rm Nature}$. Thus, $S=S_{n}$
is good. We get $L\in\mathcal{G}$ such that $\varepsilon\in L$ and a
$\mathit{BPol}(\mathcal{G})$-cover $\mathbf{K}$ of $L$ which is separating for
$S$. Lemma 3.4 then yields
$\mathcal{I}_{\mathit{BPol}(\mathcal{G})}[\mathcal{G},\mathcal{A}]\subseteq S$
as desired.

######  Remark 4.10.

The proof of Proposition 4.9 actually provides a construction for building
$L\in\mathcal{G}$ such that $\varepsilon\in L$ and a
$\mathit{BPol}(\mathcal{G})$-cover $\mathbf{K}$ of $L$ which is separating for
$S$ (yet, this involves building separators in $\mathcal{G}$, see Lemma 4.11).
As we have now established that
$S=\mathcal{I}_{\mathit{BPol}(\mathcal{G})}[\mathcal{G},\mathcal{A}]$, one may
then follow the proof of Proposition 3.5 to build a
$\mathit{BPol}(\mathcal{G})$-cover $\mathbf{H}$ of $A^{*}$ which is separating
for $\mathcal{I}_{\mathit{BPol}(\mathcal{G})}[\mathcal{A}]$. Finally,
$\mathbf{H}$ encodes separators for all pairs of languages recognized by
$\mathcal{A}$ which are $\mathit{BPol}(\mathcal{G})$-separable (this is the
proof of Lemma 3.3 presented in Appendix B). Altogether, we get a way to build
separators in $\mathit{BPol}(\mathcal{G})$, when they exist.

We now prove Proposition 4.9. Let $R\subseteq Q^{4}$ be good. We have to build
$L\in\mathcal{G}$ with $\varepsilon\in L$ and a
$\mathit{BPol}(\mathcal{G})$-cover $\mathbf{K}$ of $L$ which is separating for
$\tau_{\mathcal{A},\mathcal{G}}(R)$ (which will prove that
$\tau_{\mathcal{A},\mathcal{G}}(R)$ is good as well). We first build $L$ (this
part is independent from our hypothesis on $R$).

######  Lemma 4.11.

There exists $L\in\mathcal{G}$ such that $\varepsilon\in L$ and for every
$(q,r,s,t)\in Q^{4}$, if $L_{\mathcal{B}_{R}}((q,s,q),(r,t,r))\cap
L\neq\emptyset$ and $L_{\mathcal{B}_{R}}((s,q,s),(t,r,t))\cap L\neq\emptyset$,
then $(q,r,s,t)\in\tau_{\mathcal{A},\mathcal{G}}(R)$.

######  Proof 4.12.

Let $\mathbf{H}$ be the _finite_ set of all languages recognized by
$\mathcal{B}_{R}$ such that $\\{\varepsilon\\}$ is $\mathcal{G}$-separable
from $H$. For every $H\in\mathbf{H}$, there exists $L_{H}\in\mathcal{G}$ such
that $\varepsilon\in L_{H}$ and $L_{H}\cap H=\emptyset$. We define
$L=\bigcap_{H\in\mathbf{H}}L_{H}\in\mathcal{G}$. It is clear that
$\varepsilon\in L$. Moreover, given $(q,r,s,t)\in Q^{4}$, if
$L_{\mathcal{B}_{R}}((q,s,q),(r,t,r))\cap L\neq\emptyset$ and
$L_{\mathcal{B}_{R}}((s,q,s),(t,r,t))\cap L\neq\emptyset$, it follows from the
definition of $L$ that $\\{\varepsilon\\}$ is not $\mathcal{G}$-separable from
both $L_{\mathcal{B}_{R}}((q,s,q),(r,t,r))$ and
$L_{\mathcal{B}_{R}}((s,q,s),(t,r,t))$. It follows from (1) in the definition
of $\tau_{\mathcal{A},\mathcal{G}}$ that
$(q,r,s,t)\in\tau_{\mathcal{A},\mathcal{G}}(R)$.

We fix $L\in\mathcal{G}$ as described in Lemma 4.11 for the remainder of the
proof. We now build the $\mathit{BPol}(\mathcal{G})$-cover $\mathbf{K}$ of $L$
using the hypothesis that $R$ is good and Proposition 2.6.

######  Lemma 4.13.

For all $(q,r)\in Q^{2}$, there is $H_{q,r}\in\mathit{BPol}(\mathcal{G})$ such
that $L_{\mathcal{A}}(q,r)\cap L\subseteq H_{q,r}$ and for all pairs $(s,t)\in
Q^{2}$, if $L_{\mathcal{A}}(s,t)\cap H_{q,r}\neq\emptyset$ then
$L_{\mathcal{B}_{R}}((q,s,q),(r,t,r))\cap L\neq\emptyset$.

######  Proof 4.14.

Since $R$ is good, there are $U\in\mathcal{G}$ such that $\varepsilon\in U$
and a $\mathit{BPol}(\mathcal{G})$-cover $\mathbf{V}$ of $U$ which is
separating for $R$. We use them to build $H_{q,r}$. Since $U$ is a group
language and $\varepsilon\in U$, Proposition 2.6 yields a cover $\mathbf{P}$
of $L_{\mathcal{A}}(q,r)\cap L$ such that every $P\in\mathbf{P}$ is of the
form $P=\mathord{\uparrow}_{U}w_{P}$ where $w_{P}\in L_{\mathcal{A}}(q,r)\cap
L$. For every $P\in\mathbf{P}$, we build a $\mathit{BPol}(\mathcal{G})$-cover
$\mathbf{K}_{P}$ of $P$. Let $a_{1},\dots,a_{n}\in A$ be the letters such that
$w_{P}=a_{1}\cdots a_{n}$. We have $P=Ua_{1}U\cdots a_{n}U$. Since
$U\in\mathcal{G}\subseteq\mathit{Pol}(\mathcal{G})$ and $\mathbf{V}$ is a
$\mathit{BPol}(\mathcal{G})$-cover of $U$, Proposition 2.5 yields a
$\mathit{BPol}(\mathcal{G})$-cover $\mathbf{K}_{P}$ of $P$ such that for every
$K\in\mathbf{K}_{P}$, there exist $V_{0},\dots,V_{n}\in\mathbf{V}$ satisfying
$K\subseteq V_{0}a_{1}V_{1}\cdots a_{n}V_{n}$. We define $H_{q,r}$ as the
union of all languages $K$ such that $K\in\mathbf{K}_{P}$ for some
$P\in\mathbf{P}$ and $L_{\mathcal{A}}(q,r)\cap K\neq\emptyset$. Clearly,
$H_{q,r}\in\mathit{BPol}(\mathcal{G})$. Moreover, since $\mathbf{P}$ is a
cover of $L_{\mathcal{A}}(q,r)\cap L$, and $\mathbf{K}_{P}$ is a cover of $P$
for each $P\in\mathbf{P}$, it is clear that $L_{\mathcal{A}}(q,r)\cap
L\subseteq H_{q,r}$. We now fix $(s,t)\in Q^{2}$ such that
$L_{\mathcal{A}}(s,t)\cap H_{q,r}\neq\emptyset$ and show that
$L_{\mathcal{B}_{R}}((q,s,q),(r,t,r))\cap L\neq\emptyset$. By definition of
$H_{q,r}$, we get $P\in\mathbf{P}$ and $K\in\mathbf{K}_{P}$ such that
$L_{\mathcal{A}}(q,r)\cap K\neq\emptyset$ and $L_{\mathcal{A}}(s,t)\cap
K\neq\emptyset$. By definition, $P=\mathord{\uparrow}_{U}w_{P}$ with $w_{P}\in
L_{\mathcal{A}}(q,r)\cap L$. Hence, it suffices to prove that $w_{P}\in
L_{\mathcal{B}_{R}}((q,s,q),(r,t,r))$.

We fix $x\in L_{\mathcal{A}}(s,t)\cap K$ and $y\in L_{\mathcal{A}}(q,r)\cap
K$. Recall that $w_{P}=a_{1}\cdots a_{n}$ (if $n=0$, then
$w_{P}=\varepsilon$). Since $w_{P}\in L_{\mathcal{A}}(q,r)$, we may consider
the corresponding run in $\mathcal{A}$: we get $p_{0},\dots,p_{n}\in Q$ such
that $p_{0}=q$, $p_{n}=r$ and $(p_{i-1},a_{i},p_{i})\in\delta$ for $1\leq
i\leq n$. Moreover, since $K\in\mathbf{K}_{P}$ and $w_{P}=a_{1}\cdots a_{n}$,
we have $K\subseteq V_{0}a_{1}V_{1}\cdots a_{n}V_{n}$ for
$V_{0},\dots,V_{n}\in\mathbf{V}$ (if $n=0$, then $K\subseteq V_{0}$). Since
$x,y\in K$, we get $x_{i},y_{i}\in V_{i}$ for $0\leq i\leq n$ such that
$x=x_{0}a_{1}x_{1}\cdots a_{n}x_{n}$ and $y=y_{0}a_{1}y_{1}\cdots a_{n}y_{n}$.
Since $x\in L_{\mathcal{A}}(s,t)$, we get $s_{0},t_{0},\dots,s_{n},t_{n}\in Q$
such that $s_{0}=s$, $t_{n}=t$, $x_{i}\in L_{\mathcal{A}}(s_{i},t_{i})$ for
$0\leq i\leq n$, and $(t_{i-1},a_{i},s_{i})\in\delta$ for $1\leq i\leq n$.
Symmetrically, since $y\in L_{\mathcal{A}}(q,r)$, we get
$q_{0},r_{0},\dots,q_{n},r_{n}\in Q$ such that $q_{0}=q$, $r_{n}=r$, $y_{i}\in
L_{\mathcal{A}}(q_{i},r_{i})$ for $0\leq i\leq n$, and
$(r_{i-1},a_{i},q_{i})\in\delta$ for $1\leq i\leq n$. By definition of
$\gamma_{R}$, it is immediate that
$((p_{i-1},t_{i-1},r_{i-1}),a_{i},(p_{i},s_{i},q_{i}))\in\gamma_{R}$ for
$1\leq i\leq n$. Since $V_{i}\in\mathbf{V}$ and $\mathbf{V}$ is separating for
$R$, the fact that $x_{i},y_{i}\in V_{i}$ implies that
$(s_{i},t_{i},q_{i},r_{i})\in R$ for $0\leq i\leq n$. Hence,
$((p_{i},s_{i},q_{i}),\varepsilon,(p_{i},t_{i},r_{i}))\in\gamma_{R}$ by
definition. Thus, we get a run labeled by $w_{P}$ from $(p_{0},s_{0},q_{0})$
to $(p_{n},t_{n},r_{n})$ in $\mathcal{B}_{R}$, _i.e._ , $w_{P}\in
L_{\mathcal{B}_{R}}((q,s,q),(r,t,r))$ as desired.

We may now build $\mathbf{K}$. Let $\mathbf{H}=\big{\\{}H_{q,r}\mid(q,r)\in
Q^{2}\big{\\}}$. Consider the following equivalence $\sim$ defined on $L$:
given $u,v\in L$, we let $u\sim v$ if and only if $u\in H_{q,r}\Leftrightarrow
v\in H_{q,r}$ for every $(q,r)\in Q^{2}$. We let $\mathbf{K}$ as the partition
of $L$ into $\sim$-classes. Clearly, each $K\in\mathbf{K}$ is a Boolean
combination involving the languages in $\mathbf{H}$ (which belong to
$\mathit{BPol}(\mathcal{G})$) and $L\in\mathcal{G}$. Hence, $\mathbf{K}$ is a
$\mathit{BPol}(\mathcal{G})$-cover of $L$. We now prove that it is separating
for $\tau_{\mathcal{A},\mathcal{G}}(R)$. Let $q,r,s,t\in Q$ and
$K\in\mathbf{K}$ such that there are $u\in L_{\mathcal{A}}(q,r)\cap K$ and
$v\in L_{\mathcal{A}}(s,t)\cap K$. We show that
$(q,r,s,t)\in\tau_{\mathcal{A},\mathcal{G}}(R)$. By definition of
$\mathbf{K}$, we have $u,v\in L$ and $u\sim v$. In particular, $u\in
L_{\mathcal{A}}(q,r)\cap L$ which yields $u\in H_{q,r}$ by definition in Lemma
4.13. Together with $u\sim v$, this yields $v\in H_{q,r}$. Hence,
$L_{\mathcal{A}}(s,t)\cap H_{q,r}\neq\emptyset$ and Lemma 4.13 yields
$L_{\mathcal{B}_{R}}((q,s,q),(r,t,r))\cap L\neq\emptyset$. One may now use a
symmetrical argument to obtain $L_{\mathcal{B}_{R}}((s,q,s),(t,r,t))\cap
L\neq\emptyset$. By definition of $L$ in Lemma 4.11, this yields
$(q,r,s,t)\in\tau_{\mathcal{A},\mathcal{G}}(R)$, completing the proof.

##  5 Conclusion

In this paper, we proved that for every group prevariety $\mathcal{G}$, there
exist generic polynomial time Turing reductions from
$\mathit{BPol}(\mathcal{G})$\- and $\mathit{BPol}(\mathcal{G}^{+})$-separation
to $\mathcal{G}$-separation, for input languages represented by NFAs. While a
generic reduction from $\mathit{BPol}(\mathcal{G})$-separation to
$\mathcal{G}$-separation was already developed in [21], it relied on an
involved machinery, which required to dig into a more general problem than
$\mathit{BPol}(\mathcal{G})$-separation, namely
“$\mathit{BPol}(\mathcal{G})$-covering”. In particular, the techniques from
[21] do not provide any way to build separators in
$\mathit{BPol}(\mathcal{G})$ (when they exist). They also yield poor upper
complexity bounds. At last, the results of [21] do not apply to
$\mathit{BPol}(\mathcal{G}^{+})$. In this case, even the existence of a
generic reduction is new. It would be interesting to unify ideas of the
present paper with the techniques of [21], to lift them to the setting of
$\mathit{BPol}(\mathcal{G})$\- and $\mathit{BPol}(\mathcal{G}^{+})$-covering.
We leave this for further work.

Our results imply that separation is decidable in _polynomial time_ for a
number of standard classes: the piecewise testable languages (_i.e._ ,
$\mathit{BPol}(\textup{ST})$ or equivalently $\mathcal{B}\Sigma_{1}(<)$), the
languages of dot-depth one (_i.e._ , $\mathit{BPol}(\textup{ST}^{+})$ or
equivalently $\mathcal{B}\Sigma_{1}(<,+1)$), the classes
$\mathit{BPol}(\textup{MOD})$ and $\mathit{BPol}(\textup{MOD}^{+})$ (_i.e._ ,
$\mathcal{B}\Sigma_{1}(<,MOD)$ and $\mathcal{B}\Sigma_{1}(<,+1,MOD)$) and the
classes $\mathit{BPol}(\textup{GR})$ and $\mathit{BPol}(\textup{GR}^{+})$.
While this was well-known for the piecewise testable languages [17, 6], all
other results are new—not only regarding the complexity, but even regarding
the decidability. Actually, it is shown in [12] that
$\mathit{BPol}(\textup{ST})$-separation is P-complete. It turns out that the
reduction of [12], from the circuit value problem, adapts to prove the
P-completeness of separation for all of the above classes (we leave the
details for further work). Finally, our results also apply to the classes
$\mathit{BPol}(\textup{AMT})$ and $\mathit{BPol}(\textup{AMT}^{+})$ (_i.e._ ,
$\mathcal{B}\Sigma_{1}(<,AMOD)$ and $\mathcal{B}\Sigma_{1}(<,+1,AMOD)$): we
obtain that separation is in co-NP. While this is currently unknown, we
conjecture that this is a _tight_ upper bound. Indeed, it is known that AMT-
separation is co-NP-complete [25].

## References

  * [1] Jorge Almeida and Marc Zeitoun.  The pseudovariety ${\bf J}$ is hyperdecidable.  RAIRO Theoretical Informatics and Applications, 31(5):457–482, 1997\.
  * [2] Mustapha Arfi.  Polynomial operations on rational languages.  In Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science, STACS’87, pages 198–206, Berlin, Heidelberg, 1987\. Springer-Verlag.
  * [3] Janusz A. Brzozowski and Rina S. Cohen.  Dot-depth of star-free events.  Journal of Computer and System Sciences, 5(1):1–16, 1971.
  * [4] Antonio Cano, Giovanna Guaiana, and Jean-Eric Pin.  Regular languages and partial commutations.  Journal of Information and Computation, 230:76–96, 2013.
  * [5] Laura Chaubard, Jean Éric Pin, and Howard Straubing.  First order formulas with modular predicates.  In Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS’06), pages 211–220, 2006.
  * [6] Wojciech Czerwiński, Wim Martens, and Tomáš Masopust.  Efficient separability of regular languages by subsequences and suffixes.  In Proceedings of the 40th International Colloquium on Automata, Languages, and Programming, ICALP’13, pages 150–161, Berlin, Heidelberg, 2013\. Springer-Verlag.
  * [7] Samuel Eilenberg.  Automata, Languages, and Machines, volume B.  Academic Press, Inc., Orlando, FL, USA, 1976.
  * [8] Karsten Henckell, Stuart Margolis, Jean-Eric Pin, and John Rhodes.  Ash’s type II theorem, profinite topology and Malcev products.  International Journal of Algebra and Computation, 1:411–436, 1991\.
  * [9] Robert Knast.  A semigroup characterization of dot-depth one languages.  RAIRO - Theoretical Informatics and Applications, 17(4):321–330, 1983.
  * [10] Alexis Maciel, Pierre Péladeau, and Denis Thérien.  Programs over semigroups of dot-depth one.  Theoretical Computer Science, 245(1):135–148, 2000.
  * [11] Stuart Margolis and Jean-Eric Pin.  Product of Group Languages.  In FCT Conference, volume Lecture Notes in Computer Science, pages 285–299. Springer-Verlag, 1985.
  * [12] Tomás Masopust.  Separability by piecewise testable languages is ptime-complete.  Theor. Comput. Sci., 711:109–114, 2018.
  * [13] Jean-Eric Pin.  Algebraic tools for the concatenation product.  Theoretical Computer Science, 292:317–342, 2003.
  * [14] Jean-Eric Pin.  An explicit formula for the intersection of two polynomials of regular languages.  In DLT 2013, volume 7907 of Lect. Notes Comp. Sci., pages 31–45. Springer, 2013.
  * [15] Jean-Eric Pin and Howard Straubing.  Some results on $\mathcal{C}$-varieties.  RAIRO - Theoretical Informatics and Applications, 39(1):239–262, 2005.
  * [16] Thomas Place, Varun Ramanathan, and Pascal Weil.  Covering and separation for logical fragments with modular predicates.  Logical Methods in Computer Science, 15(2), 2019.
  * [17] Thomas Place, Lorijn van Rooijen, and Marc Zeitoun.  Separating regular languages by piecewise testable and unambiguous languages.  In Proceedings of the 38th International Symposium on Mathematical Foundations of Computer Science, MFCS’13, pages 729–740, Berlin, Heidelberg, 2013. Springer-Verlag.
  * [18] Thomas Place and Marc Zeitoun.  Separation for dot-depth two.  In Proceedings of the 32th Annual ACM/IEEE Symposium on Logic in Computer Science, (LICS’17), pages 202–213. IEEE Computer Society, 2017\.
  * [19] Thomas Place and Marc Zeitoun.  The covering problem.  Logical Methods in Computer Science, 14(3), 2018.
  * [20] Thomas Place and Marc Zeitoun.  Generic results for concatenation hierarchies.  Theory of Computing Systems (ToCS), 63(4):849–901, 2019.  Selected papers from CSR’17.
  * [21] Thomas Place and Marc Zeitoun.  Separation and covering for group based concatenation hierarchies.  In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’19, pages 1–13, 2019.
  * [22] Thomas Place and Marc Zeitoun.  Adding successor: A transfer theorem for separation and covering.  ACM Transactions on Computational Logic, 21(2):9:1–9:45, 2020\.
  * [23] Thomas Place and Marc Zeitoun.  Separation for dot-depth two.  Logical Methods in Computer Science, Volume 17, Issue 3, 2021\.
  * [24] Thomas Place and Marc Zeitoun.  Characterizing level one in group-based concatenation hierarchies.  In Computer Science – Theory and Applications, Cham, 2022. Springer International Publishing.
  * [25] Thomas Place and Marc Zeitoun.  Group separation strikes back.  To appear, a preliminary version is vailable at https://www.labri.fr/perso/tplace/Files/groups.pdf, 2022.
  * [26] Imre Simon.  Piecewise testable events.  In Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, pages 214–222, Berlin, Heidelberg, 1975. Springer-Verlag.
  * [27] Benjamin Steinberg.  Inevitable graphs and profinite topologies: Some solutions to algorithmic problems in monoid and automata theory, stemming from group theory.  International Journal of Algebra and Computation, 11(1):25–72, 2001\.
  * [28] Howard Straubing.  A generalization of the schützenberger product of finite monoids.  Theoretical Computer Science, 13(2):137–150, 1981.
  * [29] Howard Straubing.  Finite semigroup varieties of the form V * D.  Journal of Pure and Applied Algebra, 36:53–94, 1985.
  * [30] Howard Straubing.  On logical descriptions of regular languages.  In Proceedings of the 5th Latin American Symposium on Theoretical Informatics, LATIN’02, pages 528–538, Berlin, Heidelberg, 2002. Springer-Verlag.
  * [31] Denis Thérien.  Classification of finite monoids: The language approach.  Theoretical Computer Science, 14(2):195–208, 1981.
  * [32] Gabriel Thierrin.  Permutation automata.  Theory of Computing Systems, 2(1):83––90, 1968.
  * [33] Wolfgang Thomas.  Classifying regular events in symbolic logic.  Journal of Computer and System Sciences, 25(3):360–376, 1982.
  * [34] Bret Tilson.  Categories as algebra: essential ingredient in the theory of monoids.  Journal of Pure and Applied Algebra, 48(1):83–198, 1987.
  * [35] Georg Zetzsche.  Separability by piecewise testable languages and downward closures beyond subwords.  In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’18, pages 929–938, 2018.

##  Appendix A Appendix to Section 2

We start with the proof of Proposition 2.5. Let us first recall the statement.

See 2.5

######  Proof A.1.

We first handle the case when $n=1$ (_i.e._ , there are two languages
$L_{0},L_{1}\in\mathit{Pol}(\mathcal{C})$) and then lift the result to the
general case using a simple induction. For the sake of avoiding clutter, we
write $\mathcal{D}=\mathit{Pol}(\mathcal{C})$ in the proof.

Case $n=1$. Consider two languages $L_{0},L_{1}\in\mathcal{D}$ and $a\in A$.
Moreover, let $\mathbf{H}_{0}$ and $\mathbf{H}_{1}$ be
$\mathit{Bool}(\mathcal{D})$-covers of $L_{0}$ and $L_{1}$. We need to build
an appropriate $\mathit{Bool}(\mathcal{D})$-cover $\mathbf{K}$ of
$L_{0}aL_{1}$. By hypothesis, every language in
$\mathbf{H}_{0}\cup\mathbf{H}_{1}$ is a Boolean combination of languages in
$\mathcal{D}$. Moreover, $L_{0},L_{1}\in\mathcal{D}$. Hence, there exists a
_finite_ set of languages $\mathbf{U}\subseteq\mathcal{D}$ containing
$L_{0},L_{1}$ and such that every language
$H\in\mathbf{H}_{0}\cup\mathbf{H}_{1}$ is a Boolean combination of languages
in $\mathbf{U}$. We define $\mathbf{V}$ as the set containing all finite
intersections of languages in $\mathbf{U}$. Clearly, $\mathbf{V}$ remains
finite and since $\mathcal{D}=\mathit{Pol}(\mathcal{C})$ is a lattice by
Theorem 2.2, we have $\mathbf{U}\subseteq\mathbf{V}\subseteq\mathcal{D}$. We
let $\mathbf{P}=\\{V_{0}aV_{1}\mid V_{0},V_{1}\in\mathbf{V}\\}$. We have
$L_{0}aL_{1}\in\mathbf{P}$ by definition and $\mathbf{P}\subseteq\mathcal{D}$
since $\mathcal{D}=\mathit{Pol}(\mathcal{C})$ is closed under marked product .
We now use $\mathbf{P}$ to define an equivalence on $A^{*}$. Given
$w,w^{\prime}\in A^{*}$, we write $w\sim w^{\prime}$ if and only if $w\in
P\Leftrightarrow w^{\prime}\in P$ for every $P\in\mathbf{P}$. Since
$\mathbf{P}$ is finite, we know that $\sim$ has finite index. Moreover, by
definition, every $\sim$-class is a Boolean combination of languages in
$\mathbf{P}\subseteq\mathcal{D}$, which means that it belongs to
$\mathit{Bool}(\mathcal{D})$.

Since $L_{0}aL_{1}\in\mathbf{P}$, the definition implies that $L_{0}aL_{1}$ is
a finite union of $\sim$-classes. We define $\mathbf{K}$ as the set containing
all $\sim$-classes in this union. This is a $\mathit{Bool}(\mathcal{D})$-cover
of $L_{0}aL_{1}$ by definition. It remains to prove that for every
$K\in\mathbf{K}$, there exist $H_{0}\in\mathbf{H}_{0}$ and
$H_{1}\in\mathbf{H}_{1}$ such that $K\subseteq H_{0}aH_{1}$. We fix
$K\in\mathbf{K}$ for the proof and use the following lemma.

######  Lemma A.2.

Let $G\subseteq K$ be a _finite_ language. There exists
$H_{0}\in\mathbf{H}_{0}$ and $H_{1}\in\mathbf{H}_{1}$ such that $G\subseteq
H_{0}aH_{1}$.

We first apply Lemma A.2 to complete the main argument. For each $n\in{\rm
Nature}$, we let $G_{n}\subseteq K$ as the (finite) language containing all
words in $K$ of length at most $n$. Clearly, we have,

$K=\bigcup_{n\in{\rm Nature}}G_{n}\quad\text{and}\quad G_{n}\subseteq
G_{n+1}\text{ for all $n\in{\rm Nature}$}.$

For every $n\in{\rm Nature}$, Lemma A.2 yields $H_{0,n}\in\mathbf{H}_{0}$ and
$H_{1,n}\in\mathbf{H}_{1}$ such that $G_{n}\subseteq H_{0,n}aH_{1,n}$. Since
$\mathbf{H}_{0}$ and $\mathbf{H}_{1}$ are finite sets, there exist
$H_{0}\in\mathbf{H}_{0}$ and $H_{1}\in\mathbf{H}_{1}$ such that
$H_{0,n}=H_{0}$ and $H_{1,n}=H_{1}$ for infinitely many $n$. Since
$G_{n}\subseteq G_{n+1}$ for every $n\in{\rm Nature}$, it then follows that
$G_{n}\subseteq H_{0}aH_{1}$ for every $n\in{\rm Nature}$. Finally, since
$K=\bigcup_{n\in{\rm Nature}}G_{n}$, this implies $K\subseteq H_{0}aH_{1}$,
completing the main proof.

We turn to the proof of Lemma A.2. We fix a finite language $G\subseteq K$ for
the proof. We exhibit $H_{0}\in\mathbf{H}_{0}$ and $H_{1}\in\mathbf{H}_{1}$
such that $G\subseteq H_{0}aH_{1}$. Let $w_{1},\dots,w_{n}\in A^{*}$ be the
words contained in $G$, _i.e._ $G=\\{w_{1},\dots,w_{n}\\}$. By definition, we
know that $K$ is a $\sim$-class included in $L_{0}aL_{1}$. Consequently, we
have $w_{1},\dots,w_{n}\in L_{0}aL_{1}$ and $w_{1}\sim\cdots\sim w_{n}$. We
use the latter property to prove an intermediary fact. Given two words
$w,w^{\prime}\in A^{*}$, we write $w\preceq w^{\prime}$ if and only if $w\in
V\Rightarrow w^{\prime}\in V$ for every $V\in\mathbf{V}$. Clearly, “$\preceq$”
is a preorder.

######  Claim 1.

For every $u,v\in A^{*}$ such that $w_{n}=uav$, there exist
$u_{1},\dots,u_{n},v_{1},\dots,v_{n}\in A^{*}$ such that $w_{i}=u_{i}av_{i}$
for every $i\leq n$, $u\preceq u_{1}\preceq\cdots\preceq u_{n}$ and $v\preceq
v_{1}\preceq\cdots\preceq v_{n}$.

######  Proof A.3.

We prove the existence of $u_{1},v_{1}\in A^{*}$ such that
$w_{1}\\!=\\!u_{1}av_{1}$, $u\preceq u_{1}$ and $v\preceq v_{1}$ using the
fact that $w_{n}=uav$ and $w_{n}\sim w_{1}$, one may then iterate the argument
to build $u_{2},\dots,u_{n}\in A^{*}$ and $v_{2},\dots,v_{n}\in A^{*}$.
Consider the languages $L_{u}=\bigcap_{\\{V\in\mathbf{V}\mid u\in V\\}}V$ and
$L_{v}=\bigcap_{\\{V\in\mathbf{V}\mid v\in V\\}}V$. Since $\mathbf{V}$ is
finite and closed under intersection by definition, we have
$L_{u},L_{v}\in\mathbf{V}$. Hence, $L_{u}L_{v}\in\mathbf{P}$ by definition of
$\mathbf{P}$. Moreover, it is clear that $uav\in L_{u}aL_{v}$. Therefore,
since $uav=w_{n}\sim w_{1}$, the definition of $\sim$ implies that $w_{1}\in
L_{u}aL_{v}$. This yields $u_{1}\in L_{u}$ and $v_{1}\in L_{v}$ such that
$w_{1}=u_{1}av_{1}$. Finally, the definitions of $L_{u}$ and $L_{v}$ imply
that $u\preceq u_{1}$ and $v\preceq v_{1}$, completing the proof.

Since $w_{n}\in L_{0}aL_{1}$, it can be decomposed as $w_{n}=uav$ with $u\in
L_{0}$ and $v\in L_{1}$. Since $w_{1}$ is a finite word, it admits finitely
many decompositions $w_{1}=u_{1}av_{1}$ with $u_{1},v_{1}\in A^{*}$.
Therefore, a repeated application of the claim together with the pigeon-hole
principle yield $u_{1},\dots,u_{n},v_{1},\dots,v_{n}\in A^{*}$ such that
$w_{i}=u_{i}av_{i}$ for every $i\leq n$ and,

$u\preceq u_{1}\preceq\cdots\preceq u_{n}\preceq u_{1}\qquad\text{and}\qquad
v\preceq v_{1}\preceq\cdots\preceq v_{n}\preceq v_{1}.$

Since $u\in L_{0}$, $v\in L_{1}$ and $L_{0},L_{1}\in\mathbf{V}$ by definition
of $\mathbf{V}$, we get that $u_{1}\in L_{0}$ and $v_{1}\in L_{1}$ by
definition of $\preceq$. Therefore, since $\mathbf{H}_{0}$ and
$\mathbf{H}_{1}$ are covers of $L_{0}$ and $L_{1}$ respectively, there exist
$H_{0}\in\mathbf{H}_{0}$ and $H_{1}\in\mathbf{H}_{1}$ such that $u_{1}\in
H_{0}$ and $v_{1}\in H_{1}$. Moreover, we have $u_{1}\preceq u_{i}\preceq
u_{1}$ and $v_{1}\preceq v_{i}\preceq v_{1}$ for every $i\leq n$. By
definition of $\preceq$, this implies that for every language
$V\in\mathbf{V}$, we have $u_{1}\in V\Leftrightarrow u_{i}\in V$ and $v_{1}\in
V\Leftrightarrow v_{i}\in V$. Since the languages in
$\mathbf{H}_{0}\cup\mathbf{H}_{1}$ are Boolean combinations of those in
$\mathbf{V}$, it follows that $u_{1}\in H\Leftrightarrow u_{i}\in H$ and
$v_{1}\in H\Leftrightarrow v_{i}\in H$ for all
$H\in\mathbf{H}_{0}\cup\mathbf{H}_{1}$ and $i\leq n$. Hence, since $u_{1}\in
H_{0}$, $H_{0}\in\mathbf{H}_{0}$, $v_{1}\in H_{1}$ and
$H_{1}\in\mathbf{H}_{1}$, we obtain $u_{1},\dots,u_{n}\in H_{0}$ and
$v_{1},\dots,v_{n}\in H_{1}$. Altogether, it follows that
$G=\\{w_{1},\dots,w_{n}\\}=\\{u_{1}av_{1},\dots,u_{n}av_{n}\\}\subseteq
H_{0}aH_{1}$. This concludes the proof of Lemma A.2.

General case. We now use induction on $n\in{\rm Nature}$ to prove the general
case in Proposition 2.5. We fix $L_{0},\dots,L_{n}\in\mathcal{D}$,
$a_{1},\dots,a_{n}\in A$ and $\mathbf{H}_{i}$ a
$\mathit{BPol}(\mathcal{C})$-cover of $L_{i}$ for all $i\leq n$. We have to
construct an appropriate $\mathit{Bool}(\mathcal{D})$-cover $\mathbf{K}$ of
$L_{0}a_{1}L_{1}\cdots a_{n}L_{n}$.

The case $n=0$ is trivial: it suffices to define $\mathbf{K}=\mathbf{H}_{0}$.
Assume now that $n>1$. By induction hypothesis, there exists a
$\mathit{Bool}(\mathcal{C})$-cover $\mathbf{K}^{\prime}$ of
$L_{1}a_{2}L_{2}\cdots a_{n}L_{n}$ such that for every
$K^{\prime}\in\mathbf{K}^{\prime}$, we have $H_{i}\in\mathbf{H}_{i}$ for
$2\leq i\leq n$ such that $K^{\prime}\subseteq H_{1}a_{2}H_{2}\cdots
a_{n}H_{n}$. Since $\mathcal{D}=\mathit{Pol}(\mathcal{C})$ is closed under
marked product, we have $L_{1}a_{2}L_{2}\cdots a_{n}L_{n}\in\mathcal{D}$.
Hence, since we have a $\mathit{Bool}(\mathcal{D})$-cover $\mathbf{H}_{0}$ of
$L_{0}\in\mathcal{D}$ and a $\mathit{Bool}(\mathcal{C})$-cover
$\mathbf{K}^{\prime}$ of $L_{1}a_{2}L_{2}\cdots a_{n}L_{n}\in\mathcal{D}$, we
may use the case $n=1$ in Proposition 2.5 (which we proved above) to get a
$\mathit{Bool}(\mathcal{D})$-cover $\mathbf{K}$ of $L_{0}a_{1}L_{1}\cdots
a_{n}L_{n}$ such that for every $K\in\mathbf{K}$, there exist
$H_{0}\in\mathbf{H}_{0}$ and $K^{\prime}\in\mathbf{K}^{\prime}$ which satisfy
$K\subseteq H_{0}a_{1}K^{\prime}$. By definition of $\mathbf{K}^{\prime}$, we
know that there also exist $H_{i}\in\mathbf{H}_{i}$ for $2\leq i\leq n$ such
that $K^{\prime}\subseteq H_{1}a_{2}H_{2}\cdots a_{n}H_{n}$. Altogether, it
follows that $K\subseteq H_{0}a_{1}H_{1}\cdots a_{n}H_{n}$ which completes the
proof.

We now prove Proposition 2.6. Let us first recall the statement.

See 2.6

######  Proof A.4.

Since $L$ is a group language, there exists a morphism $\eta:A^{*}\to G$ into
a finite group $G$ recognizing $L$. We let $L^{\prime}=\eta^{-1}(1_{G})$.
Clearly, $L^{\prime}$ is a group language and $\varepsilon\in L^{\prime}$.
Moreover, since $\varepsilon\in L$ and $L$ is recognized by $\eta$, we have
$L^{\prime}\subseteq L$.

We use $L^{\prime}$ to define an ordering “$\preceq$” on $A^{*}$. Consider two
words $u,v\in A^{*}$, we write $u\preceq v$ when
$v\in\mathord{\uparrow}_{L^{\prime}}u$. By definition of $L^{\prime}$, it is
straightforward to verify that for every $u,v\in A^{*}$, if $u\preceq v$, then
$\eta(u)=\eta(v)$. Since $\varepsilon\in L^{\prime}$, it is simple to verify
that $\preceq$ is reflexive and antisymmetric. We prove that it is transitive.
Let $u,v,w\in A^{*}$ such that $u\preceq v$ and $v\preceq w$. We show that
$u\preceq w$. By definition, we have $v\in\mathord{\uparrow}_{L^{\prime}}u$.
Hence, we get $a_{1},\dots,a_{n}\in A$ and $x_{0},\dots,x_{n}\in L^{\prime}$
such that $u=a_{1}\cdots a_{n}$ and $v=x_{0}a_{1}x_{1}\cdots a_{n}x_{n}$.
Since we also have $w\in\mathord{\uparrow}_{L^{\prime}}v$, one may verify that
this yields $y_{0},\dots,y_{n}\in A^{*}$ such that $w=y_{0}a_{1}y_{1}\cdots
a_{n}y_{n}$ and $y_{i}\in\mathord{\uparrow}_{L^{\prime}}x_{i}$ for every
$i\leq n$. The latter property implies that $\eta(x_{i})=\eta(y_{i})$ for
every $i\leq n$. Hence, since $x_{0},\dots,x_{n}\in
L^{\prime}=\eta^{-1}(1_{G})$, we get $y_{0},\dots,y_{n}\in L^{\prime}$. We
conclude that $w\in\mathord{\uparrow}_{L^{\prime}}u$ which exactly says that
$u\preceq w$ as desired. The following lemma states that $\preceq$ is a “well
quasi-order”. A proof is available in [4, Proposition 3.10]. Here we use a
simple generalization of the proof of Higman’s lemma.

######  Lemma A.5.

Consider an infinite sequence $(u_{i})_{i\in{\rm Nature}}$ of words in
$A^{*}$. There exist $i,j\in{\rm Nature}$ such that $i<j$ and $u_{i}\preceq
u_{j}$.

######  Proof A.6.

We say that a sequence $(u_{i})_{i\in{\rm Nature}}$ is _bad_ if
$u_{i}\not\preceq u_{j}$ for every $i<j$. We need to prove that there exists
no bad sequence. We proceed by contradiction and assume that there exists a
bad sequence. We first use this hypothesis to construct a specific one. Using
induction, we build a particular sequence $(u_{i})_{i\in{\rm Nature}}$ such
that for every $i\in{\rm Nature}$, $u_{0},\dots,u_{i}$ can be continued into a
bad sequence and then verify that $(u_{i})_{i\in{\rm Nature}}$ is bad itself.

We let $u_{0}$ be a word of minimal length such that $u_{0}$ can be continued
into a bad sequence. Such a word must exist by the assumption that there
exists a bad sequence. Assume now that $u_{0},\dots,u_{i}$ have been defined
up to some $i\in{\rm Nature}$. By construction, $u_{0},\dots,u_{i}$ can be
continued into a bad sequence. We define $u_{i+1}$ as a word of minimal length
such that $u_{0},\dots,u_{i},u_{i+1}$ can be continued into a bad sequence.
This defines $(u_{i})_{i\in{\rm Nature}}$. Observe that it is necessarily bad.
Indeed, otherwise, we would have $i<j$ such that $u_{i}\preceq u_{j}$ which
contradicts the hypothesis that $u_{0},\dots,u_{j}$ can be continued into a
bad sequence.

Consider the set $A^{|G|}$ consisting of all words of length $|G|$. Since
$A^{|G|}$ is finite, there exists some word $w\in A^{|G|}$ such that $w$ is a
prefix of infinitely many words in the sequence $(u_{i})_{i\in{\rm Nature}}$.
We write $i_{1}<i_{2}<\cdots$ the infinitely many indices such that $w$ is a
prefix of $u_{i_{k}}$, _i.e._ $u_{i_{k}}=wv_{i_{k}}$ for some word
$v_{i_{k}}\in A^{*}$. Since $|w|=|G|$, a pumping argument yields $x,z\in
A^{*}$ and $y\in A^{+}$ such that $w=xyz$ and $\eta(x)=\eta(xy)$. Since $G$ is
a group, it follows that $\eta(y)=1_{G}$. We prove that the infinite sequence
$u_{0},u_{1},\dots,u_{i_{1}-1},xzv_{i_{1}},xzv_{i_{2}},xzv_{i_{3}},\dots$ is
bad. In particular, this means that $u_{0},\dots,u_{i_{1}-1},xzv_{i_{1}}$ can
be continued into a bad sequence. This is a contradiction: we have
$u_{i_{1}}=xyzv_{i_{1}}$ and since $y\in A^{+}$, this implies that
$|xzv_{i_{1}}|<|u_{i_{1}}|$. This is not possible since $u_{i_{1}}$ is defined
as a word of minimal length such that $u_{0},\dots,u_{i_{1}-1},u_{i_{1}}$ can
be continued into a bad sequence.

It remains to prove that
$u_{0},u_{1},\dots,u_{i_{1}-1},xzv_{i_{1}},xzv_{i_{2}},xzv_{i_{3}},\dots$ is
bad. Since $(u_{i})_{i\in{\rm Nature}}$ is bad itself, we already know that
for $i<j\leq i_{1}-1$, we have $u_{i}\not\preceq u_{j}$. We now prove that
$u_{i}\not\preceq xzv_{i_{h}}$ for $i\leq i_{1}-1$ and $h\geq 1$. By
contradiction, if $u_{i}\preceq xzv_{i_{h}}$, then $u_{i}\preceq
xyzv_{i_{h}}=u_{i_{h}}$ since $\eta(y)=1_{G}$. This contradicts the hypothesis
that $(u_{i})_{i\in{\rm Nature}}$ is bad. Finally, we show that given $h,k$
such that $1\leq h<k$, we have $xzv_{i_{h}}\not\preceq xzv_{i_{k}}$. By
contradiction assume that $xzv_{i_{h}}\preceq xzv_{i_{k}}$. One may verify
from the definition of $\preceq$ that this yields $v,v^{\prime}\in A^{*}$ such
that $v_{i_{k}}=vv^{\prime}$, $xz\preceq xzv$ and $v_{i_{h}}\preceq
v^{\prime}$. Moreover, $xz\preceq xzv$ implies that $\eta(xz)=\eta(xzv)$ by
definition. Hence, $\eta(v)=1_{G}$ since $G$ is a group. It follows that
$xyz\preceq xyzv$ by definition of $\preceq$. Since we also have
$v_{i_{h}}\preceq v^{\prime}$, one may verify from the definition of $\preceq$
that this yields $xyzv_{i_{h}}\preceq xyzvv^{\prime}$. Since
$u_{i_{h}}=xyzv_{i_{h}}$ and $u_{i_{k}}=xyzv_{i_{k}}=xyzvv^{\prime}$, this
exactly says that $u_{i_{h}}\preceq u_{i_{k}}$, contradicting the hypothesis
that $(u_{i})_{i\in{\rm Nature}}$ is bad.

We may now complete the proof and build the desired cover of the language
$H\subseteq A^{*}$. We say that a word $v\in H$ is _minimal_ if there exists
no other word $u\in H$ such that $u\preceq v$. Moreover, we define $F\subseteq
H$ as the set of all minimal words of $H$. By definition, we have
$u\not\preceq u^{\prime}$ for every $u,u^{\prime}\in F$ such that $u\neq
u^{\prime}$. Hence, it is immediate from Lemma A.5 that $F\subseteq H$ is
finite. We define $\mathbf{K}=\\{\mathord{\uparrow}_{L}u\mid u\in F\\}$. It
remains to prove that $\mathbf{K}$ is a cover of $H$. Since $\mathbf{K}$ is
finite by definition, we have to prove that for every $v\in H$, there exists
$u\in F$ such that $v\in\mathord{\uparrow}_{L}u$. We fix $v$ for the proof. If
$v$ is minimal, then $v\in F$ and it is clear that
$v\in\mathord{\uparrow}_{L}v$ since $\varepsilon\in L$. Assume now that $v$ is
_not_ minimal. In that case, there exists another word $u\in H$ which is
minimal and such that $u\preceq v$. Since $u$ is minimal, we have $u\in F$.
Thus, it suffices to prove that $v\in\mathord{\uparrow}_{L}u$. Since $u\preceq
v$, we have $v\in\mathord{\uparrow}_{L^{\prime}}u$ by definition. Moreover,
since $L^{\prime}\subseteq L$, it is immediate that
$\mathord{\uparrow}_{L^{\prime}}u\subseteq\mathord{\uparrow}_{L}u$.
Consequently, we obtain that $v\in\mathord{\uparrow}_{L}u$, which completes
the proof.

We turn to Proposition 2.7. The statement is as follows.

See 2.7

######  Proof A.7.

We write $\mathcal{A}=(Q,\delta)$ and consider the _transition morphism_ of
$\mathcal{A}$. We let $M=2^{Q^{2}}$. It is standard that $M$ is a finite
monoid for the following multiplication: given $P,P^{\prime}\in M$ (_i.e._ ,
$P,P^{\prime}\subseteq Q^{2}$), we let $PP^{\prime}=\\{(q,r)\in
Q^{2}\mid\text{there is $p\in Q$ such that $(q,p)\in P$ and $(p,r)\in
P^{\prime}$}\\}$ (the neutral element is $\\{(q,q)\mid q\in Q\\}$). The
transition morphism $\alpha:A^{*}\to M$ of $\mathcal{A}$ is defined by
$\alpha(a)=\\{(q,r)\in Q^{2}\mid(q,a,r)\in\delta\\}$ for every $a\in A$.
Recall that an idempotent $e\in M$ is an element such that $ee=e$.

We fix $k=|M|^{2}$ for the proof. We define an auxiliary alphabet
$\mathbb{B}$. Intuitively, we use a word in $\mathbb{B}^{+}$ to represent the
$\mathcal{A}$-guarded decompositions of nonempty words in $A^{+}$ with length
greater than $k$. We write $E\subseteq\alpha(A^{+})$ for the set of all
idempotents in $\alpha(A^{+})$. Consider the following sets (note that the
bound on $|w|$ in $\mathbb{B}_{r}$ differs from the ones in
$\mathbb{B}_{\ell}$, $\mathbb{B}_{c}$):

$\begin{array}[]{lll}\mathbb{B}_{\ell}&=&\\{(w,f)\in A^{+}\times E\mid|w|\leq
2k\text{ and }\alpha(w)f=\alpha(w)\\}.\\\ \mathbb{B}_{c}&=&\\{(e,w,f)\in
E\times A^{+}\times E\mid|w|\leq 2k\text{ and }e\alpha(w)f=\alpha(w)\\}.\\\
\mathbb{B}_{r}&=&\\{(e,w)\in E\times A^{+}\mid|w|\leq k\text{ and
}e\alpha(w)=\alpha(w)\\}.\end{array}$

We define $\mathbb{B}=\mathbb{B}_{\ell}\cup\mathbb{B}_{r}\cup\mathbb{B}_{c}$.
It is clear from the definition that $\mathbb{B}$ is finite. We use it as an
alphabet and define a morphism $\gamma:\mathbb{B}^{*}\to A^{*}$. Let
$b\in\mathbb{B}$. There exists a nonempty word $w\in A^{+}$ and $e,f\in E$
such that $b=(w,f)\in\mathbb{B}_{\ell}$, $b=(e,w)\in\mathbb{B}_{r}$ or
$b=(e,w,f)\in\mathbb{B}_{c}$. We define $\gamma(b)=w$. Moreover, we write
$\gamma_{c}:\mathbb{B}_{c}^{*}\to A^{*}$ for the restriction of $\gamma$ to
$\mathbb{B}_{c}^{*}$. Finally, we say that a word $x\in\mathbb{B}^{*}$ is
_well-formed_ if $x\in\mathbb{B}_{\ell}\mathbb{B}_{c}^{*}\mathbb{B}_{r}$ (in
particular, $|x|\geq 2$) and $x$ is of the form
$x=(w_{1},f_{1})(e_{2},w_{2},f_{2})\cdots(e_{n},w_{n},f_{n})(e_{n+1},w_{n+1})$
where $f_{i}=e_{i+1}$ for every $i\leq n$. We have the following lemma.

######  Lemma A.8.

Let $b_{1},\dots,b_{m}\in\mathbb{B}$ be letters such that the word
$x=b_{1}\cdots b_{m}\in\mathbb{B}^{+}$ is well-formed. Then,
$(\gamma(b_{1}),\dots,\gamma(b_{m}))$ is an $\mathcal{A}$-guarded
decomposition of the word $\gamma(x)\in A^{+}$.

######  Proof A.9.

Since $\gamma$ is a morphism, it is immediate from the definition that
$\gamma(x)=\gamma(b_{1})\cdots\gamma(b_{m})$. Hence, it suffices to verify
that for every $i<m$, there exists $z_{i}\in A^{+}$ which is a right
$\mathcal{A}$-loop for $\gamma(b_{i})$ and a left $\mathcal{A}$-loop for
$\gamma(b_{i+1})$. By definition of well-formed words, there exists an
idempotent $e_{i}\in E\subseteq\alpha(A^{+})$ such that
$\alpha(\gamma(b_{i}))e_{i}=\alpha(\gamma(b_{i}))$ and
$e_{i}\alpha(\gamma(b_{i+1}))=\alpha(\gamma(b_{i+1}))$. We let $z_{i}\in
A^{+}$ be an antecedent of $e_{i}$: we have $\alpha(z_{i})=e_{i}\in E$. It
remains to prove that $z_{i}$ is a right $\mathcal{A}$-loop for
$\gamma(b_{i})$ and a left $\mathcal{A}$-loop for $\gamma(b_{i+1})$. By
symmetry, we only prove the former. We fix $q,r\in Q$ such that
$\gamma(b_{i})\in L_{\mathcal{A}}(q,r)$ for the proof. By definition of
$\alpha$, it follows that $(q,r)\in\alpha(\gamma(b_{i}))$. Hence, since
$\alpha(\gamma(b_{i}))e_{i}=\alpha(\gamma(b_{i}))$ and $e_{i}=\alpha(z_{i})$,
we get $(q,r)\in\alpha(\gamma(b_{i})z_{i})$ which means that
$\gamma(b_{i})z_{i}\in L_{\mathcal{A}}(q,r)$. This yields $s\in Q$ such that
$\gamma(b_{i})\in L_{\mathcal{A}}(q,s)$ and $z_{i}\in L_{\mathcal{A}}(s,r)$.
Finally, since $e_{i}=\alpha(z_{i})$ is an idempotent and $z_{i}\in
L_{\mathcal{A}}(s,r)$, one may verify using a pumping argument that there
exists $t\in Q$ such that $z_{i}\in L_{\mathcal{A}}(s,t)\cap
L_{\mathcal{A}}(t,t)\cap L_{\mathcal{A}}(t,r)$. This completes the proof.

Intuitively, Lemma A.8 states that every well-formed word in
$x\in\mathbb{B}^{+}$ encodes an $\mathcal{A}$-guarded decomposition of some
word in $A^{+}$. We handle the converse direction in the following lemma: for
every long enough word $w\in A^{+}$, there exists an $\mathcal{A}$-guarded
decomposition of $w$ which is encoded by a word in $\mathbb{B}^{+}$.

######  Lemma A.10.

For every $w\in A^{+}$ such that $|w|>k$, there exists $x\in\mathbb{B}^{+}$
which is well-formed and such that $w=\gamma(x)$.

######  Proof A.11.

We proceed by induction on the length of $w$. Since $|w|>k$, there exist
$a_{0},\dots,a_{k}\in A$ and $w^{\prime}\in A^{*}$ such that
$w=w^{\prime}a_{0}\cdots a_{k}$. Since $k=|M|^{2}$, we may apply the pigeon-
hole principle to obtain $i,j$ such that $0\leq i<j\leq k$,
$\alpha(a_{0}\cdots a_{i})=\alpha(a_{0}\cdots a_{j})$ and
$\alpha(a_{i+1}\cdots a_{k})=\alpha(a_{j+1}\cdots a_{k})$. Let $u=a_{0}\cdots
a_{i}$ and $v=a_{i+1}\cdots a_{k}$. We have $u,v\in A^{+}$, $|u|\leq k$ and
$|v|\leq k$. Moreover, $w=w^{\prime}uv$. We consider the idempotent
$e=(\alpha(a_{i+1}\cdots a_{j}))^{\omega}\in E$. By definition, we have
$\alpha(u)e=\alpha(u)$ and $e\alpha(v)=\alpha(v)$. There are now two cases
depending on $w^{\prime}$.

Assume first that $|w^{\prime}|\leq k$. In that case $|w^{\prime}u|\leq 2k$
which implies that $(w^{\prime}u,e)\in\mathbb{B}_{\ell}$ since
$\alpha(u)e=\alpha(u)$. Moreover, we have $(e,v)\in\mathbb{B}_{r}$ since
$|v|\leq k$ and $e\alpha(v)=\alpha(v)$. Consequently,
$x=(w^{\prime}u,e)(e,v)\in\mathbb{B}^{+}$ is a well-formed word such that
$\gamma(x)=w^{\prime}uv=w$. Assume now that $|w^{\prime}|>k$. Since it is
clear that $|w^{\prime}|<|w|$, induction yields a well-formed word
$x^{\prime}\in\mathbb{B}^{+}$ such that $\gamma(x^{\prime})=w^{\prime}$. By
definition $x^{\prime}=x^{\prime\prime}(f,v^{\prime})$ where
$x^{\prime\prime}\in\mathbb{B}^{+}$ and $(f,v^{\prime})\in\mathbb{B}_{r}$. In
particular, we have $|v^{\prime}|\leq k$ and
$f\alpha(v^{\prime})=\alpha(v^{\prime})$ by definition of $\mathbb{B}_{r}$.
Hence, $|v^{\prime}u|\leq 2k$ which implies that
$(f,v^{\prime}u,e)\in\mathbb{B}_{c}$ since $\alpha(u)e=\alpha(u)$. Moreover,
we have $(e,v)\in\mathbb{B}_{r}$ since $|v|\leq k$ and $e\alpha(v)=\alpha(v)$.
Let $x=x^{\prime\prime}(f,v^{\prime}u,e)(e,v)$. Clearly, $x$ is well-formed
since $x^{\prime}=x^{\prime\prime}(f,v)$ was well-formed. Moreover,
$\gamma(x)=\gamma(x^{\prime\prime}(f,v^{\prime}))uv=w^{\prime}uv=w$. This
concludes the proof.

We now prove Proposition 2.7. We define
$L_{c}=\gamma_{c}^{-1}(L)\subseteq\mathbb{B}_{c}^{*}$. Since $L$ is a group
language (over $A$) and $\varepsilon\in L$, one may verify that $L_{c}$ is
also a group language (over $\mathbb{B}_{c}$) and $\varepsilon\in L_{c}$. Let
$b_{\ell}\in\mathbb{B}_{\ell}$ and $b_{r}\in\mathbb{B}_{r}$. We define,

$H_{b_{\ell},b_{r}}=\\{x\in\mathbb{B}_{c}^{*}\mid\text{$b_{\ell}xb_{r}\in\mathbb{B}^{*}$
is well-formed and $\gamma(b_{\ell}xb_{r})\in H$}\\}.$

Proposition 2.6 yields a _finite_ set $F_{b_{\ell},b_{r}}\subseteq
H_{b_{\ell},b_{r}}\subseteq\mathbb{B}_{c}^{*}$ such that
$\\{\mathord{\uparrow}_{L_{c}}x\mid x\in F_{b_{\ell},b_{r}}\\}$ is a cover of
$H_{b_{\ell},b_{r}}$. We are ready to build the desired cover $\mathbf{K}$ of
$H\subseteq A^{*}$. For every word $x=b_{1}\cdots b_{n}\in\mathbb{B}_{c}^{*}$,
every $b_{\ell}\in\mathbb{B}_{\ell}$ and every $b_{r}\in\mathbb{B}_{r}$, we
associate the language
$[x]_{b_{\ell},b_{r}}=\gamma(b_{\ell})L\gamma(b_{1})L\cdots\gamma(b_{n})L\gamma(b_{r})\subseteq
A^{+}$. Finally, we define,

$\mathbf{K}=\\{\\{w\\}\mid w\in H\text{ and }|w|\leq
k\\}\cup\bigcup_{b_{\ell}\in\mathbb{B}_{\ell}}\bigcup_{b_{r}\in\mathbb{B}_{r}}\\{[x]_{b_{\ell},b_{r}}\mid
x\in F_{b_{\ell},b_{r}}\\}.$

It remains to prove that $\mathbf{K}$ is the desired cover of $H$. First, let
us verify that every $K\in\mathbf{K}$ is of the form $K=w_{1}L\cdots
w_{n}Lw_{n+1}$ where $(w_{1},\dots,w_{n+1})$ is an $\mathcal{A}$-guarded
decomposition of some word $w\in H$. This immediate if $K=\\{w\\}$ for some
$w\in H$. We have to handle the case when $K=[x]_{b_{\ell},b_{r}}$ for some
$x\in F_{b_{\ell},b_{r}}$. By definition, $x\in H_{b_{\ell},b_{r}}$ which
means that $b_{\ell}xb_{r}\in\mathbb{B}^{*}$ is well-formed and
$\gamma(b_{\ell}xb_{r})\in H$. Let $b_{1},\dots,b_{n}\in\mathbb{B}_{c}^{*}$ be
the letters such that $x=b_{1}\cdots b_{n}$. Since $b_{\ell}b_{1}\cdots
b_{n}b_{r}\in\mathbb{B}^{*}$ is well-formed, Lemma A.8 yields that
$(\gamma(b_{\ell}),\gamma(b_{1}),\dots,\gamma(b_{n}),\gamma(b_{r}))$ is an
$\mathcal{A}$-guarded decomposition of $\gamma(b_{\ell}xb_{r})\in H$. This
concludes the proof since
$K=[x]_{b_{\ell},b_{r}}=\gamma(b_{\ell})L\gamma(b_{1})L\cdots\gamma(b_{n})L\gamma(b_{r})$.

We now prove that $\mathbf{K}$ is a cover of $H$. It is immediate by
definition that $\mathbf{K}$ is finite. Given $w\in H$, we exhibit
$K\in\mathbf{K}$ such that $w\in K$. This is immediate if $|w|\leq k$: we have
$\\{w\\}\in\mathbf{K}$ in that case. We now consider the case $|w|>k$. Lemma
A.10 yields $x\in B^{+}$ which is well-formed and such that $w=\gamma(x)$. By
definition of well-formed words $x=b_{\ell}yb_{r}$ where
$y\in\mathbb{B}_{c}^{*}$, $b_{\ell}\in\mathbb{B}_{\ell}$ and
$b_{r}\in\mathbb{B}_{r}$. Therefore, since $\gamma(x)=w\in H$, we have $y\in
H_{b_{\ell},b_{r}}$ by definition. Hence, since
$\\{\mathord{\uparrow}_{L_{c}}z\mid z\in F_{b_{\ell},b_{r}}\\}$ is a cover of
$H_{b_{\ell},b_{r}}$, we get $z\in F_{b_{\ell},b_{r}}$ such that
$y\in\mathord{\uparrow}_{L_{c}}z$. We prove that $w\in[z]_{b_{\ell},b_{r}}$
which concludes the proof since $[z]_{b_{\ell},b_{r}}\in\mathbf{K}$ by
definition. We have $\mathord{\uparrow}_{L_{c}}z=L_{c}b_{1}L_{c}\cdots
b_{n}L_{c}$ where $b_{1},\dots,b_{n}\in\mathbb{B}_{c}$ are the letters such
that $b_{1}\cdots b_{n}=z\in H_{b_{\ell},b_{r}}$. Therefore, since
$y\in\mathord{\uparrow}_{L_{c}}z$, this yields $x_{0},\dots,x_{n}\in L_{c}$
such that $y=x_{0}b_{1}x_{1}\cdots b_{n}x_{n}$. Altogether, it follows that
$x=b_{\ell}x_{0}b_{1}x_{1}\cdots b_{n}x_{n}b_{r}$. Since $w=\gamma(x)$, we get
$w=\gamma(b_{\ell})\gamma(x_{0})\gamma(b_{1})\gamma(x_{1})\cdots\gamma(b_{n})\gamma(x_{n})\gamma(b_{r})$.
Finally, since $L_{c}=\gamma_{c}^{-1}(L)$ and $x_{0},\dots,x_{n}\in L_{c}$, we
have $\gamma(x_{i})\in L$ for every $i\leq n$. Hence, we obtain that
$w\in\gamma(b_{\ell})L\gamma(b_{1})L\cdots\gamma(b_{n})L\gamma(b_{r})$. This
exactly says that $w\in[z]_{b_{\ell},b_{r}}$ since $b_{1}\cdots b_{n}=z$ by
definition. This concludes the proof.

##  Appendix B Appendix to Section 3

We present the missing proofs for the statements in Section 3. We start with
those concerning classical separation.

###  B.1 Non-separable quadruples

We first prove Lemma 3.1. The statement is as follows.

See 3.1

######  Proof B.1.

Given $K\in\mathcal{C}$ such that $L_{0}H_{0}\subseteq K$, we prove that
$L_{1}H_{1}\cap K\neq\emptyset$. Consider the two following languages:

$U=\bigcap_{w\in H_{0}}Kw^{-1}\quad\text{and}\quad V=\bigcap_{u\in U}u^{-1}K.$

Since $K\in\mathcal{C}$ is regular, it has finitely many quotients by the
Myhill-Nerode theorem. Therefore, while the above intersections may be
infinite, they boil down to finite ones. Since $\mathcal{C}$ is a prevariety
and $K\in\mathcal{C}$, it follows that $U,V\in\mathcal{C}$. Moreover,
$L_{0}\subseteq U$. Indeed, if $x\in L_{0}$, then for every $w\in H_{0}$ we
have $xw\in L_{0}H_{0}\subseteq K$ which yields $x\in U$ by definition of $U$.
Therefore, since $L_{0}$ is not $\mathcal{C}$-separable from $L_{1}$, we get
$L_{1}\cap U\neq\emptyset$. We fix $u\in L_{1}\cap U$. Additionally,
$H_{0}\subseteq V$. Indeed, if $y\in H_{0}$, then for every $x\in U$, we have
$xy\in K$ which yields $y\in V$ by definition. Consequently, since $H_{0}$ is
not $\mathcal{C}$-separable from $H_{1}$, we get $H_{1}\cap V\neq\emptyset$.
Let $v\in H_{1}\cap V$. Altogether, we have $uv\in L_{1}H_{1}$, $u\in U$ and
$v\in V$. By definition of $V$, we get $uv\in K$. Hence, $L_{1}H_{1}\cap
K\neq\emptyset$ as desired.

We first consider Proposition 3.2. The statement is as follows.

See 3.2

######  Proof B.2.

Assume first that $L_{\mathcal{A}}(I_{1},F_{1})$ is $\mathcal{C}$-separable
from $L_{\mathcal{A}}(I_{2},F_{2})$. This yields a separator
$K\in\mathcal{C}$. It is clear that for every $(q_{1},r_{1},q_{2},r_{2})\in
I_{1}\times F_{1}\times I_{2}\times F_{2}$, $K\in\mathcal{C}$ also separates
$L_{\mathcal{A}}(q_{1},r_{1})$ from $L_{\mathcal{A}}(q_{2},r_{2})$ (these two
languages are included in $L_{\mathcal{A}}(I_{1},F_{1})$ and
$L_{\mathcal{A}}(I_{2},F_{2})$ respectively). Thus, $\left(I_{1}\times
F_{1}\times I_{2}\times
F_{2}\right)\cap\mathcal{I}_{\mathcal{C}}[\mathcal{A}]=\emptyset$ by
definition of $\mathcal{I}_{\mathcal{C}}[\mathcal{A}]$.

Conversely, assume that $\left(I_{1}\times F_{1}\times I_{2}\times
F_{2}\right)\cap\mathcal{I}_{\mathcal{C}}[\mathcal{A}]=\emptyset$. By
definition, this means that for every $(q_{1},r_{1},q_{2},r_{2})\in
I_{1}\times F_{1}\times I_{2}\times F_{2}$, there exists a language
$K_{q_{1},r_{1},q_{2},r_{2}}\in\mathcal{C}$ which separates
$L_{\mathcal{A}}(q_{1},r_{1})$ from $L_{\mathcal{A}}(q_{2},r_{2})$. Consider
the following language:

$K=\bigcup_{(q_{1},r_{1})\in I_{1}\times F_{1}}\left(\bigcap_{(q_{2},r_{2})\in
I_{2}\times F_{2}}K_{q_{1},r_{1},q_{2},r_{2}}\right).$

Since $\mathcal{C}$ is a lattice, we have $K\in\mathcal{C}$. Moreover, one may
verify that $K$ separates $L_{\mathcal{A}}(I_{1},F_{1})$ from
$L_{\mathcal{A}}(I_{2},F_{2})$, concluding the proof.

We now prove Lemma 3.3 whose statement is the following.

See 3.3

######  Proof B.3.

By definition of $\mathcal{I}_{\mathcal{C}}[\mathcal{A}]$, for every quadruple
$\bar{q}=(q,r,s,t)\in Q^{4}\setminus\mathcal{I}_{\mathcal{C}}[\mathcal{A}]$,
there exists $H_{\bar{q}}\in\mathcal{C}$ which separates
$L_{\mathcal{A}}(q,r)$ from $L_{\mathcal{A}}(s,t)$. We use the languages
$H_{\bar{q}}$ to define the following equivalence $\sim$ on $A^{*}$: for
$u,v\in A^{*}$, we let $u\sim v$ if and only if $u\in
H_{\bar{q}}\Leftrightarrow v\in H_{\bar{q}}$ for every $\bar{q}\in
Q^{4}\setminus\mathcal{I}_{\mathcal{C}}[\mathcal{A}]$. Let $\mathbf{K}$ be the
partition of $A^{*}$ into $\sim$-classes. By definition, each $K\in\mathbf{K}$
is a Boolean combination of languages $H_{\bar{q}}\in\mathcal{C}$. Hence,
$K\in\mathcal{C}$ since $\mathcal{C}$ is a Boolean algebra. We conclude that
$\mathbf{K}$ is a $\mathcal{C}$-cover of $A^{*}$. Moreover, one may verify
from the definition of the languages $H_{\bar{q}}$ that $\mathbf{K}$ is
separating for $\mathcal{I}_{\mathcal{C}}[\mathcal{A}]$.

For the second assertion, we let $S\subseteq Q^{4}$ and consider a
$\mathcal{C}$-cover $\mathbf{K}$ of $A^{*}$ which is separating for $S$. We
show that $Q^{4}\setminus S\subseteq
Q^{4}\setminus\mathcal{I}_{\mathcal{C}}[\mathcal{A}]$. By definition, this
boils down to proving that if $(q,r,s,t)\in Q^{4}\setminus S$, then
$L_{\mathcal{A}}(q,r)$ is $\mathcal{C}$-separable from $L_{\mathcal{A}}(s,t)$.
We build a separator $H\in\mathcal{C}$ from $\mathbf{K}$. Let
$H\in\mathcal{C}$ be the union of all languages $K\in\mathbf{K}$ such that
$K\cap L_{\mathcal{A}}(q,r)\neq\emptyset$. Clearly,
$L_{\mathcal{A}}(q,r)\subseteq H$ since $\mathbf{K}$ is a cover of $A^{*}$. It
remains to prove that $H\cap L_{\mathcal{A}}(s,t)=\emptyset$. By
contradiction, assume that $H\cap L_{\mathcal{A}}(s,t)\neq\emptyset$. By
definition of $H$, this yields $K\in\mathbf{K}$ such that $K\cap
L_{\mathcal{A}}(q,r)\neq\emptyset$ and $K\cap
L_{\mathcal{A}}(s,t)\neq\emptyset$. Since $\mathbf{K}$ is separating for $S$,
it follows that $(q,r,s,t)\in S$ which is a contradiction since $(q,r,s,t)\in
Q^{4}\setminus S$.

We turn to Proposition 3.4. The statement is as follows.

See 3.4

######  Proof B.4.

For every quadruple $\bar{(}q)=(q,r,s,t)\in
Q^{4}\setminus\mathcal{I}_{\mathcal{C}}[\mathcal{D},\mathcal{A}]$, there
exists $L_{\bar{q}}\in\mathcal{D}$ such that $\varepsilon\in\mathcal{D}$ and
$H_{\bar{q}}\in\mathcal{C}$ which separates $L_{\mathcal{A}}(q,r)\cap
L_{\bar{q}}$ from $L_{\mathcal{A}}(s,t)\cap L_{\bar{q}}$. We define
$L\in\mathcal{D}$ as the intersection of all languages $L_{\bar{q}}$ for
$\bar{q}\in Q^{4}\setminus\mathcal{I}_{\mathcal{C}}[\mathcal{D},\mathcal{A}]$.
Clearly, we have $\varepsilon\in L$. Moreover, we define an equivalence $\sim$
on $L$: for $u,v\in L$, we let $u\sim v$ if and only if $u\in
H_{\bar{q}}\Leftrightarrow v\in H_{\bar{q}}$ for every $\bar{q}\in
Q^{4}\setminus\mathcal{I}_{\mathcal{C}}[\mathcal{D},\mathcal{A}]$. Finally, we
let $\mathbf{K}$ be the partition of $L$ into $\sim$-classes. By definition,
each $K\in\mathbf{K}$ is a Boolean combination involving the languages
$H_{\bar{q}}\in\mathcal{C}$ and $L\in\mathcal{D}\subseteq\mathcal{C}$. Hence,
$K\in\mathcal{C}$ since $\mathcal{C}$ is a Boolean algebra. We conclude that
$\mathbf{K}$ is a $\mathcal{C}$-cover of $L$. Moreover, one may verify from
the definition of the languages $H_{\bar{q}}$ that $\mathbf{K}$ is separating
for $\mathcal{I}_{\mathcal{C}}[\mathcal{D},\mathcal{A}]$.

For the second assertion, we let $S\subseteq Q^{4}$. Consider
$L\in\mathcal{D}$ such that $\varepsilon\in L$ and a $\mathcal{C}$-cover
$\mathbf{K}$ of $L$ which is separating for $S$. We show that $Q^{4}\setminus
S\subseteq Q^{4}\setminus\mathcal{I}_{\mathcal{C}}[\mathcal{D},\mathcal{A}]$.
By definition,it suffices to prove that if $(q,r,s,t)\in Q^{4}\setminus S$,
then $L_{\mathcal{A}}(q,r)\cap L$ is $\mathcal{C}$-separable from
$L_{\mathcal{A}}(s,t)\cap L$. We build a separator $H\in\mathcal{C}$ from
$\mathbf{K}$. Let $H\in\mathcal{C}$ be the union of all languages
$K\in\mathbf{K}$ such that $K\cap L_{\mathcal{A}}(q,r)\cap L\neq\emptyset$.
Clearly, $L_{\mathcal{A}}(q,r)\cap L\subseteq H$ since $\mathbf{K}$ is a cover
of $L$. It remains to prove that $H\cap L_{\mathcal{A}}(s,t)\cap L=\emptyset$.
By contradiction, assume that $H\cap L_{\mathcal{A}}(s,t)\cap L\neq\emptyset$.
By definition of $H$, this yields $K\in\mathbf{K}$ such that $K\cap
L_{\mathcal{A}}(q,r)\cap L\neq\emptyset$ and $K\cap L_{\mathcal{A}}(s,t)\cap
L\neq\emptyset$. Since $\mathbf{K}$ is separating for $S$, we get
$(q,r,s,t)\in S$. This is a contradiction since $(q,r,s,t)\in Q^{4}\setminus
S$.

###  B.2 Tuple separation

We now present proofs for the statements concerning tuple separation. We start
with Lemma 3.8.

See 3.8

######  Proof B.5.

We proceed by induction on $n\geq 1$. If $n=1$, then $(L_{1})$ and $(H_{1})$
being not $\mathcal{C}$-separable means that $L_{1}\neq\emptyset$ and
$H_{1}\neq\emptyset$. Hence, $L_{1}H_{1}\neq\emptyset$ which implies that
$(L_{1}H_{1})$ is not $\mathcal{C}$-separable. Assume now $n>1$ and consider
$(L_{1},\dots,L_{n}),(H_{1},\dots,H_{n})$ which are not
$\mathcal{C}$-separable. Given $K\in\mathcal{C}$ such that
$L_{1}H_{1}\subseteq K$, we prove that $(L_{2}H_{2},\dots,L_{n}H_{n})\cap K$
is not $\mathcal{C}$-separable. Consider the two following languages:

$U=\bigcap_{w\in H_{1}}Kw^{-1}\quad\text{and}\quad V=\bigcap_{u\in U}u^{-1}K.$

Note that since $K\in\mathcal{C}$ is regular, it has finitely many quotients
by the Myhill-Nerode theorem. Hence, while the above intersections may be
infinite, they boil down to finite ones. Since $\mathcal{C}$ is a prevariety
and $K\in\mathcal{C}$, it follows that $U,V\in\mathcal{C}$.

Observe that $L_{1}\subseteq U$. Indeed, if $x\in L_{1}$, then for every $w\in
H_{1}$ we have $xw\in L_{1}H_{1}\subseteq K$ which yields $x\in U$ by
definition. Since $(L_{1},\dots,L_{n})$ is not $\mathcal{C}$-separable, it
follows that $(L_{2},\dots,L_{n})\cap U$ is not $\mathcal{C}$-separable.
Moreover, observe that $H_{1}\subseteq V$. Indeed, if $y\in H_{1}$, then for
every $x\in U$, we have $xy\in K$ which yields $y\in V$ by definition. Since
$(H_{1},\dots,H_{n})$ is not $\mathcal{C}$-separable, it follows that
$(H_{2},\dots,H_{n})\cap V$ is not $\mathcal{C}$-separable. It now follows
from induction on $n$ that $((L_{2}\cap U)(H_{2}\cap V),\dots,(L_{n}\cap
U)(H_{n}\cap V))$ is not $\mathcal{C}$-separable. It is clear that $(L_{i}\cap
U)(H_{i}\cap V)\subseteq(L_{i}H_{i})\cap(UV)$ for every $i\leq n$. Moreover,
observe that $UV\subseteq K$. Indeed, if $u\in U$ and $v\in V$, we have $uv\in
K$ by definition of $V$. Altogether, it follows from the second assertion in
Lemma 3.7 that $(L_{2}H_{2},\dots,L_{n}H_{n})\cap K$ is not
$\mathcal{C}$-separable, which completes the proof.

We turn to Corollary 3.9. As we explained in the main paper, this statement
follows from a theorem of [18] which we first recall and prove.

######  Theorem B.6.

Let $\mathcal{C}$ be a lattice and $L_{0},L_{1}\subseteq A^{*}$. The following
properties are equivalent:

  1. 1.

$L_{0}$ is $\mathit{Bool}(\mathcal{C})$ separable from $L_{1}$.

  2. 2.

There exists $p\geq 1$ and such that $(L_{0},L_{1})^{p}$ is
$\mathcal{C}$-separable.

######  Proof B.7.

We first prove that $2)\Rightarrow 1)$. Let $L_{0},L_{1}\subseteq A^{*}$ and
assume that there exists $p\geq 1$ such that $(L_{0},L_{1})^{p}$ is
$\mathcal{C}$-separable. We use induction on $p$ to prove that $L_{0}$ is
$\mathit{Bool}(\mathcal{C})$-separable from $L_{1}$. When $p=1$, $L_{0}$ is
$\mathcal{C}$-separable from $L_{1}$ and since
$\mathcal{C}\subseteq\mathit{Bool}(\mathcal{C})$, the result is trivial.
Assume that $p\geq 2$. By hypothesis, we have $K,K^{\prime}\in\mathcal{C}$
such that $L_{0}\subseteq K$, $L_{1}\cap K\subseteq K^{\prime}$ and
$(L_{0},L_{1})^{p-1}\cap K\cap K^{\prime}$ is $\mathcal{C}$-separable. Using
induction, we then obtain a language $P\in\mathit{Bool}(\mathcal{C})$
separating $L_{0}\cap K\cap K^{\prime}$ from $L_{1}\cap K\cap K^{\prime}$.
Consider the language $H=(K\cap P)\cup(K\setminus
K^{\prime})\in\mathit{Bool}(\mathcal{C})$. We prove that $H$ separates $L_{0}$
from $L_{1}$. We begin with $L_{0}\subseteq H$. Let $w\in L_{0}$, we prove
that $w\in H$. Clearly, $w\in K$ since $L_{0}\subseteq K$. Moreover, either
$w\in K^{\prime}$ and therefore $w\in K\cap P$ since $L_{0}\cap K\cap
K^{\prime}\subseteq P$, or $w\not\in K^{\prime}$ and therefore $w\in
K\setminus K^{\prime}$. Altogether, we conclude that $w\in H$. It remains to
prove that $L_{1}\cap H=\emptyset$. Let $w\in L_{1}$, we prove that $w\not\in
H$. There are two cases depending on whether $w\in K$. If $w\not\in K$, then
clearly $w\not\in K\cap P$ and $w\not\in K\setminus K^{\prime}$, hence
$w\not\in H$. Otherwise, $w\in L_{1}\cap K\subseteq K^{\prime}$. Therefore,
$w\not\in K\setminus K^{\prime}$ and $w\not\in K\cap P$ since $L_{1}\cap K\cap
K^{\prime}\cap P=\emptyset$ by the choice of $P$. We get $w\not\in H$, which
completes the proof.

We turn to the implication $1)\Rightarrow 2)$ in Theorem B.6. We start with an
auxiliary lemma.

######  Lemma B.8.

Let $k\geq 1$ and $(L_{1},\dots,L_{k})$ be a $k$-tuple. Moreover, let
$K_{1},K_{2}\in\mathcal{C}$ be such that $(L_{1},\dots,L_{k})\cap K_{1}$ and
$(L_{1},\dots,L_{k})\cap K_{2}$ are both $\mathcal{C}$-separable. Then,
$(L_{1},\dots,L_{k})\cap(K_{1}\cup K_{2})$ is $\mathcal{C}$-separable as well.

######  Proof B.9.

We proceed by induction on $k$. When $k=1$, then we have $L_{1}\cap
K_{1}=\emptyset$ and $L_{1}\cap K_{2}=\emptyset$ by hypothesis. Hence,
$L_{1}\cap(K_{1}\cup K_{2})=\emptyset$ and $(L_{1})\cap(K_{1}\cup K_{2})$ is
$\mathcal{C}$-separable. When $k\geq 2$, for $i=1,2$, our hypothesis yields a
separator $U_{i}\in\mathcal{C}$ for $(L_{1},\dots,L_{k})\cap K_{i}$. We prove
that $U=(U_{1}\cap K_{1})\cup(U_{2}\cap K_{2})\in\mathcal{C}$ is a separator
for $(L_{1},\dots,L_{k})\cap(K_{1}\cup K_{2})$. It is clear that
$L_{1}\cap(K_{1}\cup K_{2})\subseteq U$ since we have $L_{1}\cap
K_{1}\subseteq U_{1}$ and $L_{2}\cap K_{2}\subseteq U_{2}$ by definition of
$U_{1}$ and $U_{2}$. Moreover, we know that $(L_{2},\dots,L_{k})\cap K_{1}\cap
U_{1}$ and $(L_{2},\dots,L_{k})\cap K_{2}\cap U_{2}$ are both
$\mathcal{C}$-separable. Thus, it is immediate from induction that
$(L_{2},\dots,L_{k})\cap U$ is $\mathcal{C}$-separable, concluding the proof.

We now concentrate on proving the implication $1)\Rightarrow 2)$ in Theorem
B.6. Given $L_{0},L_{1}\subseteq A^{*}$ which are
$\mathit{Bool}(\mathcal{C})$-separable, we have to prove that there exists
$p\geq 1$ such that $(L_{0},L_{1})^{p}$ is $\mathcal{C}$-separable. By
hypothesis there exists a language $K\in\mathit{Bool}(\mathcal{C})$ such that
$L_{0}\subseteq K$ and $L_{1}\cap K=\emptyset$. By definition, $K$ is the
Boolean combination of languages in $\mathcal{C}$. We put it in disjunctive
normal form. Each disjunct is an intersection languages belonging to