Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400, Talence, France
and
http://www.labri.fr/perso/tplacetplace@labri.frhttps://orcid.org/0009-0000-2840-9586
Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400, Talence, France
and
http://www.labri.fr/perso/zeitounmz@labri.frhttps://orcid.org/0000-0003-4101-8437
Thomas Place and Marc Zeitoun [500]Theory of computation Formal languages and
automata theory [cite=pz_gen_tl_csl]Extended version 2024 6

# A generic characterization of generalized unary temporal logic and two-
variable first-order logic

Thomas Place  Marc Zeitoun

###### Abstract

We study an operator on classes of languages. For each class $\mathcal{C}$, it
produces a new class $\textup{FO}^{2}(\mathbb{I}_{\mathcal{C}})$ associated
with a variant of two-variable first-order logic equipped with a signature
$\mathbb{I}_{\mathcal{C}}$ built from $\mathcal{C}$. For
$\mathcal{C}=\\{\emptyset,A^{*}\\}$, we obtain the usual $\textup{FO}^{2}(<)$
logic, equipped with linear order. For
$\mathcal{C}=\\{\emptyset,\\{\varepsilon\\},A^{+},A^{*}\\}$, we get the
variant $\textup{FO}^{2}(<,+1)$, which also includes the successor predicate.
If $\mathcal{C}$ consists of all Boolean combinations of languages
$A^{*}aA^{*}$, where $a$ is a letter, we get the variant
$\textup{FO}^{2}(<,\mathit{Bet})$, which includes “between” relations. We
prove a _generic_ algebraic characterization of the classes
$\textup{FO}^{2}(\mathbb{I}_{\mathcal{C}})$. It elegantly generalizes those
known for all the cases mentioned above. Moreover, it implies that if
$\mathcal{C}$ has decidable separation (plus some standard properties), then
$\textup{FO}^{2}(\mathbb{I}_{\mathcal{C}})$ has a decidable membership
problem.

We actually work with an equivalent definition of
$\textup{FO}^{2}(\mathbb{I}_{\mathcal{C}})$ in terms of _unary temporal
logic_. For each class $\mathcal{C}$, we consider a variant
$\textup{TL}(\mathcal{C})$ of unary temporal logic whose future/past
modalities depend on $\mathcal{C}$ and such that
$\textup{TL}(\mathcal{C})=\textup{FO}^{2}(\mathbb{I}_{\mathcal{C}})$. Finally,
we also characterize $\textup{FL}(\mathcal{C})$ and
$\textup{PL}(\mathcal{C})$, the pure-future and pure-past restrictions of
$\textup{TL}(\mathcal{C})$. Like for $\textup{TL}(\mathcal{C})$, these
characterizations imply that if $\mathcal{C}$ is a class with decidable
separation, then $\textup{FL}(\mathcal{C})$ and $\textup{PL}(\mathcal{C})$
have decidable membership.

###### keywords:

Classes of regular languages, Generalized unary temporal logic, Generalized
two-variable first-order logic, Generic decidable characterizations,
Membership, Separation

###### category:

##  1 Introduction

Context. Regular languages of finite words form a robust class: they admit a
wide variety of equivalent definitions, whether by regular expressions, finite
automata, finite monoids or monadic second-order logic. It is therefore
natural to study the _fragments_ of regular languages obtained by restricting
the syntax of one of the above-mentioned formalisms. For each particular
fragment, we seek to prove that it has a decidable _membership problem_ :
given a regular language as input, decide whether it belongs to the fragment.
Intuitively, doing so requires a thorough knowledge of the fragment and the
languages it can describe.

This approach was initiated by Schützenberger [30] for the class SF of star-
free languages. These are the languages defined by a _star-free expression_ :
a regular expression without Kleene star but with complement instead.
Equivalently, these are the languages that can be defined in first-order logic
with the linear order [16] ($\textup{FO}(<)$) or in linear temporal logic [11]
(LTL). Schützenberger established an algebraic characterization of SF: a
regular language is star-free if and only if its _syntactic monoid is
aperiodic_. This yields a membership procedure for SF because the syntactic
monoid can be computed and aperiodicity is a decidable property.

Operators. This seminal result prompted researchers to look at other natural
classes, spawning a fruitful line of research (see _e.g._ , [4, 33, 12, 18,
36, 24]). Although there are numerous classes, they can be grouped into
families based on “variants” of the same syntax. Let us use logic to clarify
this point. Each logical fragment can use several _signatures_ (_i.e._ , sets
of predicates allowed in formulas), each giving rise to a class. For instance,
first-order logic is commonly equipped with predicates such as the linear
order “$<$” [16, 30], the successor “$+1$” [3] or the modular predicates
“$\mathit{MOD}$” [2]. While it is worth looking at multiple variants of
prominent classes, doing so individually for each of them has an obvious
disadvantage: the proof has to be systematically modified to accommodate each
change. This can be tedious, difficult, and not necessarily enlightening. To
overcome this drawback, a natural approach is to capture a whole family of
variants with an _operator_. An operator “Op” takes a class $\mathcal{C}$ as
input, and outputs a larger one $\textup{Op}(\mathcal{C})$. Thus, we can study
all classes $\textup{Op}(\mathcal{C})$ _simultaneously_ : the question
becomes: “what hypotheses about $\mathcal{C}$ guarantee the decidability of
$\textup{Op}(\mathcal{C})$-membership?”. For example, one can generalize the
three definitions of star-free languages through operators:

  1. 1.

The _star-free closure_ $\mathcal{C}\mapsto\textup{{SF}}(\mathcal{C})$ has
been introduced in [31, 34]. Languages in $\textup{{SF}}(\mathcal{C})$ are
defined by “extended” star-free expressions, which can freely use languages
from $\mathcal{C}$.

  2. 2.

A construction associating a signature $\mathbb{I}_{\mathcal{C}}$ to a class
$\mathcal{C}$ has been given in [23]. For each $L\in\mathcal{C}$, the set
$\mathbb{I}_{\mathcal{C}}$ contains a binary predicate $I_{L}(x,y)$: for a
word $w$ and two positions $i,j$ in $w$, $I_{L}(i,j)$ holds if and only if
$i<j$ and the infix of $w$ between $i$ and $j$ belongs to $L$. We get an
operator $\mathcal{C}\mapsto\textup{FO}(\mathbb{I}_{\mathcal{C}})$ based on
first-order logic. It captures many choices of signature.

  3. 3.

Similarly, an operator $\mathcal{C}\mapsto\textup{LTL}(\mathcal{C})$ that
generalizes LTL has been defined in [28].

It is shown in [23, 28] that
$\textup{{SF}}(\mathcal{C})=\textup{FO}(\mathbb{I}_{\mathcal{C}})=\textup{LTL}(\mathcal{C})$
for any class $\mathcal{C}$ (with mild hypotheses). Moreover, a _generic_
algebraic characterization is proved in [25, 28]. Given a regular language
$L$, it relies on a construction that identifies monoids inside its syntactic
monoid, called the _$\mathcal{C}$ -orbits_: $L\in\textup{{SF}}(\mathcal{C})$
if and only if its $\mathcal{C}$-orbits are all _aperiodic_. This elegantly
generalizes Schützenberger’s theorem and gives a _transfer theorem_ for
membership. Indeed, the $\mathcal{C}$-orbits are connected with a decision
problem that strengthens membership: _$\mathcal{C}$ -separation_. Given _two_
input regular languages $L_{1}$ and $L_{2}$, $\mathcal{C}$-separation asks
whether there is $K\in\mathcal{C}$ such that $L_{1}\subseteq K$ and $L_{2}\cap
K=\emptyset$. The crucial point is that $\mathcal{C}$-orbits are computable if
$\mathcal{C}$-separation is decidable. Thus,
$\textup{{SF}}(\mathcal{C})$-membership is also decidable in this case.
Similar results are known for other operators such as _polynomial closure_
[23] or its _unambiguous_ restriction [22, 27].

Unary temporal logic and two-variable first-order logic. The operator we
investigate generalizes another important class admitting multiple definitions
[35, 6] (see [8, 7] for extensions). We are interested in two of them. It
consists of languages that can be defined in _two-variable first-order logic_
with the linear order ($\textup{FO}^{2}(<)$) or equivalently in _unary
temporal logic_ (TL) with the modalities F (sometimes in the future) and P
(sometimes in the past). Etessami, Vardi and Wilke [9] have shown that
$\textup{FO}^{2}(<)=\textup{TL}$. Its algebraic characterization by Thérien
and Wilke [36] is one of the famous results of this type: a regular language
belongs to $\textup{FO}^{2}(<)=\textup{TL}$ if and only if its syntactic
monoid belongs to the variety of monoids DA.

Both definitions extend to natural operators. First, the generic signatures
$\mathbb{I}_{\mathcal{C}}$ yield an operator
$\mathcal{C}\mapsto\textup{FO}^{2}(\mathbb{I}_{\mathcal{C}})$ based on
$\textup{FO}^{2}$. Second, an operator
$\mathcal{C}\mapsto\textup{TL}(\mathcal{C})$ has been defined in [27]. It
enriches TL with new modalities $\textup{F}_{L}$ and $\textup{P}_{L}$, both
depending on the languages $L\in\mathcal{C}$. For example, the formula
$\textup{F}_{L}\,\varphi$ holds at a position $i$ in a word $w$ if there is a
position $j>i$ in $w$ such that $\varphi$ holds at $j$ and the infix between
$i$ and $j$ belongs to $L$. We know that
$\textup{FO}^{2}(\mathbb{I}_{\mathcal{C}})=\textup{TL}(\mathcal{C})$ when
$\mathcal{C}$ is closed under Boolean operations [27]. Here, we work with the
$\textup{TL}(\cdot)$ operator, which encompasses all classic classes based on
two-variable first-order logic or unary temporal logic. This includes the
original variants $\textup{FO}^{2}(<)=\textup{TL}$ and
$\textup{FO}^{2}(<,+1)=\textup{TLX}$, both of which were studied by Thérien
and Wilke [36] (here, “$+1$” is the successor predicate and TLX is defined by
enriching TL with “next” and “yesterday” modalities). Another example is the
variant $\textup{FO}^{2}(<,\mathit{MOD})$ endowed with _modular predicates_ ,
investigated by Dartois and Paperman [5]. Finally, we capture the variant
$\textup{FO}^{2}(<,Bet)=\textup{BInvTL}$ equipped with “ _between_ ”
relations, defined and characterized by Krebs, Lodaya, Pandya and Straubing
[13, 14, 15].

Contributions. We prove a _generic_ algebraic characterization of the classes
$\textup{FO}^{2}(\mathbb{I}_{\mathcal{C}})=\textup{TL}(\mathcal{C})$. We reuse
the $\mathcal{C}$-orbits introduced for star-free closure: for any class
$\mathcal{C}$ (having mild properties) we show that a regular language belongs
to $\textup{TL}(\mathcal{C})$ if and only if all $\mathcal{C}$-orbits of its
syntactic monoid belong to DA. In particular, this yields a _transfer theorem_
for membership: if $\mathcal{C}$ has decidable _separation_ , then
$\textup{FO}^{2}(\mathbb{I}_{\mathcal{C}})=\textup{TL}(\mathcal{C})$ has
decidable membership. Moreover, this characterization generalizes the
characterizations known for all the above instances.

A key feature of our proof is that we use a third auxiliary operator. It
combines two other operators: Boolean polynomial closure (BPol) and
unambiguous polynomial closure (UPol). We have
$\textup{UPol}(\textup{BPol}(\mathcal{C}))\subseteq\textup{TL}(\mathcal{C})$
if $\mathcal{C}$ has mild properties [27]. In fact, for many natural classes,
$\textup{UPol}(\textup{BPol}(\mathcal{C}))\,{=}\,\textup{TL}(\mathcal{C})$.
For example, $\textup{UPol}(\textup{BPol}(\\{\emptyset,A^{*}\\}))$ is the
class UL of  _unambiguous languages_ defined by Schützenberger [32]. It is
known [36] that $\textup{UL}=\textup{TL}=\textup{FO}^{2}(<)$. More generally,
$\textup{UPol}(\textup{BPol}(\mathcal{C}))=\textup{TL}(\mathcal{C})$ for every
class $\mathcal{C}$ consisting of _group languages_ [27]. Yet, this is a
strong hypothesis and the inclusion
$\textup{UPol}(\textup{BPol}(\mathcal{C}))\subseteq\textup{TL}(\mathcal{C})$
is _strict_ in general. For example, the results of [15] imply that
$\textup{UPol}(\textup{BPol}(\and))\neq\textup{TL}(\and)$, where and consists
of all Boolean combinations of languages $A^{*}aA^{*}$ (with $a\in A$).
Nevertheless, the classes $\textup{UPol}(\textup{BPol}(\mathcal{C}))$ serve as
a central ingredient in the most difficult direction of our proof: “ _If a
language satisfies our characterization on $\mathcal{C}$-orbits, prove that it
belongs to $\textup{TL}(\mathcal{C})$_”. More precisely, we exploit the known
characterization of $\textup{UPol}(\textup{BPol}(\mathcal{C}))$ to prove that
auxiliary languages belong to this class, and we then conclude using the
inclusion
$\textup{UPol}(\textup{BPol}(\mathcal{C}))\subseteq\textup{TL}(\mathcal{C})$.

Finally, we look at two additional operators:
$\mathcal{C}\mapsto\textup{FL}(\mathcal{C})$ and
$\mathcal{C}\mapsto\textup{PL}(\mathcal{C})$. They are also defined in terms
of unary temporal logic, as the pure-future and the pure-past restrictions of
$\mathcal{C}\mapsto\textup{TL}(\mathcal{C})$. We present generic algebraic
characterizations for these two operators as well. Again, they are based on
$\mathcal{C}$-orbits. For every class $\mathcal{C}$ (with mild hypotheses), we
show that a regular language belongs to $\textup{FL}(\mathcal{C})$ (resp.
$\textup{PL}(\mathcal{C})$) if and only if all the $\mathcal{C}$-orbits inside
its syntactic monoid are $\mathrel{\mathscr{L}}$-trivial (resp.
$\mathrel{\mathscr{R}}$-trivial) monoids. As before, these results yield
_transfer theorems_ : if $\mathcal{C}$ has decidable _separation_ , then
$\textup{FL}(\mathcal{C})$ and $\textup{PL}(\mathcal{C})$ have decidable
membership.

Organization of the paper. We recall the notation and background in Section 2.
In Section 3, we present the $\mathcal{C}$-orbits and their properties. In
Section 4, we define the operator
$\mathcal{C}\mapsto\textup{TL}(\mathcal{C})$. Section 5 is devoted to the
generic characterization of $\textup{TL}(\mathcal{C})$ and to its proof. In
Section 6, finally, we state the characterizations of the pure-future and
pure-past restrictions of $\textup{TL}(\mathcal{C})$.

##  2 Preliminaries

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$. A
_language_ is a subset of $A^{*}$. We let
$A^{+}=A^{*}\setminus\\{\varepsilon\\}$. For $u,v\in A^{*}$, we write $uv$ for
the word obtained by concatenating $u$ and $v$. We lift the concatenation to
languages as follows: if $K,L\subseteq A^{*}$, we let $KL=\\{uv\mid u\in
K,v\in L\\}$. If $w\in A^{*}$, we write $|w|\in{\rm Nature}$ for its length. A
word $w=a_{1}\cdots a_{|w|}\in A^{*}$ is viewed as an _ordered set
$\textup{{Pos}}(w)=\\{0,1,\dots,|w|,|w|+1\\}$ of $|w|+2$ positions_. In
addition, we let
$\textup{{Pos}}_{c}(w)=\\{1,\dots,|w|\\}\subsetneq\textup{{Pos}}(w)$. Position
$i\in\textup{{Pos}}_{c}(w)$ carries label $a_{i}\in A$, which we write
$w[i]=a_{i}$. On the other hand, positions $0$ and $|w|+1$ carry _no label_.
We write $w[0]=min$ and $w[|w|+1]=max$. For $v,w\in A^{*}$, we say that $v$ is
an _infix_ (resp.  _prefix_ , _suffix_) of $w$ when there exist $x,y\in A^{*}$
such that $w=xvy$ (resp. $w=vy$, $w=xv$). Given a word $w=a_{1}\cdots
a_{|w|}\in A^{*}$ and $i,j\in\textup{{Pos}}(w)$ such that $i<j$, we write
$w(i,j)=a_{i+1}\cdots a_{j-1}\in A^{*}$ (_i.e._ , the infix obtained by
keeping the letters carried by positions _strictly_ between $i$ and $j$).

Classes. A _class_ of languages $\mathcal{C}$ is simply a set of languages.
Such a class $\mathcal{C}$ is a _lattice_ when $\emptyset\in\mathcal{C}$,
$A^{*}\in\mathcal{C}$ and $\mathcal{C}$ is closed under both union and
intersection: for all $K,L\in\mathcal{C}$, we have $K\cup L\in\mathcal{C}$ and
$K\cap L\in\mathcal{C}$. Moreover, a class of languages $\mathcal{C}$ is a
_Boolean algebra_ if it is a lattice closed under complement: for all
$L\in\mathcal{C}$, we have $A^{*}\setminus L\in\mathcal{C}$. Finally, the
class $\mathcal{C}$ is _closed under quotients_ if for all $L\in\mathcal{C}$
and $u\in A^{*}$, we have $u^{-1}L\stackrel{{\scriptstyle\smash{\text{\tiny
def}}}}{{=}}\\{w\in A^{*}\mid uw\in L\\}\in\mathcal{C}$ and
$Lu^{-1}\stackrel{{\scriptstyle\smash{\text{\tiny def}}}}{{=}}\\{w\in
A^{*}\mid wu\in L\\}\in\mathcal{C}$. A _prevariety_ is a Boolean algebra
closed under quotients and containing only _regular languages_. Regular
languages are those which can be equivalently defined by finite automata,
finite monoids or monadic second-order logic. We work with the definition by
monoids, which we now recall.

Monoids. A _monoid_ is a set $M$ endowed with an associative multiplication
$(s,t)\mapsto st$ having an identity element $1_{M}$ (_i.e._ , such that
${1_{M}}s=s{1_{M}}=s$ for every $s\in M$). An _idempotent_ of a monoid $M$ is
an element $e\in M$ such that $ee=e$. We write $E(M)\subseteq M$ for the set
of all idempotents in $M$. It is folklore that for every _finite_ monoid $M$,
there exists a natural number $\omega(M)$ (denoted by $\omega$ when $M$ is
understood) such that for every $s\in M$, the element $s^{\omega}$ is an
idempotent. Finally, we shall use the following Green relations [10] defined
on monoids. Given a monoid $M$ and $s,t\in M$, we write:

$\begin{array}[]{ll@{\ }l}s\leqslant_{\mathscr{J}}t&\text{when}&\text{there
exist $x,y\in M$ such that $s=xty$},\\\
s\leqslant_{\mathscr{L}}t&\text{when}&\text{there exists $x\in M$ such that
$s=xt$},\\\ s\leqslant_{\mathscr{R}}t&\text{when}&\text{there exists $y\in M$
such that $s=ty$}.\\\ \end{array}$

Clearly, $\leqslant_{\mathscr{J}}$, $\leqslant_{\mathscr{L}}$ and
$\leqslant_{\mathscr{R}}$ are preorders (_i.e._ , they are reflexive and
transitive). We write $<_{\mathscr{J}}$, $<_{\mathscr{L}}$ and
$<_{\mathscr{R}}$ for their strict variants (for example, $s<_{\mathscr{J}}t$
when $s\leqslant_{\mathscr{J}}t$ but $t\not\leqslant_{\mathscr{J}}s$).
Finally, we write $\mathrel{\mathscr{J}}$, $\mathrel{\mathscr{L}}$ and
$\mathrel{\mathscr{R}}$ for the corresponding equivalence relations (for
example, $s\mathrel{\mathscr{J}}t$ when $s\leqslant_{\mathscr{J}}t$ and
$t\leqslant_{\mathscr{J}}s$). There are many technical results about Green
relations. We will just need the following easy and standard lemma, which
applies to _finite_ monoids (see _e.g._ , [17, 20]).

######  Lemma 2.1.

Let $M$ be a finite monoid and let $s,t\in M$. If $s\mathrel{\mathscr{J}}t$
and $s\leqslant_{\mathscr{R}}t$, then $s\mathrel{\mathscr{R}}t$.

Regular languages and syntactic morphisms. Since $A^{*}$ is a monoid whose
multiplication is concatenation (the identity element is $\varepsilon$), we
may consider monoid morphisms $\alpha:A^{*}\to M$ where $M$ is an arbitrary
monoid. That is, $\alpha:A^{*}\to M$ is a map satisfying
$\alpha(\varepsilon)=1_{M}$ and $\alpha(uv)=\alpha(u)\alpha(v)$ for all
$u,v\in A^{*}$. We say that a language $L\subseteq A^{*}$ is _recognized_ by
$\alpha$ when there exists a set $F\subseteq M$ such that $L=\alpha^{-1}(F)$.

It is well known that regular languages are exactly those recognized by a
morphism into a _finite_ monoid. Moreover, every language $L$ is recognized by
a canonical morphism, which we briefly recall. One can associate to $L$ an
equivalence $\equiv_{L}$ over $A^{*}$: the _syntactic congruence of $L$_.
Given $u,v\in A^{*}$, we let $u\equiv_{L}v$ if and only if $xuy\in
L\Leftrightarrow xvy\in L$ for every $x,y\in A^{*}$. One can check that
“$\equiv_{L}$” is indeed a congruence on $A^{*}$: it is an equivalence
compatible with word concatenation. Thus, the set of equivalence classes
$M_{L}={A^{*}}/{\equiv_{L}}$ is a monoid. It is called the _syntactic monoid
of $L$_. Finally, the map $\alpha_{L}:A^{*}\to M_{L}$ sending every word to
its equivalence class is a morphism recognizing $L$, called the _syntactic
morphism of $L$_. It is known that a language $L$ is regular if and only if
$M_{L}$ is finite (_i.e._ , $\equiv_{L}$ has finite index): this is the
Myhill-Nerode theorem. In this case, one can compute the syntactic morphism
$\alpha_{L}:A^{*}\to M_{L}$ from any representation of $L$ (such as an
automaton or a monoid morphism).

Decision problems. We consider two decision problems, both depending on an
arbitrary class $\mathcal{C}$. They serve as mathematical tools for analyzing
it, as obtaining an algorithm for one of these problems requires a solid
understanding of that class $\mathcal{C}$. The _$\mathcal{C}$ -membership
problem_ is the simplest: it takes as input a single regular language $L$ and
simply asks whether $L\in\mathcal{C}$. The second problem, _$\mathcal{C}$
-separation_, is more general. Given three languages $K,L_{1},L_{2}$, we say
that $K$ _separates_ $L_{1}$ from $L_{2}$ if $L_{1}\subseteq K$ and $L_{2}\cap
K=\emptyset$. Given a class $\mathcal{C}$, we say that $L_{1}$ is
_$\mathcal{C}$ -separable_ from $L_{2}$ if some language of $\mathcal{C}$
separates $L_{1}$ from $L_{2}$. The _$\mathcal{C}$ -separation problem_ takes
as input two regular languages $L_{1},L_{2}$ and asks whether $L_{1}$ is
$\mathcal{C}$-separable from $L_{2}$.

######  Remark 2.2.

The $\mathcal{C}$-separation problem generalizes $\mathcal{C}$-membership.
Indeed, a regular language belongs to $\mathcal{C}$ if and only if it is
$\mathcal{C}$-separable from its complement, which is regular.

##  3 Orbits

Instead of looking at single classes, we consider _operators_. These are
correspondences $\mathcal{C}\mapsto\textup{Op}(\mathcal{C})$ that take as
input a class $\mathcal{C}$ to build a new one $\textup{Op}(\mathcal{C})$. We
investigate three operators in Sections 4 to 6. For now, we present general
tools for handling such operators. Given a class $\mathcal{C}$ and a morphism
$\alpha:A^{*}\to M$, we define special subsets of $M$: the
$\mathcal{C}$-orbits for $\alpha$. This notion was introduced in [28]. We
shall use it to formulate _generic characterizations_ of the operators
$\mathcal{C}\mapsto\textup{Op}(\mathcal{C})$ that we consider: for each input
prevariety $\mathcal{C}$, the languages in $\textup{Op}(\mathcal{C})$ are
characterized by a property of the $\mathcal{C}$-orbits for their syntactic
morphisms.

$\mathcal{C}$-pairs. Consider a class $\mathcal{C}$ and a morphism
$\alpha:A^{*}\to M$. We say that a pair $(s,t)\in M^{2}$ is a _$\mathcal{C}$
-pair for $\alpha$_ if and only if $\alpha^{-1}(s)$ is _not_
$\mathcal{C}$-separable from $\alpha^{-1}(t)$. Note that if
$\mathcal{C}$-separation is decidable, then one can compute all
$\mathcal{C}$-pairs for an input morphism.

We turn to a useful technical result, which characterizes the
$\mathcal{C}$-pairs using morphisms. Consider _two_ morphisms $\alpha:A^{*}\to
M$ and $\eta:A^{*}\to N$. For every pair $(s,t)\in M^{2}$, we say that $(s,t)$
is an _$\eta$ -pair for $\alpha$_ when there exist $u,v\in A^{*}$ such that
$\eta(u)=\eta(v)$, $\alpha(u)=s$ and $\alpha(v)=t$. In addition, for each
class $\mathcal{C}$, we define the _$\mathcal{C}$ -morphisms_ as the
_surjective_ morphisms $\eta:A^{*}\to N$ into a finite monoid $N$ such that
all languages recognized by $\eta$ belong to $\mathcal{C}$. We have the
following elementary lemma, proved in [27, Lemma 5.11].

######  Lemma 3.1.

Let $\mathcal{C}$ be a prevariety and $\alpha:A^{*}\to M$ be a morphism. Then,

  1. 1.

For every $\mathcal{C}$-morphism $\eta:A^{*}\to N$, all $\mathcal{C}$-pairs
for $\alpha$ are also $\eta$-pairs for $\alpha$.

  2. 2.

There exists a $\mathcal{C}$-morphism $\eta:A^{*}\to N$ such that all
$\eta$-pairs for $\alpha$ are also $\mathcal{C}$-pairs for $\alpha$.

$\mathcal{C}$-orbits. Consider a class $\mathcal{C}$ and a morphism
$\alpha:A^{*}\to M$. For every _idempotent_ $e\in E(M)$, the _$\mathcal{C}$
-orbit of $e$ for $\alpha$_ is the set $M_{e}\subseteq M$ consisting of all
elements $ete\in M$ such that $(e,t)\in M^{2}$ is a $\mathcal{C}$-pair. If
$\mathcal{C}$ is a prevariety and $\alpha$ is surjective, it is proved in [28,
Lemma 5.5] that $M_{e}$ is a monoid in $M$: it is closed under multiplication
and $e\in M_{e}$ is its identity. On the other hand, $M_{e}$ is not a “ _sub_
monoid” of $M$ (this is because $1_{M}$ needs not belong to $M_{e}$).

######  Lemma 3.2.

Let $\mathcal{C}$ be a prevariety and $\alpha:A^{*}\to M$ be a surjective
morphism into a finite monoid. For all $e\in E(M)$, the $\mathcal{C}$-orbit of
$e$ for $\alpha$ is a monoid in $M$ whose identity is $e$.

As seen above, when $\mathcal{C}$ has decidable separation, one can compute
the $\mathcal{C}$-pairs associated with an input morphism. Hence, one can also
compute the $\mathcal{C}$-orbits in this case.

######  Lemma 3.3.

Let $\mathcal{C}$ be a class with decidable separation. Given as input a
morphism $\alpha:A^{*}\to M$ into a finite monoid and $e\in E(M)$, one can
compute the $\mathcal{C}$-orbit of $e$ for $\alpha$.

Finally, the following lemma connects $\mathcal{C}$-orbits with
$\mathcal{C}$-morphisms.

######  Lemma 3.4.

Let $\mathcal{C}$ be a prevariety and $\alpha:A^{*}\to M$ be a morphism.
Moreover, let $\eta:A^{*}\to N$ be a $\mathcal{C}$-morphism. For every $e\in
E(M)$, there exists $f\in E(N)$ such that the $\mathcal{C}$-orbit of $e$ for
$\alpha$ is contained in the set $\alpha(\eta^{-1}(f))$.

######  Proof 3.5.

Let $t_{1},\dots,t_{n}\in M$ be all elements of the set $\\{t\in
M\mid(e,t)\text{ is a $\mathcal{C}$-pair}\\}$. By definition, the
$\mathcal{C}$-orbit of $e$ for $\alpha$ is
$M_{e}=\\{et_{1}e,\dots,et_{n}e\\}$. Since $\eta$ is a $\mathcal{C}$-morphism,
Lemma 3.1 implies that $(e,t_{i})$ is an $\eta$-pair for all $i\leq n$. This
yields $x_{i},y_{i}\in A^{*}$ such that $\eta(x_{i})=\eta(y_{i})$,
$\alpha(x_{i})=e$ and $\alpha(y_{i})=t_{i}$. Let $p=\omega(N)$,
$w=(x_{1}\cdots x_{n})^{p}$ and $f=\eta(w)$. Note that $f$ is idempotent by
choice of $p$. We show that $et_{i}e\in\alpha(\eta^{-1}(f))$ for $i\leq n$. We
define $w_{i}=(x_{1}\cdots x_{n})^{p}x_{1}\cdots x_{i-1}y_{i}x_{i+1}\cdots
x_{n}(x_{1}\cdots x_{n})^{2p-1}$. By definition, we have
$\alpha(w_{i})=et_{i}e$. Now, since $\eta(x_{i})=\eta(y_{i})$, we get
$\eta(w_{i})=\eta(w)=f$. Hence, $et_{i}e\in\alpha(\eta^{-1}(f))$, as desired.

##  4 Generalized unary temporal logic

In this section, we define generalized unary temporal logic. We introduce an
_operator_ $\mathcal{C}\mapsto\textup{TL}(\mathcal{C})$ that associates a new
class of languages $\textup{TL}(\mathcal{C})$ with every input class
$\mathcal{C}$. We first recall its definition (taken from [27]), and we then
complete it with useful properties.

###  4.1 Definition

Syntax. We associate with any class $\mathcal{C}$ a set of temporal formulas
denoted by $\textup{TL}[\mathcal{C}]$ as follows. A $\textup{TL}[\mathcal{C}]$
formula is built from atomic formulas using Boolean connectives and temporal
operators. The atomic formulas are $\top$, $\bot$, $min$, $max$ and “$a$” for
every letter $a\in A$. All Boolean connectives are allowed: if $\psi_{1}$ and
$\psi_{2}$ are $\textup{TL}[\mathcal{C}]$ formulas, then so are
$(\psi_{1}\vee\psi_{2})$, $(\psi_{1}\wedge\psi_{2})$ and $(\neg\psi_{1})$. We
associate _two temporal modalities_ with every language $L\in\mathcal{C}$,
which we denote by $\textup{F}_{L}$ and $\textup{P}_{L}$: if $\psi$ is a
$\textup{TL}[\mathcal{C}]$ formula, then so are
$(\mbox{$\textup{F}_{L}\,\psi$})$ and $(\textup{P}_{L}\,\psi)$. For the sake
of improved readability, we omit parentheses when there is no ambiguity.

Semantics. Evaluating a $\textup{TL}[\mathcal{C}]$ formula $\varphi$ requires
a word $w\in A^{*}$ and a position $i\in\textup{{Pos}}(w)$. We define by
induction what it means for _$(w,i)$ to satisfy $\varphi$_, which one denotes
by $w,i\models\varphi$.

  * •

Atomic formulas: $w,i\models\top$ always holds, $w,i\models\bot$ never holds
and for every symbol $\ell\in A\cup\\{min,max\\}$, $w,i\models\ell$ holds when
$\ell=w[i]$.

  * •

Disjunction: $w,i\models\psi_{1}\vee\psi_{2}$ when $w,i\models\psi_{1}$ or
$w,i\models\psi_{2}$.

  * •

Conjunction: $w,i\models\psi_{1}\wedge\psi_{2}$ when $w,i\models\psi_{1}$ and
$w,i\models\psi_{2}$.

  * •

Negation: $w,i\models\neg\psi$ when $w,i\models\psi$ does not hold.

  * •

Finally: for $L\in\mathcal{C}$, we let
$w,i\models\mbox{$\textup{F}_{L}\,\psi$}$ when there exists
$j\in\textup{{Pos}}(w)$ such that $i<j$, $w(i,j)\in L$ and $w,j\models\psi$.

  * •

Previously: for $L\in\mathcal{C}$, we let $w,i\models\textup{P}_{L}\,\psi$
when there exists $j\in\textup{{Pos}}(w)$ such that $j<i$, $w(j,i)\in L$ and
$w,j\models\psi$.

When no distinguished position is specified, it is customary to evaluate
formulas at the  _leftmost_ unlabeled position. One could also consider the
symmetrical convention of evaluating formulas at the _rightmost_ unlabeled
position. The convention chosen does not matter: we end-up with the same class
of languages. However, we shall consider restrictions of
$\textup{TL}[\mathcal{C}]$ for which this choice _does_ matter. This is why we
introduce notations for both conventions. Given a formula
$\varphi\in\textup{TL}[\mathcal{C}]$ we let $L_{min}(\varphi)=\\{w\in
A^{*}\mid w,0\models\varphi\\}$ and $L_{max}(\varphi)=\\{w\in A^{*}\mid
w,|w|+1\models\varphi\\}$.

We are now ready to define the operator
$\mathcal{C}\mapsto\textup{TL}(\mathcal{C})$. Consider an arbitrary class
$\mathcal{C}$. We write $\textup{TL}(\mathcal{C})$ for the class consisting of
all languages $L_{min}(\varphi)$ where $\varphi\in\textup{TL}[\mathcal{C}]$.
Observe that by definition, $\textup{TL}(\mathcal{C})$ is a Boolean algebra.
Actually, the results of [27] imply that when $\mathcal{C}$ is a prevariety,
then so is $\textup{TL}(\mathcal{C})$ (we do not need this fact in the present
paper).

Classic unary temporal logic. Let $\textup{ST}=\\{\emptyset,A^{*}\\}$ and
$\textup{DD}=\\{\emptyset,\\{\varepsilon\\},A^{+},A^{*}\\}$. The modalities
$\textup{F}_{A^{*}}$ and $\textup{P}_{A^{*}}$ have the same semantics as the
modalities F and P of standard unary temporal logic— _e.g._ ,
$w,i\models\mbox{$\textup{F}\,\varphi$}$ when there exists
$j\in\textup{{Pos}}(w)$ such that $i<j$ and $w,j\models\varphi$. Similarly,
the modalities $\textup{F}_{\\{\varepsilon\\}}$ and
$\textup{P}_{\\{\varepsilon\\}}$ have the same semantics as the modalities X
(next) and Y (yesterday)— _e.g._ , $w,i\models{\textup{X}\,\varphi}$ when
$i+1\in\textup{{Pos}}(w)$ and $w,i+1\models\varphi$. Using these facts, one
can check that the classes $\textup{TL}(\textup{ST})$ and
$\textup{TL}(\textup{DD})$ correspond exactly to the two original standard
variants of unary temporal logic (see _e.g._ , [9]): we have
$\textup{TL}=\textup{TL}(\textup{ST})$ and
$\textup{TLX}=\textup{TL}(\textup{DD})$.

######  Remark 4.1 (Robustness of classes to which TL is applied).

Note that including $\emptyset$ in an input class does not bring any new
modality in unary temporal logic. Similarly, the classes
$\textup{TL}(\textup{DD})$ and $\textup{TL}(\textup{DD}\setminus\\{A^{+}\\})$
are identical. However, in order to use generic results such as those from
Section 3, we require the classes to which the operator
$\mathcal{C}\mapsto\textup{TL}(\mathcal{C})$ is applied to have robust
properties: they should be prevarieties (hence, they should be closed under
complement).

######  Remark 4.2 (Connection with $\textup{FO}^{2}$).

Etessami, Vardi and Wilke [9] have shown that the variant TL corresponds to
the class $\textup{FO}^{2}(<)$ (two-variable first-order logic equipped with
the linear order), and that TLX corresponds to $\textup{FO}^{2}(<,+1)$ (which
also allows the successor). In [27], these results are generalized to all
classes $\textup{TL}(\mathcal{C})$ where $\mathcal{C}$ is a _Boolean algebra_.
In this case, we can construct from $\mathcal{C}$ a set of predicates
$\mathbb{I}_{\mathcal{C}}$ such that
$\textup{TL}(\mathcal{C})=\textup{FO}^{2}(\mathbb{I}_{\mathcal{C}})$.

######  Remark 4.3.

Another important input is the class and of alphabet testable languages. It
consists of all Boolean combinations of languages $A^{*}aA^{*}$, where $a\in
A$ is a letter. The class $\textup{TL}(\and)$ has been studied by Krebs,
Lodaya, Pandya and Straubing [13, 14, 15], who worked with the definition
based on two-variable first-order logic (_i.e._ , with the class
$\textup{FO}^{2}(\mathbb{I}_{\and})$, see Remark 4.2). In particular, they
proved that $\textup{TL}(\and)$ has decidable membership. We shall obtain this
result as a corollary of our generic characterization of the classes
$\textup{TL}(\mathcal{C})$.

###  4.2 Connection with unambiguous polynomial closure

It is shown in [27] that $\mathcal{C}\mapsto\textup{TL}(\mathcal{C})$ can be
expressed by other operators for very specific inputs: prevarieties of _group
languages_. If $\mathcal{G}$ is such a class, then $\textup{TL}(\mathcal{G})$
coincides with $\textup{UPol}(\textup{BPol}(\mathcal{G}))$, a class built on
top of $\mathcal{G}$ with the two standard operators UPol and BPol. We do not
use this result here, since we are tackling _arbitrary_ input prevarieties,
and in general, $\textup{UPol}(\textup{BPol}(\mathcal{C}))$ is _strictly_
included in $\textup{TL}(\mathcal{C})$ (it follows from [15] that the
inclusion is strict for the class $\and$ of Remark 4.3). However, the
operators UPol and BPol remain key tools in the paper: we use two results of
[27] about them. Let us first briefly recall their definitions.

Given finitely many 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$. A single
language $L_{0}$ is a marked product (this is the case $n=0$). The _polynomial
closure_ of a class $\mathcal{C}$, denoted by $\textup{Pol}(\mathcal{C})$,
consists of all _finite_ _unions_ of marked products $L_{0}a_{1}L_{1}\cdots
a_{n}L_{n}$ such that $L_{0},\dots,L_{n}\in\mathcal{C}$. If $\mathcal{C}$ is a
prevariety, then $\textup{Pol}(\mathcal{C})$ is a lattice (this is due to Arfi
[1], see also [19, 23] for recent proofs). However,
$\textup{Pol}(\mathcal{C})$ need not be closed under complement. This is why
it is often combined with another operator: the Boolean closure of a class
$\mathcal{D}$, denoted by $\textup{Bool}(\mathcal{D})$, is the least Boolean
algebra containing $\mathcal{D}$. We write $\textup{BPol}(\mathcal{C})$ for
$\textup{Bool}(\textup{Pol}(\mathcal{C}))$. It is standard that if
$\mathcal{C}$ is a prevariety, then so is $\textup{BPol}(\mathcal{C})$ (see
[23] for example). Finally, UPol is the _unambiguous_ restriction of Pol. A
marked product $L_{0}a_{1}L_{1}\cdots a_{n}L_{n}$ is _unambiguous_ when every
word $w\in L_{0}a_{1}L_{1}\cdots a_{n}L_{n}$ has a _unique_ decomposition
$w=w_{0}a_{1}w_{1}\cdots a_{n}w_{n}$ where $w_{i}\in L_{i}$ for $0\leq i\leq
n$. The _unambiguous polynomial closure_ of a class $\mathcal{C}$, written
$\textup{UPol}(\mathcal{C})$, consists of all _finite disjoint unions_ of
_unambiguous marked products_ $L_{0}a_{1}L_{1}\cdots a_{n}L_{n}$ such that
$L_{0},\dots,L_{n}\in\mathcal{C}$ (by “disjoint” we mean that the languages in
the union must be pairwise disjoint). While this is not apparent on the
definition, it is known [27] that if the input class $\mathcal{C}$ is a
prevariety, then so is $\textup{UPol}(\mathcal{C})$. Thus, UPol preserves
closure under complement.

In the paper, we are interested in the “combined” operator
$\mathcal{C}\mapsto\textup{UPol}(\textup{BPol}(\mathcal{C}))$. Indeed, it is
connected to the classes $\textup{TL}(\mathcal{C})$ by the following
proposition proved in [27, Proposition 9.12].

######  Proposition 4.4.

For every prevariety $\mathcal{C}$, we have
$\textup{UPol}(\textup{BPol}(\mathcal{C}))\subseteq\textup{TL}(\mathcal{C})$.

Although the inclusion of Proposition 4.4 is _strict_ in general, it is
essential for proving that _particular_ languages belong to
$\textup{TL}(\mathcal{C})$. Indeed, we will combine it with the next result
[27, Theorem 6.7] to prove that languages belong to
$\textup{UPol}(\textup{BPol}(\mathcal{C}))$—and therefore to
$\textup{TL}(\mathcal{C})$.

######  Theorem 4.5.

Let $\mathcal{C}$ be a prevariety, $L\subseteq A^{*}$ be a regular language
and $\alpha:A^{*}\to M$ be its syntactic morphism. Then,
$L\in\textup{UPol}(\textup{BPol}(\mathcal{C}))$ if and only if $\alpha$
satisfies the following property:

$(esete)^{\omega+1}=(esete)^{\omega}ete(esete)^{\omega}\quad\text{for every
$\mathcal{C}$-pair $(e,s)\in M^{2}$ and every $t\in M$}.$ (1)

##  5 Algebraic characterization of $\textup{TL}(\mathcal{C})$

We present a generic characterization of $\textup{TL}(\mathcal{C})$ when
$\mathcal{C}$ is a prevariety. It elegantly generalizes the characterizations
of $\textup{TL}=\textup{FO}^{2}(<)$ and $\textup{TLX}=\textup{FO}^{2}(<,+1)$
by Thérien and Wilke [36] and that of
$\textup{TL}(\and)=\textup{FO}^{2}(\mathbb{I}_{\and})$ by Krebs, Lodaya,
Pandya and Straubing [13, 14, 15].

###  5.1 Statement

The characterization is based on the well-known variety of finite monoids DA
(see [35] for a survey on this class). A finite monoid $M$ belongs to DA if it
satisfies the following equation:

$(st)^{\omega}=(st)^{\omega}t(st)^{\omega}\quad\text{for every $s,t\in M$}.$
(2)

Thérien and Wilke [36] showed that a regular language belongs to TL if and
only if its syntactic monoid is in DA (strictly speaking, they considered two-
variable first-order logic, the equality $\textup{FO}^{2}(<)=\textup{TL}$ is
due to Etessami, Vardi and Wilke [9]). We extend this result in the following
generic characterization of $\textup{TL}(\mathcal{C})$, based on
$\mathcal{C}$-orbits introduced in Section 3.

######  Theorem 5.1.

Let $\mathcal{C}$ be a prevariety, $L\subseteq A^{*}$ be a regular language
and $\alpha:A^{*}\to M$ be its syntactic morphism. The two following
properties are equivalent:

  1. 1.

$L\in\textup{TL}(\mathcal{C})$.

  2. 2.

For every idempotent $e\in E(M)$, the $\mathcal{C}$-orbit of $e$ for $\alpha$
belongs to DA.

Given as input a regular language $L\subseteq A^{*}$, one can compute its
syntactic morphism $\alpha:A^{*}\to M$. In view of Theorem 5.1,
$L\in\textup{TL}(\mathcal{C})$ if and only if for every $e\in E(M)$, the
$\mathcal{C}$-orbit of $e$ for $\alpha$ belongs to DA. The latter condition
can be decided by checking all $\mathcal{C}$-orbits, provided that we are able
to compute them. By Lemma 3.3, this is possible when $\mathcal{C}$-separation
is decidable. Altogether, we obtain the following corollary of Theorem 5.1.

######  Corollary 5.2.

If a prevariety $\mathcal{C}$ has decidable separation,
$\textup{TL}(\mathcal{C})$ has decidable membership.

######  Remark 5.3.

Let $L\subseteq A^{*}$ be a regular language and $\alpha:A^{*}\to M$ be its
syntactic morphism. The fact that the $\mathcal{C}$-orbit of $e\in E(M)$ for
$\alpha$ belongs to DA means that we have,

$(esete)^{\omega}=(esete)^{\omega}ete(esete)^{\omega}\quad\text{for all
$s,t\in M$ such that $(e,s)$ and $(e,t)$ are $\mathcal{C}$-pairs.}$ (3)

One can check that (3) follows from (1), which characterizes
$\textup{UPol}(\textup{BPol}(\mathcal{C}))$ (this is consistent with
Proposition 4.4 asserting that
$\textup{UPol}(\textup{BPol}(\mathcal{C}))\subseteq\textup{TL}(\mathcal{C})$).
Indeed, choosing $t=s$ in (1) shows that the $\mathcal{C}$-orbit of $e$ is
aperiodic, _i.e._ , $(ese)^{{\omega+1}}=(ese)^{\omega}$ if $(e,s)$ is a
$\mathcal{C}$-pair. However, note that the element $t$ is “free” in (1),
whereas it must be part of a $\mathcal{C}$-pair $(e,t)$ in (3).

Before proving Theorem 5.1, we first explain why it generalizes the original
characterizations of the classes TL, TLX and $\textup{TL}(\and)$, as mentioned
at the beginning of the section.

###  5.2 Application to historical classes

We first deduce the original characterizations of the classes
$\textup{TL}=\textup{TL}(\textup{ST})$ and
$\textup{TLX}=\textup{TL}(\textup{DD})$ by Thérien and Wilke [36] as simple
corollaries of Theorem 5.1. We start with the former.

######  Theorem 5.4 (Thérien and Wilke [36]).

Let $L\subseteq A^{*}$ be a regular language and let $M$ be its syntactic
monoid. The two following properties are equivalent:

  1. 1.

$L$ belongs to TL.

  2. 2.

$M$ belongs to DA.

######  Proof 5.5.

Let $\alpha:A^{*}\to M$ be the syntactic morphism of $L$. Since
$\textup{TL}=\textup{TL}(\textup{ST})$, Theorem 5.1 implies that
$L\in\textup{TL}$ if and only if every ST-orbit for $\alpha$ belongs to DA.
Since $\textup{ST}=\\{\emptyset,A^{*}\\}$, every pair $(e,s)\in E(M)\times M$
is a $\mathcal{C}$-pair, so that the ST-orbit of $e\in E(M)$ for $\alpha$ is
$eMe$. In particular the ST-orbit of $1_{M}$ is the whole monoid $M$. Hence,
every ST-orbit for $\alpha$ belongs to DA if and only if $M$ belongs to DA,
which completes the proof.

We turn to the characterization of $\textup{TLX}=\textup{TL}(\textup{DD})$,
also due to Thérien and Wilke [36]. In order to state it, we need an
additional definition. Consider a regular language $L$ and let
$\alpha:A^{*}\to M$ be its syntactic morphism. The _syntactic semigroup of
$L$_ is the set $S=\alpha(A^{+})$. Note that for every idempotent $e\in E(S)$,
the set $eSe$ is a monoid whose neutral element is $e$.

######  Theorem 5.6 (Thérien and Wilke [36]).

Let $L\subseteq A^{*}$ be a regular language and $S$ be its syntactic
semigroup. The two following properties are equivalent:

  1. 1.

$L$ belongs to TLX.

  2. 2.

For every $e\in E(S)$, the monoid $eSe$ belongs to DA.

######  Proof 5.7.

Let $\alpha:A^{*}\to M$ be the syntactic morphism of $L$. For $e\in E(M)$, let
$M_{e}\subseteq M$ be the DD-orbit of $e$ for $\alpha$. Since
$\textup{DD}=\\{\emptyset,\\{\varepsilon\\},A^{+},A^{*}\\}$, for $(e,s)\in
E(S)\times S$, the language $\alpha^{-1}(e)$ is not DD-separable from
$\alpha^{-1}(s)$. Hence, $(e,s)$ is a $\mathcal{C}$-pair, so that $M_{e}=eSe$
for all $e\in E(S)$. Moreover, if $1_{M}\not\in E(S)$ (which means that
$\alpha^{-1}(1_{M})=\\{\varepsilon\\}$), then we have $M_{1_{M}}=\\{1_{M}\\}$
(which clearly belongs to DA). Hence, every DD-orbit for $\alpha$ belongs to
DA if and only if $eSe\in\textup{DA}$ for every $e\in E(S)$. In view of
Theorem 5.1, this implies Theorem 5.6.

Finally, we consider the class $\textup{TL}(\and)$, defined and characterized
by Krebs, Lodaya, Pandya and Straubing [13, 14, 15]. Let us first present
their characterization. It is based on a variety of finite monoids called
$\textup{M}_{e}\textup{DA}$. Let $M$ be a finite monoid. For each $e\in E(M)$,
let $N_{e}\subseteq M$ be the submonoid of $M$ generated by the set $\\{s\in
M\mid e\leqslant_{\mathscr{J}}s\\}$. We say that $M$ belongs to
$\textup{M}_{e}\textup{DA}$ if and only if for every idempotent $e\in E(M)$,
the monoid of $eN_{e}e$ belongs to DA.

######  Theorem 5.8 (Krebs, Lodaya, Pandya and Straubing [15]).

Let $L\subseteq A^{*}$ be a regular language and $M$ be its syntactic monoid.
The two following properties are equivalent:

  1. 1.

$L\in\textup{TL}(\and)$.

  2. 2.

$M$ belongs to $\textup{M}_{e}\textup{DA}$.

######  Proof 5.9.

For $w\in A^{*}$, let $\mathit{alph}(w)\subseteq A$ be the set of letters
occurring in $w$ (_i.e._ , the least set $B\subseteq A$ such that $w\in
B^{*}$). For $e\in E(M)$, let $M_{e}$ be the and -orbit of $e$ for $\alpha$.
We prove that $M_{e}=eN_{e}e$ for every $e\in E(M)$. It will follows that $M$
belongs to $\textup{M}_{e}\textup{DA}$ if and only if every and -orbit for
$\alpha$ belongs to DA. In view of Theorem 5.1 this implies Theorem 5.8.

We first consider $s^{\prime}\in eN_{e}e$ and prove that $s^{\prime}\in
M_{e}$. We have $s\in N_{e}$ such that $s^{\prime}=ese$. By definition,
$s=s_{1}\cdots s_{n}$ where $e\leqslant_{\mathscr{J}}s_{i}$ for every $i\leq
n$. If $n=0$, then $s=1_{M}$ and $ese=e\in M_{e}$. Assume now that we have
$n\geq 1$. Since $e\leqslant_{\mathscr{J}}s_{i}$, we have $q_{i},r_{i}\in M$
such that $e=q_{i}s_{i}r_{i}$ for every $i\leq n$. Hence, since $e\in E(M)$,
we have $e=q_{1}s_{1}r_{1}\cdots q_{n}s_{n}r_{n}$. For every $i\leq n$, let
$x_{i}\in\alpha^{-1}(q_{i})$, $y_{i}\in\alpha^{-1}(r_{i})$ and
$u_{i}\in\alpha^{-1}(s_{i})$. Finally, let $w=x_{1}u_{1}y_{1}\cdots
x_{n}u_{n}y_{n}$ and $w^{\prime}=wu_{1}\cdots u_{n}w$. By definition, we have
$e=\alpha(w)$ and $ese=\alpha(w^{\prime})$. Moreover, it is clear that
$\mathit{alph}(w)=\mathit{alph}(w^{\prime})$. By definition of and , it
follows that $\alpha^{-1}(e)$ is not and -separable from $\alpha^{-1}(ese)$.
Thus, $(e,ese)$ is an and -pair for $\alpha$, which yields $s^{\prime}=ese\in
M_{e}$, as desired.

Conversely, let $s^{\prime}\in M_{e}$. By definition, there exists an and
-pair $(e,s)\in M^{2}$ with $e\in E(M)$ such that $s^{\prime}=ese$. Therefore,
by definition of and , there exist $u,v\in A^{*}$ such that
$\mathit{alph}(u)=\mathit{alph}(v)$, $\alpha(u)=e$ and $\alpha(v)=s$. Let
$a_{1}\dots,a_{n}\in A$ be the letters such that $v=a_{1}\cdots a_{n}$. Since
$\mathit{alph}(u)=\mathit{alph}(v)$, it is immediate that for each $i\leq n$,
there are $x_{i},y_{i}\in A^{*}$ such that $u=x_{i}a_{i}y_{i}$. Hence
$e=\alpha(u)\leqslant_{\mathscr{J}}\alpha(a_{i})$ and we conclude that
$s=\alpha(a_{1}\cdots a_{n})\in N_{e}$. Consequently, $s^{\prime}=ese\in
eN_{e}e$, as desired.

###  5.3 Proof of Theorem 5.1

We fix a prevariety $\mathcal{C}$, a regular language $L\subseteq A^{*}$ and
its syntactic morphism $\alpha:A^{*}\to M$ for the proof. We prove that
$L\in\textup{TL}(\mathcal{C})$ if and only if all $\mathcal{C}$-orbits for
$\alpha$ belong to DA. We start with the left-to-right implication.

From $\textup{TL}(\mathcal{C})$ to DA. This direction follows from results of
[27]. To use them, we need some preliminary terminology. We introduce
equivalence relations connected to the class $\textup{TL}(\mathcal{C})$ when
$\mathcal{C}$ is a prevariety. Given a morphism $\eta:A^{*}\to N$ into a
finite monoid $N$, denote by $\mathcal{C}_{\eta}$ be the class of all
languages recognized by $\eta$. The following fact is easy (see [27, Fact
9.3]).

######  Fact 1.

Let $\mathcal{C}$ be a prevariety. For every $\textup{TL}[\mathcal{C}]$
formula $\varphi$, there exists a $\mathcal{C}$-morphism $\eta:A^{*}\to N$
such that $\varphi$ is a $\textup{TL}[\mathcal{C}_{\eta}]$ formula.

We use the standard notion of rank of a $\textup{TL}[\mathcal{C}_{\eta}]$
formula: the _rank_ of $\varphi$ is defined as the length of the longest
sequence of nested temporal operators within its parse tree. Formally:

  * •

Any atomic formula has rank $0$.

  * •

The rank of $\neg\varphi$ is the same as the rank of $\varphi$.

  * •

The rank of $\varphi\vee\psi$ and $\varphi\wedge\psi$ is the maximum between
the ranks of $\varphi$ and $\psi$.

  * •

For every language $L\subseteq A^{*}$, the rank of $\textup{F}_{L}\,\varphi$
and $\textup{P}_{L}\,\varphi$ is the rank of $\varphi$ plus $1$.

Two $\textup{TL}[\mathcal{C}_{\eta}]$ formulas $\varphi$ and $\psi$ are
_equivalent_ if they have the same semantics. That is, for every $w\in A^{*}$
and every position $i\in\textup{{Pos}}(w)$, we have
$w,i\models\varphi\Leftrightarrow w,i\models\psi$. The following key lemma is
immediate from a simple induction on the rank of TL formulas.

######  Lemma 5.10.

Let $\eta:A^{*}\to N$ be a morphism into a finite monoid and let $k\in{\rm
Nature}$. There are only finitely many non-equivalent
$\textup{TL}[\mathcal{C}_{\eta}]$ formulas of rank at most $k$.

We now define equivalence relations. Let $\eta:A^{*}\to N$ be a morphism into
a finite monoid and let $k\in{\rm Nature}$. Given $w,w^{\prime}\in A^{*}$,
$i\in\textup{{Pos}}(w)$ and $i^{\prime}\in\textup{{Pos}}(w^{\prime})$, we
write, $w,i\cong_{\eta,k}w^{\prime},i^{\prime}$ when:

$\text{For every $\textup{TL}[\mathcal{C}_{\eta}]$ formula $\varphi$ of rank
at most $k$,}\quad w,i\models\varphi\Longleftrightarrow
w^{\prime},i^{\prime}\models\varphi.$

It is straightforward that $\cong_{\eta,k}$ is an equivalence relation.
Moreover, it is immediate from the definition and Lemma 5.10, that
$\cong_{\eta,k}$ has finite index. We lift each relation $\cong_{\eta,k}$ to
$A^{*}$ (abusing terminology, we also denote by $\cong_{\eta,k}$ the new
relation): given $w,w^{\prime}\in A^{*}$, we write $w\cong_{\eta,k}w^{\prime}$
when $w,0\cong_{\eta,k}w^{\prime},0$. Clearly, $\cong_{\eta,k}$ is an
equivalence relation of finite index over $A^{*}$. Moreover, we have the
following connection between $\textup{TL}(\mathcal{C})$ and the relations
$\cong_{\eta,k}$.

######  Lemma 5.11.

Let $\mathcal{C}$ be a prevariety and $L\subseteq A^{*}$. If
$L\in\textup{TL}(\mathcal{C})$, then there exists a $\mathcal{C}$-morphism
$\eta:A^{*}\to N$ and $k\in{\rm Nature}$ such that $L$ is a union of
$\cong_{\eta,k}$-classes.

######  Proof 5.12.

Let $L\in\textup{TL}(\mathcal{C})$. There exists a $\textup{TL}[\mathcal{C}]$
formula $\varphi$ such that $w\in L\Leftrightarrow w,0\models\varphi$ for all
$w\in A^{*}$. By Fact 1, there exists a $\mathcal{C}$-morphism $\eta:A^{*}\to
N$ such that $\varphi$ is a $\textup{TL}[\mathcal{C}_{\eta}]$ formula. Let
$k\in{\rm Nature}$ be the rank of $\varphi$. We prove that $L$ is a union of
$\cong_{\eta,k}$-classes. Given $w,w^{\prime}\in A^{*}$ such that
$w\cong_{\eta,k}w^{\prime}$, we have to prove that $w\in L\Leftrightarrow
w^{\prime}\in L$. By symmetry, we only prove the left to right implication.
Thus, we assume that $w\in L$. By definition of $\varphi$, it follows that
$w,0\models\varphi$. Moreover, since $w\cong_{\eta,k}w^{\prime}$ (_i.e._ ,
$w,0\cong_{\eta,k}w^{\prime},0$) and $\varphi$ is a
$\textup{TL}[\mathcal{C}_{\eta}]$ formula of rank $k$, we have
$w^{\prime},0\models\varphi$ by definition of $\cong_{\eta,k}$. Hence,
$w^{\prime}\in L$ by definition of $\varphi$, as desired.

In addition to the link stated in Lemma 5.11 between
$\textup{TL}(\mathcal{C})$ and the equivalence relations $\cong_{\eta,k}$, we
use a property of $\cong_{\eta,k}$ that follows from [27, Lemma 9.6 and
Proposition 9.7].

######  Proposition 5.13.

Consider a morphism $\eta:A^{*}\to N$ into a finite monoid, let $f\in E(N)$ be
an idempotent, let $u,v,z\in\eta^{-1}(f)$ and let $x,y\in A^{*}$. For every
$k\in{\rm Nature}$, we have:

$x(z^{k}uz^{2k}vz^{k})^{k}(z^{k}uz^{2k}vz^{k})^{k}y\cong_{\eta,k}x(z^{k}uz^{2k}vz^{k})^{k}z^{k}vz^{k}(z^{k}uz^{2k}vz^{k})^{k}y.$

We are ready to conclude this direction of the proof: assuming that
$L\in\textup{TL}(\mathcal{C})$, we show that all $\mathcal{C}$-orbits for its
syntactic monoid belong to DA. Let $e\in E(M)$ and $M_{e}$ be its
$\mathcal{C}$-orbit. Proving that $M_{e}\in\textup{DA}$ amounts to proving
that any elements $s,t\in M_{e}$ satisfy (2). Fix $e,s,t\in E(M)\times
M_{e}\times M_{e}$. Lemma 5.11 yields a $\mathcal{C}$-morphism $\eta:A^{*}\to
N$ and $k\in{\rm Nature}$ such that $L$ is a union of
$\cong_{\eta,k}$-classes. Since $\eta$ is a $\mathcal{C}$-morphism, Lemma 3.4
yields $f\in E(N)$ such that $M_{e}\subseteq\alpha(\eta^{-1}(f))$. Since
$e,s,t\in M_{e}$, we get $z,u,v\in A^{*}$ such that $z,u,v\in\eta^{-1}(f)$,
$\alpha(z)=e$, $\alpha(u)=s$ and $\alpha(v)=t$. Let $x,y\in A^{*}$ be two
arbitrary words. By Proposition 5.13, we obtain,

$x(z^{k}uz^{2k}vz^{k})^{k}(z^{k}uz^{2k}vz^{k})^{k}y\cong_{\eta,k}x(z^{k}uz^{2k}vz^{k})^{k}z^{k}vz^{k}(z^{k}uz^{2k}vz^{k})^{k}y.$

Since $L$ is a union of $\cong_{\eta,k}$-classes, the words
$(z^{k}uz^{k}vz^{k})^{2k}$ and
$(z^{k}uz^{k}vz^{k})^{k}z^{k}vz^{k}(z^{k}uz^{k}vz^{k})^{k}$ are equivalent for
the syntactic congruence of $L$, so they have the same image under its
syntactic morphism $\alpha$. Since $e\in E(M)$, this yields
$(esete)^{2k}=(esete)^{k}ete(esete)^{k}$. Hence, $(st)^{2k}=(st)^{k}t(st)^{k}$
since $e,s,t\in M_{e}$ and $e$ is neutral in $M_{e}$ by Lemma 3.2. It now
suffices to multiply by enough copies of $st$ on both sides to get
$(st)^{\omega}=(st)^{\omega}t(st)^{\omega}$. Therefore, (2) holds.

From DA to $\textup{TL}(\mathcal{C})$. Assuming that every $\mathcal{C}$-orbit
for the syntactic morphism $\alpha:A^{*}\to M$ of $L$ belongs to DA, we have
to show that $L\in\textup{TL}(\mathcal{C})$, _i.e._ , to build a
$\textup{TL}[\mathcal{C}]$ formula defining $L$. Let us start by giving a
high-level overview of the proof for this direction.

Since $\textup{TL}(\mathcal{C})$ is closed under union, it suffices to prove
that for all $s\in M$, the language $\alpha^{-1}(s)$ is in
$\textup{TL}(\mathcal{C})$. We achieve this by inductively constructing a
$\textup{TL}[\mathcal{C}]$ formula defining $\alpha^{-1}(s)$. According to
Lemma 3.1, there exists a $\mathcal{C}$-morphism $\eta:A^{*}\to N$ such that
the $\mathcal{C}$-pairs for $\alpha$ are exactly the $\eta$-pairs for
$\alpha$. We use $\eta$ to leverage the assumption that all
$\mathcal{C}$-orbits for $\alpha$ belong to DA. More precisely, $\eta$
recognizes all the basic languages in $\mathcal{C}$ that we shall use in our
$\textup{TL}[\mathcal{C}]$ formulas. The induction proceeds as follows: using
$\eta$, we define a sequence of languages $K_{0}\supseteq
K_{1}\supseteq\cdots\supseteq K_{|N|}$ and show by induction on $|N|-\ell$
that $K_{\ell}\cap\alpha^{-1}(s)$ can be defined by a
$\textup{TL}[\mathcal{C}]$ formula for each $\ell\leq|N|$. The induction basis
is the case $\ell=|N|$, which is simple because $K_{|N|}$ is a finite
language. Furthermore, the case $\ell=0$ gives the desired result since
$K_{0}$ contains all words. The induction step consists in building a
$\textup{TL}[\mathcal{C}]$ formula describing $K_{\ell}\cap\alpha^{-1}(s)$
from several $\textup{TL}[\mathcal{C}]$ formulas that describe the languages
$K_{\ell+1}\cap\alpha^{-1}(t)$ for all $t\in M$. However, the actual argument
is slightly more involved. Indeed, in order to perform the induction step, we
must abstract each word in $K_{\ell}\cap\alpha^{-1}(s)$ by considering a
specific decomposition of this word and viewing each infix as a new letter. We
then argue that the resulting word belongs to $K_{\ell+1}\cap\alpha^{-1}(s)$,
which allows us to apply induction. Yet, for this process to work, the letter
that we use to abstract an infix must have the same images as this original
infix under both $\alpha$ and $\eta$. This is problematic, because such a
letter does not necessarily exist. We solve this issue by considering an
extended alphabet $B$, replacing $\alpha:A^{*}\to M$ and $\eta:A^{*}\to N$
with two new morphisms $\beta:B^{*}\to M$ and $\delta:B^{*}\to N$ that have
the required property. Of course, this involves some preliminary work: we must
reformulate both our objective (proving that all languages $\alpha^{-1}(s)$
can be defined in $\textup{TL}(\mathcal{C})$) and our hypothesis (that every
$\mathcal{C}$-orbit for $\alpha$ belongs to DA) on the new morphisms $\beta$
and $\eta$.

We now start the proof by first defining $\beta$ and $\delta$. Recall that
$\eta:A^{*}\to N$ is the $\mathcal{C}$-morphism provided by Lemma 3.1: it is
such that the $\mathcal{C}$-pairs for $\alpha$ are exactly the $\eta$-pairs
for $\alpha$. We fix $\eta$ for the entire proof. We define an auxiliary
alphabet $B$. Let $P\subseteq M\times N$ be the set of all pairs
$(\alpha(w),\eta(w))\in M\times N$ where $w\in A^{+}$ is a nonempty word. For
each pair $(s,r)\in P$, we create a fresh letter $b_{s,r}\not\in A$ and we
define $B=\\{b_{s,r}\mid(s,r)\in P\\}$.

Let $\beta:B^{*}\to M$ and $\delta:B^{*}\to N$ be the morphisms defined by
$\beta(b_{s,r})=s$ and $\delta(b_{s,r})=r$ for $(s,r)\in P$. By definition, we
have $(\beta(w),\delta(w))\in P$ for all $w\in B^{+}$. Let
$\mathcal{C}_{\delta}$ be the class of all languages over $B$ recognized by
$\delta$. One can check that $\mathcal{C}_{\delta}$ is a prevariety. We now
reduce membership of inverse images under $\alpha$ to
$\textup{TL}(\mathcal{C})$ to that of inverse images under $\beta$ to
$\textup{TL}(\mathcal{C}_{\delta})$.

######  Lemma 5.14.

For every $F\subseteq M$, if
$\beta^{-1}(F)\in\textup{TL}(\mathcal{C}_{\delta})$, then
$\alpha^{-1}(F)\in\textup{TL}(\mathcal{C})$.

######  Proof 5.15.

We first define a morphism $\gamma:A^{*}\to B^{*}$. Consider a letter $a\in
A$. By definition, $(\alpha(a),\eta(a))\in P$. Hence, we may define
$\gamma(a)=b_{\alpha(a),\eta(a)}\in B$. By definition, we have
$\alpha(w)=\beta(\gamma(w))\in M$ and $\eta(w)=\delta(\gamma(w))$ for every
$w\in A^{*}$. It follows that for every $F\subseteq M$, we have
$\alpha^{-1}(F)=\gamma^{-1}(\beta^{-1}(F))\subseteq A^{*}$. Consequently, it
now suffices to prove that for every $K\subseteq B^{*}$ such that
$K\in\textup{TL}(\mathcal{C}_{\delta})$, we have
$\gamma^{-1}(K)\in\textup{TL}(\mathcal{C})$. We fix $K$ for the proof. Since
$K\in\textup{TL}(\mathcal{C}_{\delta})$, it is defined by a formula
$\psi\in\textup{TL}[\mathcal{C}_{\delta}]$. We apply two kinds of
modifications to $\psi$ in order to build a new formula
$\psi^{\prime}\in\textup{TL}[\mathcal{C}]$ defining $\gamma^{-1}(K)$:

  1. 1.

We replace every atomic subformula “$b$” for $b\in B$ by the
$\textup{TL}[\mathcal{C}]$-formula $\bigvee_{\\{a\in A\mid\gamma(a)=b\\}}a$.

  2. 2.

For every temporal modality $\textup{F}_{H}$ (resp. $\textup{P}_{H}$)
occurring in $\psi$, we have $H\in\mathcal{C}_{\delta}$ by hypothesis. Hence,
$H$ is recognized by $\delta$ and there exists $G\subseteq N$ such that
$H=\delta^{-1}(G)$. Note that $\eta^{-1}(G)\in\mathcal{C}$ since $\eta$ is a
$\mathcal{C}$-morphism. We replace the temporal modality $\textup{F}_{H}$
(resp. $\textup{P}_{H}$) by $\textup{F}_{\eta^{-1}(G)}$ (resp.
$\textup{P}_{\eta^{-1}(G)}$).

By definition the resulting formula $\psi^{\prime}$ belongs to
$\textup{TL}[\mathcal{C}]$ and one can verify that for every $w\in A^{*}$, we
have $w,0\models\psi^{\prime}\Leftrightarrow\gamma(w),0\models\psi$. Since
$L_{min}(\psi)=K$, we get $L_{min}(\psi^{\prime})=\gamma^{-1}(K)$, which
implies that $K\in\textup{TL}(\mathcal{C})$. This completes the proof.

In view of Lemma 5.14, it suffices to prove that any language recognized by
$\beta$ belongs to $\textup{TL}(\mathcal{C}_{\delta})$. Since $L$ is
recognized by $\alpha$, this will imply $L\in\textup{TL}(\mathcal{C})$, which
is our goal. In the next lemma, we reformulate on $\beta$ and $\delta$ the
assumption that every $\mathcal{C}$-orbit for $\alpha$ belongs to DA.

######  Lemma 5.16.

For every $e\in E(M)$ and every $s,t\in M$, if $(e,s)$ and $(e,t)$ are
$\delta$-pairs for $\beta$, then
$(esete)^{\omega}=(esete)^{\omega}ete(esete)^{\omega}$.

######  Proof 5.17.

By hypothesis, there exist $u,v,x,y\in B^{*}$ such that $\delta(u)=\delta(v)$,
$\delta(x)=\delta(y)$, $\beta(u)=\beta(x)=e$, $\beta(v)=s$ and $\beta(y)=t$.
The definitions of $\beta$ and $\delta$ imply that for any $w\in B^{*}$, there
exists $w^{\prime}\in A^{*}$ such that $\delta(w)=\eta(w^{\prime})$ and
$\beta(w)=\alpha(w^{\prime})$. Therefore, we obtain
$u^{\prime},v^{\prime},x^{\prime},y^{\prime}\in A^{*}$ such that
$\eta(u^{\prime})=\eta(v^{\prime})$, $\eta(x^{\prime})=\eta(y^{\prime})$,
$\alpha(u^{\prime})=\alpha(x^{\prime})=e$, $\alpha(v^{\prime})=s$ and
$\alpha(y^{\prime})=t$. Thus, $(e,s)\in M^{2}$ and $(e,t)\in M^{2}$ are
$\eta$-pairs for $\alpha$. By definition of $\eta$, it follows that they are
$\mathcal{C}$-pairs for $\alpha$. Hence, $ese$ and $ete$ both belong to the
$\mathcal{C}$-orbit of $e$ for $\alpha$. Since all $\mathcal{C}$-orbits for
$\alpha$ belong to DA by hypothesis, this gives
$(esete)^{\omega}=(esete)^{\omega}ete(esete)^{\omega}$.

We now use the Green relation $\mathrel{\mathscr{J}}$ over $N$ to associate a
number $d_{\mathrel{\mathscr{J}}}(r)\in{\rm Nature}$ with every element $r\in
N$. We let $d_{\mathrel{\mathscr{J}}}(r)$ be the maximal number $n\in{\rm
Nature}$ such that there exist $n$ elements $r_{1},\dots,r_{n}\in N$
satisfying $r<_{\mathscr{J}}r_{1}<_{\mathscr{J}}\cdots<_{\mathscr{J}}r_{n}$.
By definition, $0\leq d_{\mathrel{\mathscr{J}}}(r)\leq|N|-1$. In particular,
we have $d_{\mathrel{\mathscr{J}}}(r)=0$ if and only if $r$ is maximal for
$\leqslant_{\mathscr{J}}$ (_i.e._ , if and only if
$r\mathrel{\mathscr{J}}1_{N}$). Finally, given a word $w\in B^{*}$, we write
$d_{\mathrel{\mathscr{J}}}(w)\in{\rm Nature}$ for
$d_{\mathrel{\mathscr{J}}}(\delta(w))$. Observe that for all $x,y,z\in B^{*}$,
we have $d_{\mathrel{\mathscr{J}}}(y)\leq d_{\mathrel{\mathscr{J}}}(xyz)$ (as
$xyz\leqslant_{\mathscr{J}}y$), a fact that we shall use frequently.

In order to argue inductively, we define a family of languages
$K_{\ell}\subseteq B^{*}$ for $\ell\in{\rm Nature}$ as follows:

$K_{\ell}=\bigl{\\{}w\in B^{*}\mid\text{for all $k\leq\ell$ and $x,y,z\in
B^{*}$, if $w=xyz$ and $|y|=k$, then $d_{\mathrel{\mathscr{J}}}(y)\geq
k$}\bigr{\\}}.$

Note that $K_{0}=B^{*}$ as $d_{\mathrel{\mathscr{J}}}(y)\geq 0$ for all $y\in
B^{*}$. Also, if $\ell\geq|N|$, then $K_{\ell}$ is _finite_ (it contains words
of length at most $|N|-1$ as $d_{\mathrel{\mathscr{J}}}(y)<|N|$ for all $y\in
B^{*}$). We now have the next lemma.

######  Lemma 5.18.

Let $\ell\in{\rm Nature}$ and $w\in K_{\ell}$. Then
$d_{\mathrel{\mathscr{J}}}(w)\leq\ell$ if and only if for all $x,y,z\in B^{*}$
such that $w=xyz$ and $|y|\leq\ell+1$, we have
$d_{\mathrel{\mathscr{J}}}(y)\leq\ell$.

######  Proof 5.19.

The “only if” direction is immediate since $d_{\mathrel{\mathscr{J}}}(y)\leq
d_{\mathrel{\mathscr{J}}}(w)$ for every infix $y$ of $w$. Conversely, assume
that for all $x,y,z\in B^{*}$ such that $w=xyz$ and $|y|\leq\ell+1$, we have
$d_{\mathrel{\mathscr{J}}}(y)\leq\ell$. We prove that
$d_{\mathrel{\mathscr{J}}}(w)\leq\ell$. If $|w|\leq\ell+1$, this is immediate.
Assume now that $|w|>\ell+1$. We get $b_{1},\dots,b_{n}\in B$ and $v\in B^{*}$
such that $|v|=\ell+1$ and $w=vb_{1}\cdots b_{n}$. We use induction on $i$ to
prove that $\delta(v)\mathrel{\mathscr{J}}\delta(vb_{1}\cdots b_{i})$ for all
$i\leq n$. Since $d_{\mathrel{\mathscr{J}}}(v)\leq\ell$ by hypothesis, the
case $i=n$ yields $d_{\mathrel{\mathscr{J}}}(w)\leq\ell$. The case $i=0$ is
trivial: we have $\delta(v)\mathrel{\mathscr{J}}\delta(v)$. Assume now that
$i\geq 1$. By induction hypothesis, we know that
$\delta(v)\mathrel{\mathscr{J}}\delta(vb_{1}\cdots b_{i-1})$. Let $x,y\in
B^{*}$ such that $|y|=\ell$ and $xy=vb_{1}\cdots b_{i-1}$ (the words $x$ and
$y$ exist because $|v|=\ell+1$). Since $w\in K_{\ell}$, and $y$ is an infix of
$w$ such that $|y|=\ell$, we know that $d_{\mathrel{\mathscr{J}}}(y)\geq\ell$.
Moreover, $yb_{i}$ is an infix of $w$ such that $|yb_{i}|=\ell+1$, which
yields $d_{\mathrel{\mathscr{J}}}(yb_{i})\leq\ell$ by hypothesis. Since
$d_{\mathrel{\mathscr{J}}}(y)\leq d_{\mathrel{\mathscr{J}}}(yb_{i})$, we get
$d_{\mathrel{\mathscr{J}}}(yb_{i})=d_{\mathrel{\mathscr{J}}}(y)=\ell$, which
implies that $\delta(yb_{i})\mathrel{\mathscr{J}}\delta(y)$. Moreover, we have
$\delta(yb_{i})\leqslant_{\mathscr{R}}\delta(y)$. Thus, Lemma 2.1 yields
$\delta(yb_{i})\mathrel{\mathscr{R}}\delta(y)$. This implies that
$\delta(xyb_{i})\mathrel{\mathscr{R}}\delta(xy)$. Hence, $\delta(vb_{1}\cdots
b_{i})\mathrel{\mathscr{J}}\delta(vb_{1}\cdots
b_{i-1})\mathrel{\mathscr{J}}\delta(v)$. This completes the proof.

We now prove that for all $s\in M$ and $\ell\in{\rm Nature}$, we have
$K_{\ell}\cap\beta^{-1}(s)\in\textup{TL}(\mathcal{C}_{\delta})$. Our objective
(every language recognized by $\beta$ belongs to
$\textup{TL}(\mathcal{C}_{\delta})$) follows from the case $\ell=0$, since
$K_{0}=B^{*}$. The proof involves two steps. The first settles the case of
elements of $K_{\ell}\cap\beta^{-1}(s)$ whose image under $\delta$ has a
$d_{\mathrel{\mathscr{J}}}$ value at most $\ell$. We do not use induction for
this case, which relies on the inclusion
$\textup{UPol}(\textup{BPol}(\mathcal{C}_{\delta}))\subseteq\textup{TL}(\mathcal{C}_{\delta})$.
It is also the place where we use Lemma 5.16, _i.e._ , the hypothesis that all
$\mathcal{C}$-orbits for $\alpha$ are in DA.

######  Proposition 5.20.

Let $(\ell,s,r)\in{\rm Nature}\times M\times N\\!$. If
$d_{\mathrel{\mathscr{J}}}(r)\leq\ell$ then
$K_{\ell}\cap\beta^{-1}(s)\cap\delta^{-1}(r)\in\textup{TL}(\mathcal{C}_{\delta})$.

######  Proof 5.21.

We prove that
$K_{\ell}\cap\beta^{-1}(s)\cap\delta^{-1}(r)\in\textup{UPol}(\textup{BPol}(\mathcal{C}_{\delta}))$,
which, by Proposition 4.4, will give the desired result
$K_{\ell}\cap\beta^{-1}(s)\cap\delta^{-1}(r)\in\textup{TL}(\mathcal{C}_{\delta})$.
Let $\gamma:B^{*}\to Q$ be the syntactic morphism of
$K_{\ell}\cap\beta^{-1}(s)\cap\delta^{-1}(r)$. By Theorem 4.5, it suffices to
show that given $q_{1},q_{2}\in Q$ and $f\in E(Q)$ such that $(f,q_{1})\in
Q^{2}$ is a $\mathcal{C}_{\delta}$-pair for $\gamma$, the following equation
holds:

$(fq_{1}fq_{2}f)^{\omega+1}=(fq_{1}fq_{2}f)^{\omega}fq_{2}f(fq_{1}fq_{2}f)^{\omega}.$
(4)

Let $q_{1},q_{2},f\in Q$ be such elements. By definition of
$\mathcal{C}_{\delta}$, we know that $\delta$ is a
$\mathcal{C}_{\delta}$-morphism. Therefore, Lemma 3.1 implies that $(f,q_{1})$
is a $\delta$-pair for $\gamma$. We get $u^{\prime},v^{\prime}_{1}\in B^{*}$,
such that $\delta(u^{\prime})=\delta(v^{\prime}_{1})$, $\gamma(u^{\prime})=f$
and $\gamma(v^{\prime}_{1})=q_{1}$. Note that if $v^{\prime}_{1}=\varepsilon$,
then $q_{1}=1_{Q}$ and (4) holds since it is clear that
$(fq_{2}f)^{\omega+1}=(fq_{2}f)^{2\omega+1}$. Therefore, we assume from now on
that $v^{\prime}_{1}\in B^{+}$. Let us also choose $v^{\prime}_{2}\in B^{*}$
such that $\gamma(v^{\prime}_{2})=q_{2}$. We now define
$p=\ell\times\omega(N)\times\omega(M)\times\omega(Q)$, $u=(u^{\prime})^{p}$,
$v_{1}=(u^{\prime})^{p-1}v^{\prime}_{1}$ and
$v_{2}=uv^{\prime}_{2}u(uv_{1}uv^{\prime}_{2}u)^{p-1}$. We compute
$\gamma(u)=f$, $\gamma(v_{1})=fq_{1}$ and $\delta(u)=\delta(v_{1})$. Moreover,
since $p$ is a multiple of $\omega(N)$, the element $\delta(u)=\delta(v_{1})$
is an idempotent $g\in E(N)$. Finally, we have
$\gamma(v_{2})=fq_{2}f(fq_{1}fq_{2}f)^{p-1}$ and
$\delta(v_{2})=(g\delta(v^{\prime}_{2})g)^{p}$. In particular, it follows that
$\delta(v_{2})$ is an idempotent $h\in E(N)$ such that $gh=hg=h$.

We prove that $(uv_{1}uv_{2}u)^{p}$ and
$(uv_{1}uv_{2}u)^{p}uv_{2}u(uv_{1}uv_{2}u)^{p}$ are equivalent for the
syntactic congruence of $K_{\ell}\cap\beta^{-1}(s)\cap\delta^{-1}(r)$. This
will imply that they have the same image under $\gamma$, which yields
$(fq_{1}fq_{2}f)^{\omega}=(fq_{1}fq_{2}f)^{\omega}fq_{2}f(fq_{1}fq_{2}f)^{2\omega-1}$.
One may then multiply by $fq_{1}fq_{2}f$ on the right to get (4), as desired.
For $x,y\in A^{*}$, let $z_{1}=x(uv_{1}uv_{2}u)^{p}y$ and
$z_{2}=x(uv_{1}uv_{2}u)^{p}uv_{2}u(uv_{1}uv_{2}u)^{p}y$. We have to show that
$z_{1}\in K_{\ell}\cap\beta^{-1}(s)\cap\delta^{-1}(r)$ if and only if
$z_{2}\in K_{\ell}\cap\beta^{-1}(s)\cap\delta^{-1}(r)$. We first treat the
special case where $|u|<\ell$.

Assume that $|u|<\ell$. We show that in this case $z_{1}\not\in K_{\ell}$ and
$z_{2}\not\in K_{\ell}$ (which implies the desired result). Since
$u=(u^{\prime})^{p}$ and $p\geq\ell$, the hypothesis that $|u|<\ell$ yields
$u=u^{\prime}=\varepsilon$. Since $\delta(u)=\delta(v_{1})$, we get
$\delta(v_{1})=1_{N}$. Recall that $v_{1}=(u^{\prime})^{p-1}v^{\prime}_{1}$
and $v^{\prime}_{1}\in B^{+}$ by hypothesis. Thus, $v_{1}\in B^{+}$, which
means that it contains a letter $b\in B$ such that
$\delta(b)\mathrel{\mathscr{J}}1_{N}$. In particular
$d_{\mathrel{\mathscr{J}}}(b)=0$. Hence, $b$ is an infix of length $1$ of both
$z_{1}$ and $z_{2}$ such that $d_{\mathrel{\mathscr{J}}}(b)<1$. Now
$\ell>|u|=0$, so that $\ell\geq 1$. This implies $z_{1}\not\in K_{\ell}$ and
$z_{2}\not\in K_{\ell}$. This completes the special case.

From now on, we assume that $|u|\geq\ell$. Since $\delta(u)=\delta(v_{1})=g\in
E(N)$, $\delta(v_{2})=h\in E(N)$ and $gh=hg=h$, we have
$\delta(z_{1})=\delta(z_{2})=\delta(x)h\delta(y)$. Therefore,
$z_{1}\in\delta^{-1}(r)$ if and only if $z_{2}\in\delta^{-1}(r)$. Let us prove
that $z_{1}\in K_{\ell}\Leftrightarrow z_{2}\in K_{\ell}$. This is trivial if
$\ell=0$ since $K_{0}=B^{*}$. Assume now that $\ell\geq 1$. Since
$|u|\geq\ell$ by hypothesis, it follows that for every $k\leq\ell$, $z_{1}$
and $z_{2}$ have the same infixes of length $k$. This implies that $z_{1}\in
K_{\ell}\Leftrightarrow z_{2}\in K_{\ell}$, as desired.

It remains to prove that if $z_{1},z_{2}\in K_{\ell}\cap\delta^{-1}(r)$, then
$\beta(z_{1})=\beta(z_{2})$. We first show that our assumptions imply
$g\mathrel{\mathscr{J}}h$. Again, there are two cases. First, assume that
$\ell=0$. Since $d_{\mathrel{\mathscr{J}}}(r)\leq\ell$ by hypothesis, we get
$r\mathrel{\mathscr{J}}1_{N}$. Thus, since $u$ and $v_{2}$ are infixes of
$z_{1}\in\delta^{-1}(r)$, we have
$\delta(u)\mathrel{\mathscr{J}}\delta(v_{2})\mathrel{\mathscr{J}}1_{N}$, which
exactly says that $g\mathrel{\mathscr{J}}h\mathrel{\mathscr{J}}1_{N}$. Assume
now that $\ell\geq 1$. Recall that $|u|\geq\ell$. Since $u$ is an infix of
$v_{2}$, this also implies that $|v_{2}|\geq\ell$. Hence, since $u$ and
$v_{2}$ are infixes of $z_{2}\in K_{\ell}\cap\delta^{-1}(r)$, we get
$d_{\mathrel{\mathscr{J}}}(u)\geq\ell$ and
$d_{\mathrel{\mathscr{J}}}(v_{2})\geq\ell$,
$r\leqslant_{\mathscr{J}}\delta(u)$ and
$r\leqslant_{\mathscr{J}}\delta(v_{2})$. In particular, it follows that
$d_{\mathrel{\mathscr{J}}}(r)\geq d_{\mathrel{\mathscr{J}}}(u)\geq\ell$ and
$d_{\mathrel{\mathscr{J}}}(r)\geq d_{\mathrel{\mathscr{J}}}(v_{2})\geq\ell$.
Since $d_{\mathrel{\mathscr{J}}}(r)\leq\ell$ by hypothesis on $r$, we get
$d_{\mathrel{\mathscr{J}}}(r)=d_{\mathrel{\mathscr{J}}}(u)=d_{\mathrel{\mathscr{J}}}(v_{2})=\ell$.
Together with $r\leqslant_{\mathscr{J}}\delta(u)$ and
$r\leqslant_{\mathscr{J}}\delta(v_{2})$, this yields
$r\mathrel{\mathscr{J}}\delta(u)\mathrel{\mathscr{J}}\delta(v_{2})$, _i.e._ ,
$r\mathrel{\mathscr{J}}g\mathrel{\mathscr{J}}h$. This completes the proof that
$g\mathrel{\mathscr{J}}h$. Since we also know that $hg=gh=h$, we have
$h\leqslant_{\mathscr{R}}g$ and Lemma 2.1 yields $g\mathrel{\mathscr{R}}h$. We
get $z\in N$ such that $g=hz$. Thus, we have $h=hg=hhz=hz=g$.

Altogether, we obtain $\delta(u)=\delta(v_{1})=\delta(v_{2})=g\in E(N)$. This
implies that $(\beta(u),\beta(v_{1}))$ and $(\beta(u),\beta(v_{2}))$ are
$\delta$-pairs for $\beta$. Moreover, recall that $u=(u^{\prime})^{p}$ where
$p$ is a multiple of $\omega(M)$. Hence, we have $\beta(u)\in E(M)$.
Consequently, it follows from Lemma 5.16 that
$\beta((uv_{1}uv_{2}u)^{p})=\beta((uv_{1}uv_{2}u)^{p}uv_{2}u(uv_{1}uv_{2}u)^{p})$.
It now suffices to multiply by $\beta(x)$ on the left and $\beta(y)$ on the
right to obtain $\beta(z_{1})=\beta(z_{2})$, as desired.

We now turn to the second step of the proof, which is formalized in the
following statement.

######  Proposition 5.22.

Let $\ell\leq|N|$ and $s\in M$. There exists a
$\textup{TL}[\mathcal{C}_{\delta}]$ formula $\varphi_{\ell,s}$ such that for
every $w\in K_{\ell}$, we have
$w,0\models\varphi_{\ell,s}\Leftrightarrow\beta(w)=s$.

Let us first use Proposition 5.22 to complete the main proof: we have to show
that every language recognized by $\beta$ belongs to
$\textup{TL}(\mathcal{C}_{\delta})$. Clearly, it suffices to show that
$\beta^{-1}(s)\in\textup{TL}(\mathcal{C}_{\delta})$ for each $s\in M$. We
apply Proposition 5.22 for $\ell=0$. Since $K_{0}=B^{*}$, this yields a
formula $\varphi_{0,s}\in\textup{TL}[\mathcal{C}_{\delta}]$ such that
$L_{min}(\varphi_{0,s})=\beta^{-1}(s)$. Thus,
$\beta^{-1}(s)\in\textup{TL}(\mathcal{C}_{\delta})$, as desired.

It remains to prove Proposition 5.22. We construct
$\varphi_{\ell,s}\in\textup{TL}[\mathcal{C}_{\delta}]$ by induction on
$|N|-\ell$. If $\ell=|N|$, we define $\varphi_{\ell,s}$ so that
$L_{min}(\varphi_{\ell,s})=K_{\ell}\cap\beta^{-1}(s)$. Since
$K_{|N|}\cap\beta^{-1}(s)$ is finite and $\textup{TL}[\mathcal{C}_{\delta}]$
is closed under disjunction, it suffices to build for every word $w\in B^{*}$
a $\textup{TL}[\mathcal{C}_{\delta}]$ formula $\varphi_{w}$ defining
$\\{w\\}$. Since $B^{*}\in\mathcal{C}_{\delta}$, one may use the “F ”
modality. For $w=b_{1}\cdots b_{n}$, let

$\psi_{w}=\mbox{$\textup{F}\,($}b_{1}\wedge\mbox{$\textup{F}\,(b_{2}\wedge\mbox{$\textup{F}\,(b_{3}\wedge\cdots\wedge\mbox{$\textup{F}\,b_{n}$})$})$}).$

One may then choose $\varphi_{w}=\psi_{w}\wedge\bigwedge_{\mathit{u}\in
B^{*},|u|=|w|+1}\neg\psi_{u}$.

Assume now that $\ell<|N|$. We present a construction for splitting the words
in $K_{\ell}$ into two parts: a prefix mapped to an element $r\in N$ such that
$d_{\mathrel{\mathscr{J}}}(r)\leq\ell$ (we handle it with Proposition 5.20)
and a suffix that we abstract as a word in $K_{\ell+1}$ (we handle it by
induction).

Let $w\in K_{\ell}$. For each position $i\in\textup{{Pos}}(w)\setminus\\{0\\}$
and $k\in{\rm Nature}$, we write $\sigma_{k}(w,i)\in B^{*}$ for the infix
$w(i-1,j)$ where $j=\min(i+k,|w|+1)$. In other words,
$\sigma_{k}(w,i)=w[i]\cdots w[i+k-1]$ if $i+k-1\leq|w|$ and
$\sigma_{k}(w,i)=w[i]\cdots w[|w|]$ otherwise. In particular, we have
$|\sigma_{k}(w,i)|\leq k$.

######  Lemma 5.23.

Let $k\leq\ell+1$ and $u\in B^{*}$ be such that $|u|\leq k$. There exists a
formula $\pi_{k,u}\in\textup{TL}[\mathcal{C}_{\delta}]$ such that for all
$w\in K_{\ell}$ and $i\in\textup{{Pos}}(w)\setminus\\{0\\}$,
$w,i\models\pi_{k,u}\Leftrightarrow\sigma_{k}(w,i)=u$.

######  Proof 5.24.

If $u=\varepsilon$, it suffices to define $\pi_{k,u}=\top$ when $k=0$ and
$\pi_{k,u}=max$ when $k\geq 1$. Assume now that $|u|\geq 1$. If $k\leq 1$, it
follows that $|u|=1=k$. Hence, $u$ is a letter $b\in B$ and it suffices to
define $\pi_{k,u}=b$. Assume now that $k\geq 2$. Let $C\subseteq B$ be the set
of letters mapped to $1_{N}$ under $\delta$, so that
$H\stackrel{{\scriptstyle\smash{\text{\tiny
def}}}}{{=}}\delta^{-1}(1_{N})=C^{*}$. By definition,
$H\in\mathcal{C}_{\delta}$. Since $2\leq k\leq\ell+1$, we have $\ell\geq 1$,
which implies, by definition of $K_{\ell}$, that no word of $K_{\ell}$ can
contain a letter $b$ with $d_{\mathrel{\mathscr{J}}}(b)=0$. In particular,
words of $K_{\ell}$ cannot contain letters of $C$. Therefore, if $w\in
K_{\ell}$, $i\in\textup{{Pos}}(w)$ and
$\psi\in\textup{TL}[\mathcal{C}_{\delta}]$, we have
$w,i\models\mbox{$\textup{F}_{H}\,\psi$}$ if and only if $w,i+1\models\psi$.
Let $u=b_{1}\cdots b_{n}$ (with $b_{i}\in B$). We have $n=|u|\leq k$ by
hypothesis. We consider two cases for defining $\pi_{k,u}$:

  * •

If $n=k$, we let
$\pi_{k,u}=(b_{1}\wedge\mbox{$\textup{F}_{H}\,(b_{2}\wedge\mbox{$\textup{F}_{H}\,(b_{3}\wedge\cdots\mbox{$\textup{F}_{H}\,b_{n}$})$})$})$.

  * •

If $n<k$, we let
$\pi_{k,u}=(b_{1}\wedge\mbox{$\textup{F}_{H}\,(b_{2}\wedge\mbox{$\textup{F}_{H}\,(b_{3}\wedge\cdots\mbox{$\textup{F}_{H}\,(b_{n}\wedge\mbox{$\textup{F}_{H}\,max$})$})$})$})$.

The above fact on $\textup{F}_{H}\,$ implies that this definition fulfills the
desired property.

Pointed positions. Consider $w\in K_{\ell}$. We say that an arbitrary position
$i\in\textup{{Pos}}(w)$ is _pointed_ when either $i\in\\{0,|w|+1\\}$, or
$i\in\textup{{Pos}}_{c}(w)$ and
$d_{\mathrel{\mathscr{J}}}(\sigma_{\ell+1}(w,i))\geq\ell+1$.

######  Definition 5.25 (Detection of pointed positions in
$\textup{TL}[\mathcal{C}_{\delta}]$).

Let $\pi=min\vee max\vee\bigvee_{u\in U}\pi_{\ell+1,u}$ where $U=\\{u\in
B^{*}\mid|u|\leq\ell+1\text{ and }d_{\mathrel{\mathscr{J}}}(u)\geq\ell+1\\}$.
By definition of $\pi_{\ell+1,u}$ in Lemma 5.23, we know that for $w\in
K_{\ell}$ and $i\in\textup{{Pos}}(w)$, we have $w,i\models\pi$ if and only if
position $i$ is pointed.

A position $i\in\textup{{Pos}}(w)$ which is _not_ pointed is said to be
_safe_. We now prove that we may constrain the evaluation of
$\textup{TL}[\mathcal{C}_{\delta}]$ formulas to infixes that only contain
_safe_ positions.

######  Lemma 5.26.

Let $\psi\in\textup{TL}[\mathcal{C}_{\delta}]$ and $H\in\mathcal{C}_{\delta}$.
There exist two formulas $\textup{F}^{sa}_{H}\,\psi$ and
$\textup{P}^{sa}_{H}\,\psi$ of $\textup{TL}[\mathcal{C}_{\delta}]$ such that
for all $w\in K_{\ell}$ and all $i\in\textup{{Pos}}(w)$, the two following
properties hold:

  * •

$w,i\models\textup{F}^{sa}_{H}\,\psi$ if and only if there exists
$j\in\textup{{Pos}}(w)$ such that $j>i$, $w,j\models\psi$, $w(i,j)\in H$ and
all positions $h\in\textup{{Pos}}(w)$ such that $i<h<j$ are safe.

  * •

$w,i\models\textup{P}^{sa}_{H}\,\psi$ if and only if there exists
$j\in\textup{{Pos}}(w)$ such that $j<i$, $w,j\models\psi$, $w(j,i)\in H$ and
all positions $h\in\textup{{Pos}}(w)$ such that $j<h<i$ are safe.

######  Proof 5.27.

We begin by characterizing infixes containing only safe positions. Let $w\in
K_{\ell}$ and $i,j\in\textup{{Pos}}(w)$ be such that $i<j$. We prove that the
following two properties are equivalent:

  1. 1.

All positions $h\in\textup{{Pos}}(w)$ such that $i<h<j$ are safe.

  2. 2.

Either $\delta(w(i,j))=1_{N}$ or
$d_{\mathrel{\mathscr{J}}}(w(i,j)\sigma_{\ell}(w,j))\leq\ell$.

Assume first that all positions $h\in\textup{{Pos}}(w)$ such that $i<h<j$ are
safe. If $i+1=j$, then $w(i,j)=\varepsilon$, whence $\delta(w(i,j))=1_{N}$.
Assume now that $i+1<j$. Observe that $w(i,j)\sigma_{\ell}(w,j)$ belongs to
$K_{\ell}$ since it is an infix of $w\in K_{\ell}$. Moreover, since $i+1<j$,
there exists at least one $h\in\textup{{Pos}}(w)$ such that $i<h<j$. Combined
with the assumption that all such positions $h$ are safe, this implies that
for every $x,y,z\in B^{*}$ such that $xyz=w(i,j)\sigma_{\ell}(w,j)$ and
$|y|\leq\ell+1$, we have $d_{\mathrel{\mathscr{J}}}(y)\leq\ell$. Therefore,
Lemma 5.18 entails that
$d_{\mathrel{\mathscr{J}}}(w(i,j)\sigma_{\ell}(w,j))\leq\ell$, as desired.

Conversely, assume that either $\delta(w(i,j))=1_{N}$ or
$d_{\mathrel{\mathscr{J}}}(w(i,j)\sigma_{\ell}(w,j))\leq\ell$. We start with
the latter case. Since $w(i,j)\sigma_{\ell}(w,j)\in K_{\ell}$, Lemma 5.18
implies that for every $x,y,z\in B^{*}$ such that
$xyz=w(i,j)\sigma_{\ell}(w,j)$ and $|y|\leq\ell+1$, we have
$d_{\mathrel{\mathscr{J}}}(y)\leq\ell$. In particular, it follows that every
$h\in\textup{{Pos}}(w)$ such that $i<h<j$ is safe. Assume now that
$\delta(w(i,j))=1_{N}$. If $\ell=0$, then $\sigma_{\ell}(w,j)=\varepsilon$ and
we are back to the previous case. Otherwise, $\ell\geq 1$ and since $w\in
K_{\ell}$, the fact that $\delta(w(i,j))=1_{N}$ yields $w(i,j)=\varepsilon$,
which completes the argument.

We are now ready to complete the proof of the lemma. Let
$\psi\in\textup{TL}[\mathcal{C}_{\delta}]$ and $H\in\mathcal{C}_{\delta}$. For
every $r\in N$, we let $H_{r}=H\cap\delta^{-1}(r)$ and $U_{r}=\\{u\in
B^{*}\mid|u|\leq\ell\text{ and
}d_{\mathrel{\mathscr{J}}}(r\delta(u))\leq\ell\\}$. Observe that
$H_{r}\in\mathcal{C}_{\delta}$. Now, in view of the preliminary result, it
suffices to define,

$\textup{F}^{sa}_{H}\,\psi=\mbox{$\textup{F}_{H_{1_{N}}}\,\psi$}\vee\bigvee_{r\in
N}\bigvee_{u\in
U_{r}}\mbox{$\textup{F}_{H_{r}}\,\left(\pi_{\ell,u}\wedge\psi\right)$}\ \
\text{and}\ \
\textup{P}^{sa}_{H}\,\psi=\textup{P}_{H_{1_{N}}}\,\psi\vee\bigvee_{r\in
N}\bigvee_{u\in
U_{r}}\left(\pi_{\ell,u}\wedge\textup{P}_{H_{r}}\,\psi\right).$

This completes the proof.

Pointed decomposition. Let $w\in K_{\ell}$ and let
$0=i_{0}<i_{1}<\dots<i_{n}<i_{n+1}=|w|+1$ be all the pointed positions of $w$.
The _pointed decomposition_ of $w$ is the decomposition
$w=w_{0}b_{1}w_{1}\cdots b_{n}w_{n}$ where the highlighted letters
$b_{1},\dots,b_{n}\in B$ are those carried by the pointed positions
$i_{1},\dots,i_{n}$. For $0\leq j\leq n$, we associate the word
$f(w,i_{j})=w_{j}$ to the pointed position $i_{j}$. Moreover, we define a new
word $\widehat{w}\in B^{*}$ built from the suffix $b_{1}w_{1}\cdots
b_{n}w_{n}$. For $1\leq j\leq n$, let
$(t_{j},q_{j})=(\beta(b_{j}w_{j}),\delta(b_{j}w_{j}))\in P$. By definition of
$\beta$ and $\delta$, we know that there is a letter $b_{t_{j},q_{j}}\in B$
such that $(\beta(b_{t_{j},q_{j}}),\delta(b_{t_{j},q_{j}}))=(t_{j},q_{j})$. We
let $\widehat{w}=b_{t_{1},q_{1}}\cdots b_{t_{n},q_{n}}$. Note that by
definition, $\beta(b_{1}w_{1}\cdots b_{n}w_{n})=\beta(\widehat{w})$ and
$\delta(b_{1}w_{1}\cdots b_{n}w_{n})=\delta(\widehat{w})$. Finally, we define
a surjective map $i\mapsto\mu(i)$ associating a position
$\mu(i)\in\textup{{Pos}}(\widehat{w})$ to each _pointed_ position
$i\in\textup{{Pos}}(w)$: for $0\leq j\leq n+1$, we let $\mu(i_{j})=j$. We
complete this definition with a key property. For every pointed position
$i\in\\{0\\}\cup\textup{{Pos}}_{c}(w)$, one can compute the images of the word
$f(w,i)$ under $\beta$ and $\delta$ with a $\textup{TL}[\mathcal{C}_{\delta}]$
formula. This is where we use Proposition 5.20.

######  Lemma 5.28.

Let $(t,r)\in M\times N$. There exists
$\Gamma_{t,r}\in\textup{TL}[\mathcal{C}_{\delta}]$ such that for all $w\in
K_{\ell}$ and all pointed positions $i\in\\{0\\}\cup\textup{{Pos}}_{c}(w)$, we
have $w,i\models\Gamma_{t,r}\Leftrightarrow\beta(f(w,i))=t\text{ and
}\delta(f(w,i))=r$.

######  Proof 5.29.

First observe that by definition, if $w\in K_{\ell}$ and
$i\in\\{0\\}\cup\textup{{Pos}}_{c}(w)$ is pointed, the infix $f(w,i)$ contains
only _safe_ positions. Hence, for every $x,y,z\in B^{*}$ such that
$f(w,i)=xyz$ and $|y|\leq\ell+1$, we have
$d_{\mathrel{\mathscr{J}}}(y)\leq\ell$. By Lemma 5.18, it follows that
$d_{\mathrel{\mathscr{J}}}(f(w,i))\leq\ell$. Therefore, if
$d_{\mathrel{\mathscr{J}}}(r)>\ell$, then $\delta(f(w,i))$ cannot be equal to
$r$, and it suffices to define $\Gamma_{t,r}=\bot$.

We now assume that $d_{\mathrel{\mathscr{J}}}(r)\leq\ell$. Proposition 5.20
implies that
$K_{\ell}\cap\beta^{-1}(t)\cap\delta^{-1}(r)\in\textup{TL}(\mathcal{C}_{\delta})$.
We get a formula $\psi\in\textup{TL}[\mathcal{C}_{\delta}]$ such that for
every $u\in K_{\ell}$, we have $u,0\models\psi$ if and only if $\beta(u)=t$
and $\delta(u)=r$. Using Lemma 5.26, we modify $\psi$ so that given $w\in
K_{\ell}$, the evaluation of $\psi$ at a pointed position $i$ is constrained
to the infix $f(w,i)$. More precisely, we use structural induction to build
two formulas $\langle\psi\rangle_{min}$ and $\langle\psi\rangle_{max}$ such
that given $w\in K_{\ell}$, a pointed position
$i\in\\{0\\}\cup\textup{{Pos}}_{c}(w)$ and $j\in\textup{{Pos}}(f(w,i))$, the
two following properties hold:

  * •

If $j\leq|f(w,i)|$, then $w,i+j\models\langle\psi\rangle_{min}\Leftrightarrow
f(w,i),j\models\psi$.

  * •

If $1\leq j$, then $w,i+j\models\langle\psi\rangle_{max}\Leftrightarrow
f(w,i),j\models\psi$.

It will then suffice to define $\Gamma_{t,r}=\langle\psi\rangle_{min}$. We
only describe the construction, and leave it to the reader to check that it
satisfies the above properties. Note that we use the formula
$\pi\in\textup{TL}[\mathcal{C}_{\delta}]$ of Definition 5.25 that detects
pointed positions.

For $\psi\in B\cup\\{\top,\bot\\}$, we let
$\langle\psi\rangle_{min}=\langle\psi\rangle_{max}=\psi$. If $\psi=min$, we
let $\langle\psi\rangle_{min}=\pi$ and $\langle\psi\rangle_{max}=\bot$. If
$\psi=max$, we let $\langle\psi\rangle_{min}=\bot$ and
$\langle\psi\rangle_{max}=\pi$. We handle Boolean operators in the expected
way. For instance, we define
$\langle\psi^{\prime}\vee\psi^{\prime\prime}\rangle_{min}=\langle\psi^{\prime}\rangle_{min}\vee\langle\psi^{\prime\prime}\rangle_{min}$,
$\langle\psi^{\prime}\wedge\psi^{\prime\prime}\rangle_{min}=\langle\psi^{\prime}\rangle_{min}\wedge\langle\psi^{\prime\prime}\rangle_{min}$
and
$\langle\neg\psi^{\prime}\rangle_{min}=\neg\langle\psi^{\prime}\rangle_{min}$,
and similarly for $\langle\cdot\rangle_{max}$. If
$\psi=\mbox{$\textup{F}_{H}\,\psi^{\prime}$}$ for $H\in\mathcal{C}_{\delta}$,
we let
$\langle\psi\rangle_{min}=\textup{F}^{sa}_{H}\,\langle\psi^{\prime}\rangle_{max}$
and
$\langle\psi\rangle_{max}=\neg\pi\wedge\textup{F}^{sa}_{H}\,\langle\psi^{\prime}\rangle_{max}$.
Symmetrically, if $\psi=\textup{P}_{H}\,\psi^{\prime}$ for some
$H\in\mathcal{C}_{\delta}$, we define
$\langle\psi\rangle_{min}=\neg\pi\wedge\textup{P}^{sa}_{H}\,\langle\psi^{\prime}\rangle_{min}$
and
$\langle\psi\rangle_{max}=\textup{P}^{sa}_{H}\,\langle\psi^{\prime}\rangle_{min}$.
This concludes the inductive construction of $\langle\psi\rangle_{min}$ and
$\langle\psi\rangle_{max}$ and the proof of the proposition.

Construction of the formulas $\varphi_{\ell,s}$. We are ready to complete the
proof of Proposition 5.22. For every $s\in M$, we build a formula
$\zeta_{s}\in\textup{TL}[\mathcal{C}_{\delta}]$ such that for every $w\in
K_{\ell}$, we have $w,0\models\zeta_{s}\Leftrightarrow\beta(\widehat{w})=s$.
Given $s\in M$, it will then suffice to define
$\varphi_{\ell,s}\in\textup{TL}[\mathcal{C}_{\delta}]$ as follows:

$\varphi_{\ell,s}=\bigvee_{\\{(s_{1},s_{2})\in M^{2}\mid
s_{1}s_{2}=s\\}}\Bigl{(}\Bigl{(}\bigvee_{r\in
N}\Gamma_{s_{1},r}\Bigr{)}\wedge\zeta_{s_{2}}\Bigr{)}.$

Indeed, it is straightforward that for every word $w\in K_{\ell}$, we have
$\beta(w)=\beta(f(w,0))\beta(\widehat{w})$. Consequently, by definition of
$\varphi_{\ell,s}$, we get
$w,0\models\varphi_{\ell,s}\Leftrightarrow\beta(f(w,0))\beta(\widehat{w})=s\Leftrightarrow\beta(w)=s$
for all $w\in K_{\ell}$, which concludes the proof of Proposition 5.22. We now
concentrate on building $\zeta_{s}$. This is where we use induction in
Proposition 5.22. Indeed, we have the following lemma.

######  Lemma 5.30.

For every $w\in K_{\ell}$, we have $\widehat{w}\in K_{\ell+1}$.

######  Proof 5.31.

Let $k\leq\ell+1$ and $x,y,z\in B^{*}$ such that $\widehat{w}=xyz$ and
$|y|=k$. We have to prove that $d_{\mathrel{\mathscr{J}}}(y)\geq k$. Let
$w=w_{0}b_{1}w_{1}\cdots b_{n}w_{n}$ be the pointed decomposition of $w$. By
definition of $\widehat{w}$, we have $\delta(y)=\delta(b_{h}w_{h}\cdots
b_{h+k-1}w_{h+k-1})$ for some $h\leq n$. Let $u=b_{h}w_{h}\cdots
b_{h+k-1}w_{h+k-1}$. We have to show that
$d_{\mathrel{\mathscr{J}}}(y)=d_{\mathrel{\mathscr{J}}}(u)\geq k$. Clearly,
$|u|\geq k$. Hence, if $k\leq\ell$, the hypothesis that $w\in K_{\ell}$ yields
$d_{\mathrel{\mathscr{J}}}(u)\geq k$. Otherwise, $k=\ell+1$. Thus,
$|u|\geq\ell+1$ and since the position labeled by $b_{h}$ in $w$ is pointed,
this yields $d_{\mathrel{\mathscr{J}}}(u)\geq\ell+1$. In both cases, we get
$d_{\mathrel{\mathscr{J}}}(y)\geq k$.

Let $s\in M$. In view of Lemma 5.30, induction on $|N|-\ell$ in Proposition
5.22 yields a $\textup{TL}[\mathcal{C}_{\delta}]$ formula $\psi_{s}$ such that
for every $w\in K_{\ell}$, we have
$\widehat{w},0\models\psi_{s}\Leftrightarrow\beta(\widehat{w})=s$. Thus, it
now suffices to prove that for every
$\psi\in\textup{TL}[\mathcal{C}_{\delta}]$, there exists a formula
$\lfloor\psi\rfloor\in\textup{TL}[\mathcal{C}_{\delta}]$ such that for every
$w\in K_{\ell}$ and every pointed position $i\in\textup{{Pos}}(w)$, we have
$w,i\models\lfloor\psi\rfloor\Leftrightarrow\widehat{w},\mu(i)\models\psi$. It
will then follow, for $i=0$, that
$w,0\models\lfloor\psi_{s}\rfloor\Leftrightarrow\beta(\widehat{w})=s$, meaning
that we can define $\zeta_{s}=\lfloor\psi_{s}\rfloor$.

We construct $\lfloor\psi\rfloor$ by structural induction on $\psi$. If
$\psi\in\\{min,max,\top,\bot\\}$, we let $\lfloor\psi\rfloor=\psi$. Suppose
now that $\psi=b_{t,q}\in B$ for $(t,q)\in P$. Thus, when evaluated in $w$ at
a pointed position $i$ carrying a “$b$”, we want $\lfloor\psi\rfloor$ to check
that $\beta(b)\beta(f(w,i))=t$ and $\delta(b)\delta(f(w,i))=q$. Let
$T=\bigl{\\{}(b,t^{\prime},q^{\prime})\in B\times M\times
N\mid\beta(b)t^{\prime}=t\text{ and }\delta(b)q^{\prime}=q\bigr{\\}}$. Using
the formulas $\Gamma_{t^{\prime},q^{\prime}}$ from Lemma 5.28, we define
$\psi=\bigvee_{(b,t^{\prime},q^{\prime})\in
T}\left(b\wedge\Gamma_{t^{\prime},q^{\prime}}\right)$. Boolean operators are
handled as expected. It remains to deal with temporal modalities, _i.e._ , the
case where there exists $H\in\mathcal{C}_{\delta}$ such that
$\psi=\mbox{$\textup{F}_{H}\,\psi^{\prime}$}$ or
$\psi=\textup{P}_{H}\,\psi^{\prime}$. For every $b\in B$, let
$F_{b}=\bigl{\\{}r\in N\mid\delta(b)r\in\delta(H)\bigr{\\}}$. We define:

$\lfloor\mbox{$\textup{F}_{H}\,\psi^{\prime}$}\rfloor\stackrel{{\scriptstyle\text{def}}}{{=}}\left\\{\begin{array}[]{l@{}ll}\textup{F}^{sa}_{B^{*}}\,\bigl{(}\pi\wedge{}&\left(\bigvee_{b\in
B}\left(b\wedge\mbox{$\textup{F}_{\delta^{-1}(F_{b})}\,(\pi\wedge\lfloor\psi^{\prime}\rfloor)$}\right)\right)\bigr{)}&\text{if
$\varepsilon\not\in H$},\\\\[4.30554pt]
\textup{F}^{sa}_{B^{*}}\,\bigl{(}\pi\wedge{}&\left(\bigvee_{b\in
B}\left(b\wedge\mbox{$\textup{F}_{\delta^{-1}(F_{b})}\,(\pi\wedge\lfloor\psi^{\prime}\rfloor)$}\right)\vee\lfloor\psi^{\prime}\rfloor\right)\bigr{)}&\text{if
$\varepsilon\in H$}.\end{array}\right.$
$\lfloor\textup{P}_{H}\,\psi^{\prime}\rfloor\stackrel{{\scriptstyle\text{def}}}{{=}}\left\\{\begin{array}[]{l@{\;}ll}&\bigvee_{b\in
B}\textup{P}_{\delta^{-1}(F_{b})}\,\left(\pi\wedge
b\wedge\textup{P}^{sa}_{B^{*}}\,\left(\pi\wedge\lfloor\psi^{\prime}\rfloor\right)\right)&\text{if
$\varepsilon\not\in H$},\\\
\textup{P}^{sa}_{B^{*}}\,\left(\pi\wedge\lfloor\psi^{\prime}\rfloor\right)\vee&\bigvee_{b\in
B}\textup{P}_{\delta^{-1}(F_{b})}\,\left(\pi\wedge
b\wedge\textup{P}^{sa}_{B^{*}}\,\left(\pi\wedge\lfloor\psi^{\prime}\rfloor\right)\right)&\text{if
$\varepsilon\in H$}.\end{array}\right.$

We give an intuition when $\psi=\mbox{$\textup{F}_{H}\,\psi^{\prime}$}$ and
$\varepsilon\notin H$. Let $w_{0}b_{1}w_{1}\cdots b_{n}w_{n}$ be the pointed
decomposition of $w$ and $\widehat{w}=b^{\prime}_{1}\cdots b^{\prime}_{n}$.
Let $i_{k}\in\textup{{Pos}}(w)$ be the position of the distinguished $b_{k}$,
so that $\mu(i_{k})=k$. Now,
$\widehat{w},k\models\mbox{$\textup{F}_{H}\,\psi^{\prime}$}$ when there exists
$m>k$ such that $\widehat{w},m\models\psi^{\prime}$ and
$b^{\prime}_{k+1}\cdots b^{\prime}_{m-1}\in H$. The construction ensures that
$w,i_{k}\models\lfloor\mbox{$\textup{F}_{H}\,\psi^{\prime}$}\rfloor$ when
there exists $m>k$ such that $w,i_{m}\models\lfloor\psi^{\prime}\rfloor$ and
$b_{k+1}w_{k+1}\cdots b_{m-1}w_{m-1}\in H$. The purpose of using
$\textup{F}^{sa}_{B^{*}}\,(\pi\wedge\dots)$ is to “jump” to $b_{k+1}$. The
remainder checks that the next jump, to a pointed position, determines a word
of $\delta^{-1}(\delta(H))=H$. More generally, one can check that
$w,i\models\lfloor\psi\rfloor\Leftrightarrow\widehat{w},\mu(i)\models\psi$ for
all $w\in K_{\ell}$ and all pointed positions $i\in\textup{{Pos}}(w)$. This
concludes the proof.

##  6 Natural restrictions of generalized unary temporal logic

We turn to two natural restrictions of the classes $\textup{TL}(\mathcal{C})$,
which were defined in [26]: the pure-future and pure-past fragments. For a
class $\mathcal{C}$, we write
$\textup{FL}[\mathcal{C}]\subseteq\textup{TL}[\mathcal{C}]$ for the set of all
formulas that contain only _future_ modalities (_i.e._ , the modalities
$\textup{P}_{L}$ are disallowed). Symmetrically,
$\textup{PL}[\mathcal{C}]\subseteq\textup{TL}[\mathcal{C}]$ is the set of all
formulas in $\textup{TL}[\mathcal{C}]$ that contain only _past_ modalities
(_i.e._ , the modalities $\textup{F}_{L}$ are disallowed).

We now define the two associated operators
$\mathcal{C}\mapsto\textup{FL}(\mathcal{C})$ and
$\mathcal{C}\mapsto\textup{PL}(\mathcal{C})$. For every class $\mathcal{C}$,
let $\textup{FL}(\mathcal{C})$ be the class consisting of all languages
$L_{min}(\varphi)$ where $\varphi\in\textup{FL}[\mathcal{C}]$. Symmetrically,
we write $\textup{PL}(\mathcal{C})$ for the class consisting of all languages
$L_{max}(\varphi)$, with $\varphi\in\textup{PL}[\mathcal{C}]$.

######  Remark 6.1.

Note that $\textup{FL}[\mathcal{C}]$ formulas are evaluated at the leftmost
unlabeled position whereas $\textup{PL}[\mathcal{C}]$ formulas are evaluated
at the rightmost unlabeled position.

###  6.1 Connection with left and right polynomial closure

The main ideas to establish decidable characterizations for
$\textup{FL}(\mathcal{C})$ and $\textup{PL}(\mathcal{C})$ follow the lines of
the proof of Theorem 5.1. However, there are some differences. First, for the
easy direction (proving that some property on $\mathcal{C}$-orbits is
necessary), we have to adapt Lemma 5.11 to the operators
$\mathcal{C}\mapsto\textup{FL}(\mathcal{C})$ and
$\mathcal{C}\mapsto\textup{PL}(\mathcal{C})$. We prove these adapted
properties in appendix as corollaries of results presented in [26].

The proof of the difficult direction is mostly identical to that in Theorem
5.1. However, there is a key difference: we have to find a substitute for
Proposition 5.20, whose proof relied the inclusion
$\textup{UPol}(\textup{BPol}(\mathcal{C}))\subseteq\textup{TL}(\mathcal{C})$
from Proposition 4.4. We replace unambiguous polynomial closure (UPol) by two
variants, called _right_ and _left_ polynomial closure (RPol and LPol). It is
shown [26] that
$\textup{RPol}(\textup{BPol}(\mathcal{C}))\subseteq\textup{FL}(\mathcal{C})$
and
$\textup{LPol}(\textup{BPol}(\mathcal{C}))\subseteq\textup{PL}(\mathcal{C})$
for every prevariety $\mathcal{C}$: this serves as a substitute for
Proposition 4.4. Finally, while no simple generic characterization of the
classes $\textup{RPol}(\textup{BPol}(\mathcal{C}))$ and
$\textup{LPol}(\textup{BPol}(\mathcal{C}))$ are known, we are able to replace
Theorem 4.5 by combining independent characterizations of the operators Pol
and RPol (resp. Pol and LPol) from [23, 21].

We now establish a connection between the operators
$\mathcal{C}\mapsto\textup{FL}(\mathcal{C})$ and
$\mathcal{C}\mapsto\textup{PL}(\mathcal{C})$ and the two weaker variants RPol
and LPol of unambiguous polynomial closure. Consider a marked product
$L_{0}a_{1}L_{1}\cdots a_{n}L_{n}$. For $1\leq i\leq n$, we write
$H_{i}=L_{1}a_{1}L_{2}\cdots a_{i-1}L_{i-1}$ and
$K_{i}=L_{i}a_{i+1}L_{i+1}\cdots a_{n}L_{n}$. We say that
$L_{0}a_{1}L_{1}\cdots a_{n}L_{n}$ is _right deterministic_ (resp.  _left
deterministic_) when we have $A^{*}a_{i}K_{i}\cap K_{i}=\emptyset$ (resp.
$H_{i}a_{i}A^{*}\cap H_{i}=\emptyset$) for every $i\leq n$. The _right
polynomial closure_ of a class $\mathcal{C}$, written
$\textup{RPol}(\mathcal{C})$, consists of all _finite disjoint unions_ of
_right deterministic marked products_ $L_{0}a_{1}L_{1}\cdots a_{n}L_{n}$ such
that $L_{0},\dots,L_{n}\in\mathcal{C}$ (by “disjoint” we mean that the
languages in the union must be pairwise disjoint). Similarly, the _left
polynomial closure_ $\textup{LPol}(\mathcal{C})$ of $\mathcal{C}$ consists of
all finite disjoint unions of _left_ deterministic marked products
$L_{0}a_{1}L_{1}\cdots a_{n}L_{n}$ such that
$L_{0},\dots,L_{n}\in\mathcal{C}$. While this is not immediate, it is known
[21] that when the input class $\mathcal{C}$ is a prevariety, then so are
$\textup{RPol}(\mathcal{C})$ and $\textup{LPol}(\mathcal{C})$.

As expected, we are interested in the “combined” operators
$\mathcal{C}\mapsto\textup{RPol}(\textup{BPol}(\mathcal{C}))$ and
$\mathcal{C}\mapsto\textup{LPol}(\textup{BPol}(\mathcal{C}))$. Indeed, the
first one is connected to the classes $\textup{FL}(\mathcal{C})$ by the
following result proved in [26, Proposition 5].

######  Proposition 6.2.

For every prevariety $\mathcal{C}$, we have
$\textup{RPol}(\textup{BPol}(\mathcal{C}))\subseteq\textup{FL}(\mathcal{C})$.

We have the following symmetrical statement for $\textup{PL}(\mathcal{C})$.

######  Proposition 6.3.

For every prevariety $\mathcal{C}$, we have
$\textup{LPol}(\textup{BPol}(\mathcal{C}))\subseteq\textup{PL}(\mathcal{C})$.

Propositions 6.2 and 6.3 serve as the replacement of Proposition 4.4 when
dealing with the classes $\textup{FL}(\mathcal{C})$ and
$\textup{PL}(\mathcal{C})$, respectively. It now remains to replace the
generic algebraic characterization of the classes
$\textup{UPol}(\textup{BPol}(\mathcal{C}))$ presented in Theorem 4.5. This is
more tricky as no such characterization is known for the classes
$\textup{RPol}(\textup{BPol}(\mathcal{C}))$ (nor for the classes
$\textup{LPol}(\textup{BPol}(\mathcal{C}))$). Yet, we manage to prove a
_sufficient condition_ for a language to belong to
$\textup{RPol}(\textup{BPol}(\mathcal{C}))$ or
$\textup{LPol}(\textup{BPol}(\mathcal{C}))$ by combining results of [27] and
[21]. While it does _not_ characterize these classes in general, it suffices
for our needs: proving that particular languages belong to
$\textup{RPol}(\textup{BPol}(\mathcal{C}))$ (and therefore to
$\textup{FL}(\mathcal{C})$ by Proposition 6.2) or to
$\textup{LPol}(\textup{BPol}(\mathcal{C}))$ (and therefore to
$\textup{FL}(\mathcal{C})$ by Proposition 6.3).

######  Proposition 6.4.

Let $\mathcal{C}$ be a prevariety, $L\subseteq A^{*}$ be a regular language
and $\alpha:A^{*}\to M$ be its syntactic morphism. Assume that $\alpha$
satisfies the following property:

$(esete)^{\omega+1}=ete(esete)^{\omega}\quad\text{for every $\mathcal{C}$-pair
$(e,s)\in M^{2}$ and every $t\in M$}.$ (5)

Then, $L\in\textup{RPol}(\textup{BPol}(\mathcal{C}))$.

######  Proposition 6.5.

Let $\mathcal{C}$ be a prevariety, $L\subseteq A^{*}$ be a regular language
and $\alpha:A^{*}\to M$ be its syntactic morphism. Assume that $\alpha$
satisfies the following property:

$(esete)^{\omega+1}=(esete)^{\omega}ese\quad\text{for every $\mathcal{C}$-pair
$(e,t)\in M^{2}$ and every $s\in M$}.$

Then, $L\in\textup{LPol}(\textup{BPol}(\mathcal{C}))$.

Since Propositions 6.4 and 6.5 are symmetrical, we only prove the first one
and leave the second to the reader.

######  Proof 6.6 (Proof of Proposition 6.4).

We use a generic characterization of the classes $\textup{RPol}(\mathcal{D})$
proved in [21]. Let us first present it. For every class $\mathcal{D}$, we
define a preorder $\preceq_{\mathcal{D}}$ and an equivalence
$\sim_{\mathcal{D}}$ over $M$. Given $s,t\in M$, we let,

$\begin{array}[]{lcl}s\sim_{\mathcal{D}}t&\quad\text{if and only
if}&\text{$s\in F\Leftrightarrow t\in F$ for every $F\subseteq M$ such that
$\alpha^{-1}(F)\in\mathcal{D}$,}\\\ s\preceq_{\mathcal{D}}t&\quad\text{if and
only if}&\text{$s\in F\Rightarrow t\in F$ for every $F\subseteq M$ such that
$\alpha^{-1}(F)\in\mathcal{D}$.}\end{array}$

Clearly, $\preceq_{\mathcal{D}}$ is a preorder on $M$ and $\sim_{\mathcal{D}}$
is the equivalence generated by $\preceq_{\mathcal{D}}$. When $\alpha:A^{*}\to
M$ is the syntactic morphism of $L$, it is shown in [21, Theorem 4.1] that for
every prevariety $\mathcal{D}$, we have $L\in\textup{RPol}(\mathcal{D})$ if
and only if $s^{\omega+1}=ts^{\omega}$ for all $s,t\in M$ such that
$s\sim_{\mathcal{D}}t$.

Hence, since $\textup{BPol}(\mathcal{C})$ is a prevariety, it suffices to
prove that for every $s,t\in M$ such that
$s\sim_{\textup{BPol}(\mathcal{C})}t$, we have $s^{\omega+1}=ts^{\omega}$. We
fix $s,t$ for the proof. Since $s\sim_{\textup{BPol}(\mathcal{C})}t$, we have
$s\preceq_{\textup{BPol}(\mathcal{C})}t$. Moreover, let
$\mathit{co\textup{-}}\\!\textup{Pol}(\mathcal{C})$ be the class consisting of
all complements of languages in $\textup{Pol}(\mathcal{C})$ (_i.e._ ,
$L\in\mathit{co\textup{-}}\\!\textup{Pol}(\mathcal{C})$ if and only if
$A^{*}\setminus L\in\mathit{co\textup{-}}\\!\textup{Pol}(\mathcal{C})$).
Clearly, we have
$\mathit{co\textup{-}}\\!\textup{Pol}(\mathcal{C})\subseteq\textup{BPol}(\mathcal{C})$.
Hence, the definition implies that
$s\preceq_{\mathit{co\textup{-}}\\!\textup{Pol}(\mathcal{C})}t$

Moreover, it is shown in [27, Lemma 6.6] that
$\preceq_{\mathit{co\textup{-}}\\!\textup{Pol}(\mathcal{C})}$ is the least
preorder on $M$ such that for every $x,y,q\in M$ and $e\in E(M)$, if $(e,q)\in
M^{2}$ is a $\mathcal{C}$-pair, then
$xeqey\preceq_{\mathit{co\textup{-}}\\!\textup{Pol}(\mathcal{C})}xey$ (the
proof is based on the algebraic characterization of
$\textup{Pol}(\mathcal{C})$, see [23]). This yields $s_{0},\dots,s_{n}\in M$
such that $s=s_{0}$, $t=s_{n}$ and, for every $i\leq n$, there exist $x,y,q\in
M$ and $e\in E(M)$ such that $(e,q)\in M^{2}$ is a $\mathcal{C}$-pair,
$s_{i-1}=xeqey$ and $s_{i}=xey$. We use induction on $i$ to prove that
$s^{\omega+1}=s_{i}s^{\omega}$ for every $i\leq n$. Since $s_{n}=t$, the case
$i=n$ yields the desired result. When $i=0$, it is immediate that
$s^{\omega+1}=s_{0}s^{\omega}$ since $s_{0}=s$. Assume now that $i\geq 1$.

By induction hypothesis, we know that $s^{\omega+1}=s_{i-1}s^{\omega}$.
Moreover, we have $x,y,q\in M$ and $e\in E(M)$ such that $(e,q)\in M^{2}$ is a
$\mathcal{C}$-pair, $s_{i-1}=xeqey$ and $s_{i}=xey$. Since
$(s^{\omega+1})^{\omega+2}=s^{\omega+2}$, we get
$s^{\omega+2}=(xeqeys^{\omega})^{\omega+2}$. Hence, we get

$\begin{array}[]{lcl}s^{\omega+2}&=&x\ (eqeys^{\omega}xe)^{\omega+1}\
eqeys^{\omega}\\\ &=&x\ eys^{\omega}xe(eqeys^{\omega}xe)^{\omega}\
eqeys^{\omega}\quad\text{by\leavevmode\nobreak\ \eqref{eq:rbp} since $(e,q)$
is a $\mathcal{C}$-pair}\\\
&=&xeys^{\omega}(xeqeys^{\omega})^{\omega+1}.\end{array}$

This yields,
$s^{\omega+2}=s_{i}s^{\omega}(s_{i-1}s^{\omega})^{\omega+1}=s_{i}s^{\omega}(s^{\omega+1})^{\omega+1}=s_{i}s^{\omega+1}$.
It now remains to multiply by $s^{\omega-1}$ on the right to get
$s^{\omega+1}=s_{i}s^{\omega}$, as desired.

###  6.2 Statements

The classes $\textup{FL}(\mathcal{C})$ and $\textup{PL}(\mathcal{C})$ admit
algebraic characterizations similar to that of $\textup{TL}(\mathcal{C})$. We
reuse the $\mathcal{C}$-orbits introduced in Section 3. Let
$\mathcal{X}\in\\{\mathrel{\mathscr{L}},\mathrel{\mathscr{R}},\mathrel{\mathscr{J}}\\}$
be one the Green relations defined in Section 2. A monoid $M$ is
_$\mathcal{X}$ -trivial_ when $s\mathrel{\mathcal{X}}t$ implies $s=t$ for all
$s,t\in M$. It is standard and simple to verify that a finite monoid $M$ is
$\mathcal{R}$-trivial (resp. $\mathcal{L}$-trivial) if and only if for all
$s,t\in M$, we have $(st)^{\omega}s=(st)^{\omega}$ (resp.
$t(st)^{\omega}=(st)^{\omega}$), see [17, 20] for a proof. We are now able to
present the two symmetrical characterizations of $\textup{FL}(\mathcal{C})$
and $\textup{PL}(\mathcal{C})$.

######  Theorem 6.7.

Let $\mathcal{C}$ be a prevariety, $L\subseteq A^{*}$ be a regular language
and $\alpha:A^{*}\to M$ be its syntactic morphism. The two following
properties are equivalent:

  1. 1.

$L\in\textup{FL}(\mathcal{C})$.

  2. 2.

Every $\mathcal{C}$-orbit for $\alpha$ is $\mathrel{\mathscr{L}}$-trivial.

######  Theorem 6.8.

Let $\mathcal{C}$ be a prevariety, $L\subseteq A^{*}$ be a regular language
and $\alpha:A^{*}\to M$ be its syntactic morphism. The two following
properties are equivalent:

  1. 1.

$L\in\textup{PL}(\mathcal{C})$.

  2. 2.

Every $\mathcal{C}$-orbit for $\alpha$ is $\mathrel{\mathscr{R}}$-trivial.

Since $\textup{FL}(\mathcal{C})$ and $\textup{PL}(\mathcal{C})$ are
symmetrical, it is natural to consider a third class denoted
$\textup{FL}(\mathcal{C})\cap\textup{PL}(\mathcal{C})$. It consists of all
languages belonging simultaneously to $\textup{FL}(\mathcal{C})$ and
$\textup{PL}(\mathcal{C})$. It is standard that the finite monoids which are
both $\mathrel{\mathscr{L}}$-trivial and $\mathrel{\mathscr{R}}$-trivial are
exactly the $\mathrel{\mathscr{J}}$-trivial monoids (see [17, 20]). This
yields the following corollary of Theorems 6.7 and 6.8.

######  Corollary 6.9.

Let $\mathcal{C}$ be a prevariety, $L\subseteq A^{*}$ be a regular language
and $\alpha:A^{*}\to M$ be its syntactic morphism. The two following
properties are equivalent:

  1. 1.

$L\in\textup{FL}(\mathcal{C})\cap\textup{PL}(\mathcal{C})$.

  2. 2.

Every $\mathcal{C}$-orbit for $\alpha$ is $\mathrel{\mathscr{J}}$-trivial.

Recall that given a regular language $L\subseteq A^{*}$ as input, its
syntactic morphism $\alpha:A^{*}\to M$ can be computed. Moreover, Lemma 3.3
implies that all $\mathcal{C}$-orbits for $\alpha$ can be computed when
$\mathcal{C}$-separation is decidable. Thus, the three above characterizations
yield the following corollary.

######  Corollary 6.10.

Let $\mathcal{C}$ be a prevariety with decidable separation. Then, the classes
$\textup{FL}(\mathcal{C})$, $\textup{PL}(\mathcal{C})$ and
$\textup{FL}(\mathcal{C})\cap\textup{PL}(\mathcal{C})$ have decidable
membership.

We prove Theorem 6.7 in the appendix (on the other hand, we omit the proof of
Theorem 6.8, which is symmetrical).

##  7 Conclusion

We presented generic characterizations of the classes
$\textup{TL}(\mathcal{C})$, $\textup{FL}(\mathcal{C})$ and
$\textup{PL}(\mathcal{C})$. While the proofs are complex, the statements are
simple and elegant. They generalize in a natural way all known
characterizations of classes built with these operators. As a corollary, we
obtained that if $\mathcal{C}$ is a prevariety with decidable _separation_ ,
then all classes $\textup{TL}(\mathcal{C})$, $\textup{FL}(\mathcal{C})$ and
$\textup{PL}(\mathcal{C})$ have decidable _membership_.

The next step is to tackle _separation_. This question is difficult in
general, but it is worth looking at _particular_ input classes. For instance,
one can define the TL-hierarchy of basis $\mathcal{C}$: level $0$ is
$\textup{TL}_{0}(\mathcal{C})=\mathcal{C}$ and level $n\geq 1$ is
$\textup{TL}_{n}(\mathcal{C})=\textup{TL}(\textup{TL}_{n-1}(\mathcal{C}))$. It
can be shown that the hierarchies of bases $\textup{ST}=\\{\emptyset,A^{*}\\}$
and $\textup{DD}=\\{\emptyset,\\{\varepsilon\\},A^{+},A^{*}\\}$ are strict.
Thus, since $\textup{BPol}(\mathcal{C})\subseteq\textup{TL}(\mathcal{C})$,
they both classify the star-free languages (or equivalently the languages
definable in full linear temporal logic). We already know that in both
hierarchies, membership is decidable for levels 1 (_i.e._ , the variants TL
and TLX of unary temporal logic) and 2 (which were studied in [15]). The
results of the present paper show that if $\textup{TL}_{2}(\textup{ST})$ and
$\textup{TL}_{2}(\textup{DD})$ have decidable separation, then
$\textup{TL}_{3}(\textup{ST})$ and $\textup{TL}_{3}(\textup{DD})$ would have
decidable membership.

Finally, all other major operators have language-theoretic counterparts.
Another possible follow-up is to look for such a definition for all three
operators
$\mathcal{C}\mapsto\textup{TL}(\mathcal{C}),\textup{FL}(\mathcal{C})$ and
$\textup{PL}(\mathcal{C})$.

## References

  * [1] Mustapha Arfi.  Polynomial operations on rational languages.  In Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science, STACS’87, Lecture Notes in Computer Science, pages 198–206. Springer, 1987.
  * [2] David A. Mix Barrington, Kevin Compton, Howard Straubing, and Denis Thérien.  Regular languages in $\textup{NC}^{1}$.  Journal of Computer and System Sciences, 44(3):478 – 499, 1992\.
  * [3] Danièle Beauquier and Jean-Éric Pin.  Languages and scanners.  Theoretical Computer Science, 84(1):3–21, 1991.
  * [4] Janusz A. Brzozowski and Imre Simon.  Characterizations of locally testable events.  Discrete Mathematics, 4(3):243–271, 1973.
  * [5] Luc Dartois and Charles Paperman.  Two-variable first order logic with modular predicates over words.  In Proceedings of the 30th International Symposium on Theoretical Aspects of Computer Science, STACS’13, Leibniz International Proceedings in Informatics (LIPIcs), pages 329–340. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2013.
  * [6] Volker Diekert, Paul Gastin, and Manfred Kufleitner.  A survey on small fragments of first-order logic over finite words.  International Journal of Foundations of Computer Science, 19(3):513–548, 2008.
  * [7] Volker Diekert, Martin Horsch, and Manfred Kufleitner.  On first-order fragments for Mazurkiewicz traces.  Fundamenta Informaticae, 80(1-3):1–29, 2007.
  * [8] Volker Diekert and Manfred Kufleitner.  Fragments of first-order logic over infinite words.  Theory of Computing Systems (ToCS), 48(3):486–516, 2011.
  * [9] Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke.  First-order logic with two variables and unary temporal logic.  Information and Computation, 179(2):279–295, 2002.
  * [10] James Alexander Green.  On the structure of semigroups.  Annals of Mathematics, 54(1):163–172, 1951.
  * [11] Hans W. Kamp.  Tense Logic and the Theory of Linear Order.  Phd thesis, Computer Science Department, University of California at Los Angeles, USA, 1968.
  * [12] Robert Knast.  A semigroup characterization of dot-depth one languages.  RAIRO - Theoretical Informatics and Applications, 17(4):321–330, 1983.
  * [13] Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, and Howard Straubing.  Two-variable logic with a between relation.  In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’16, pages 106–115, 2016.
  * [14] Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, and Howard Straubing.  An algebraic decision procedure for two-variable logic with a between relation.  In 27th EACSL Annual Conference on Computer Science Logic, CSL’18, Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2018.
  * [15] Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, and Howard Straubing.  Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership.  Logical Methods in Computer Science, Volume 16, Issue 3, 2020\.
  * [16] Robert McNaughton and Seymour A. Papert.  Counter-Free Automata.  MIT Press, 1971.
  * [17] Jean-Éric Pin.  Varieties of Formal Languages.  North Oxford Academic, 1986.
  * [18] Jean-Éric Pin and Pascal Weil.  Polynomial closure and unambiguous product.  Theory of Computing Systems, 30(4):383–422, 1997.
  * [19] Jean-Éric Pin.  An explicit formula for the intersection of two polynomials of regular languages.  In Proceedings of the 17th International Conference on Developments in Language Theory, DLT’13, volume 7907 of Lecture Notes in Computer Science, pages 31–45. Springer, 2013.
  * [20] Jean-Éric Pin.  Mathematical foundations of automata theory.  Lecture notes, in preparation, 2022.  URL: https://www.irif.fr/~jep/PDF/MPRI/MPRI.pdf.
  * [21] Thomas Place.  The amazing mixed polynomial closure and its applications to two-variable first-order logic.  In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’22, 2022.
  * [22] Thomas Place and Marc Zeitoun.  Separating without any ambiguity.  In 45th International Colloquium on Automata, Languages, and Programming, ICALP’18, Leibniz International Proceedings in Informatics (LIPIcs), pages 137:1–137:14. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2018.
  * [23] 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.
  * [24] Thomas Place and Marc Zeitoun.  Going higher in first-order quantifier alternation hierarchies on words.  Journal of the ACM, 66(2):12:1–12:65, 2019.
  * [25] Thomas Place and Marc Zeitoun.  On all things star-free.  In Proceedings of the 46th International Colloquium on Automata, Languages, and Programming, ICALP’19, Leibniz International Proceedings in Informatics (LIPIcs), pages 126:1–126:14. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2019.
  * [26] Thomas Place and Marc Zeitoun.  How many times do you need to go back to the future in unary temporal logic?  In Proceedings of the 15th Latin American Symposium on Theoretical Informatics, LATIN’22, Lecture Notes in Computer Science. Springer, 2022.
  * [27] Thomas Place and Marc Zeitoun.  All about unambiguous polynomial closure.  To appear in TheoretiCS, 2023.  doi:10.48550/arxiv.2205.12703.
  * [28] Thomas Place and Marc Zeitoun.  Closing star-free closure, 2023.  arXiv:2307.09376.
  * [29] Thomas Place and Marc Zeitoun.  A generic characterization of generalized unary temporal logic and two-variable first-order logic.  In 32nd EACSL Annual Conference on Computer Science Logic, CSL’24, Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1–6:22. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2024.
  * [30] Marcel Paul Schützenberger.  On finite monoids having only trivial subgroups.  Information and Control, 8(2):190–194, 1965.
  * [31] Marcel Paul Schützenberger.  Sur certaines opérations de fermeture dans les langages rationnels.  Symposia Mathematica, XV:245–253, 1975.
  * [32] Marcel Paul Schützenberger.  Sur le produit de concaténation non ambigu.  Semigroup Forum, 13:47–75, 1976.
  * [33] Imre Simon.  Piecewise testable events.  In Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, pages 214–222. Springer, 1975.
  * [34] Howard Straubing.  Aperiodic homomorphisms and the concatenation product of recognizable sets.  Journal of Pure and Applied Algebra, 15(3):319 – 327, 1979.
  * [35] Pascal Tesson and Denis Thérien.  Diamonds are forever: The variety DA.  In Semigroups, Algorithms, Automata and Languages, pages 475–500. World Scientific, 2002.
  * [36] Denis Thérien and Thomas Wilke.  Over words, two variables are as powerful as one quantifier alternation.  In Proceedings of the 30th Annual ACM Symposium on Theory of Computing, STOC’98, pages 234–240. ACM, 1998.

##  Appendix A Appendix to Section 6

This appendix is devoted to the proof of Theorem 6.7 (on the other hand, we do
not prove Theorem 6.8, since it is symmetrical). The proof involves some
preliminary work because we have to adapt the results that we presented for
the classes $\textup{TL}(\mathcal{C})$ in Section 4 to the classes
$\textup{FL}(\mathcal{C})$. More precisely, we first prove a characteristic
property of the classes $\textup{FL}(\mathcal{C})$ in Section A.1. Section 6.1
is devoted to results that serve as replacements for Theorems 4.4 and 4.5.
Finally, the characterization of $\textup{FL}(\mathcal{C})$ is presented in
Section A.2.

###  A.1 Characteristic property of the classes $\textup{FL}(\mathcal{C})$

We associate canonical equivalences to the classes $\textup{FL}(\mathcal{C})$
where $\mathcal{C}$ is a prevariety. The definition is taken from [26] and is
similar to those defined for the classes $\textup{TL}(\mathcal{C})$. In
particular, recall that given a morphism $\eta:A^{*}\to N$ into a finite
monoid $N$, we write $\mathcal{C}_{\eta}$ for the class of all languages
recognized by $\eta$. We also reuse the notion of rank that we defined for
temporal formulas in Section 5.

Consider a morphism $\eta:A^{*}\to N$ into a finite monoid and $k\in{\rm
Nature}$. Let $\eta:A^{*}\to N$ Given $w,w^{\prime}\in A^{*}$,
$i\in\textup{{Pos}}(w)$ and $i^{\prime}\in\textup{{Pos}}(w^{\prime})$, we
write, $w,i\blacktriangleright_{\eta,k}w^{\prime},i^{\prime}$ when:

$\text{For every $\textup{FL}[\mathcal{C}_{\eta}]$ formula $\varphi$ with rank
at most $k$,}\quad w,i\models\varphi\Longleftrightarrow
w^{\prime},i^{\prime}\models\varphi.$

The relations $\blacktriangleright_{\eta,k}$ are equivalences. It is also
immediate from the definition and Lemma 5.10, that they have finite index.
Finally, we also introduce equivalences which compare single words of $A^{*}$.
Abusing terminology, we also write them $\blacktriangleright_{\eta,k}$. Given
$w,w^{\prime}\in A^{*}$, we write $w\blacktriangleright_{\eta,k}w^{\prime}$ if
$w,0\blacktriangleright_{\eta,k}w^{\prime},0$. Clearly, the relation
$\blacktriangleright_{\eta,k}$ is an equivalence relation over $A^{*}$. We use
it to characterize the classes $\textup{FL}(\mathcal{C})$ when the class
$\mathcal{C}$ is a _prevariety_. More precisely, we have the following lemma
whose proof is identical to that of Lemma 5.11.

######  Lemma A.1.

Let $\mathcal{C}$ be a prevariety and $L\subseteq A^{*}$. Then,
$L\in\textup{FL}(\mathcal{C})$ if and only if there exists a
$\mathcal{C}$-morphism $\eta:A^{*}\to N$ and $k\in{\rm Nature}$ such that $L$
is a union of $\blacktriangleright_{\eta,k}$-classes.

We now present a few key lemmas that we shall use to prove the characteristic
property of the classes $\textup{FL}(\mathcal{C})$. The first one states that
the equivalences $\blacktriangleright_{\eta,k}$ are congruences. This can be
verified from the definition.

######  Lemma A.2.

Consider a morphism $\eta:A^{*}\to N$ into a finite monoid and $k\in{\rm
Nature}$. For every $u,v,u^{\prime},v^{\prime}\in A^{*}$ such that
$u\blacktriangleright_{\eta,k}u^{\prime}$ and
$v\blacktriangleright_{\eta,k}v^{\prime}$, we have
$uv\blacktriangleright_{\eta,k}u^{\prime}v^{\prime}$.

Moreover, we have the following useful lemma, which involves auxiliary
alphabets. It can also be verified from the definitions.

######  Lemma A.3.

Let $A,B$ be two alphabets and let $\gamma:B^{*}\to A^{*}$ be a morphism. Let
$\eta:A^{*}\to N$ be a morphism into a finite monoid and let
$\delta=\eta\circ\gamma:B^{*}\to N$. For all $w,w^{\prime}\in B^{*}$ and
$k\in{\rm Nature}$ such that $w\blacktriangleright_{\delta,k}w^{\prime}$, we
have $\gamma(w)\blacktriangleright_{\eta,k}\gamma(w^{\prime})$.

Finally, we adapt Proposition 5.13 to the equivalences
$\blacktriangleright_{\eta,k}$.

######  Proposition A.4.

Consider a morphism $\eta:A^{*}\to N$ into a finite monoid, let $e\in E(N)$ be
an idempotent and let $u,v,z\in\eta^{-1}(e)$. For every $k\in{\rm Nature}$,
the following property holds:

$(z^{k}uz^{2k}vz^{k})^{k}\blacktriangleright_{\eta,k}z^{k}vz^{k}(z^{k}uz^{2k}vz^{k})^{k}.$

######  Proof A.5.

Note first that proving the property boils down to the special case when $u,v$
and $z$ are single letter words. Indeed, let $B=\\{a,b,c\\}$ and consider the
morphism $\gamma:B^{*}\to A^{*}$ defined by $\gamma(a)=u$, $\gamma(b)=v$ and
$\gamma(c)=z$. Moreover, let $\delta=\eta\circ\alpha:B^{*}\to N$. We prove
that
$(c^{k}ac^{2k}bc^{k})^{k}\blacktriangleright_{\delta,k}c^{k}bc^{k}(c^{k}ac^{2k}bc^{k})^{k}$.
It will then follow from Lemma A.3 that
$(z^{k}uz^{2k}vz^{k})^{k}\blacktriangleright_{\eta,k}z^{k}vz^{k}(z^{k}uz^{2k}vz^{k})^{k}$,
which will conclude the proof.

We use induction to prove a stronger property. Let us start with a preliminary
definition. Let $w,w^{\prime}\in B^{*}$, $i\in\textup{{Pos}}(w)$,
$i^{\prime}\in\textup{{Pos}}(w^{\prime})$ and $\ell\in{\rm Nature}$ we write
$w,i\sim_{\ell}w^{\prime},i^{\prime}$ if and only if one the two following
conditions is satisfied.

  1. 1.

$|w|+1-i=|w^{\prime}|+1-i^{\prime}$, $w[i]=w^{\prime}[i^{\prime}]$ and, if
$i<|w|+1$, $w{i}=w^{\prime}{i^{\prime}}$.

  2. 2.

$i<|w|+1-\ell$, $i^{\prime}<|w^{\prime}|+1-\ell$,
$w[i]=w^{\prime}[i^{\prime}]$ and
$w(i,i+\ell)=w^{\prime}(i^{\prime},i^{\prime}+\ell)$.

We can now present the general property that we shall prove by induction. We
write $x=c^{k}ac^{k}$ and $y=c^{k}bc^{k}$ for the proof. Let $\ell\in{\rm
Nature}$ and consider a quadruple $(w,i,w^{\prime},i^{\prime})$ where
$w,w^{\prime}\in A^{*}$, $i\in\textup{{Pos}}(w)$ and
$i^{\prime}\in\textup{{Pos}}(w^{\prime})$. We say that
$(w,i,w^{\prime},i^{\prime})$ is an _$\ell$ -candidate_ if there exist
$m\geq\ell$ and $w_{1},w^{\prime}_{1}\in(x+y)^{*}$ such that
$w=w_{1}(xy)^{m}$, $w^{\prime}=w^{\prime}_{1}(xy)^{m}$, $i\leq|w_{1}|$,
$i^{\prime}\leq|w^{\prime}_{1}|$ and $w,i\sim_{\ell}w^{\prime},i^{\prime}$.

######  Lemma A.6.

For every $\ell\leq k$, every $\ell$-candidate $(w,i,w^{\prime},i^{\prime})$
and every formula $\varphi\in\textup{FL}[\mathcal{C}_{\delta}]$ of rank at
most $\ell$, we have $w,i\models\varphi\Leftrightarrow
w^{\prime},i^{\prime}\models\varphi$.

Let us first apply Lemma A.6 to complete the main proof. Clearly,
$((xy)^{k},0,y(xy)^{k},0)$ is a $k$-candidate (recall that both $x$ and $y$
start with the prefix $c^{k}$). Hence, the lemma implies that for all
$\varphi\in\textup{FL}[\mathcal{C}_{\delta}]$ of rank at most $k$, we have
$(xy)^{k},0\models\varphi\Leftrightarrow y(xy)^{k},0\models\varphi$. This
exactly says that
$(c^{k}ac^{2k}bc^{k})^{k}\blacktriangleright_{\delta,k}c^{k}bc^{k}(c^{k}ac^{2k}bc^{k})^{k}$
which completes the main proof.

We now concentrate on the proof of Lemma A.6. We fix $\ell\leq k$, an
$\ell$-candidate $(w,i,w^{\prime},i^{\prime})$ and a formula
$\varphi\in\textup{FL}[\mathcal{C}_{\delta}]$ of rank at most $\ell$ for the
proof. We use induction on the size of $\varphi$ to prove that
$w,i\models\varphi\Leftrightarrow w^{\prime},i^{\prime}\models\varphi$. Assume
first that $\varphi$ is an atomic formula. Since $(w,i,w^{\prime},i^{\prime})$
is an $\ell$-candidate, we have $w,i\sim_{\ell}w^{\prime},i^{\prime}$, which
yields $w[i]=w^{\prime}[i^{\prime}]$. Hence, $w,i\models\varphi\Leftrightarrow
w^{\prime},i^{\prime}\models\varphi$ since $\varphi$ is atomic. Boolean
connectives are handled in the natural way using induction on the size of
$\varphi$. It remains to handle the case when
$\varphi=\mbox{$\textup{F}_{L}\,\psi$}$ for $L\in\mathcal{C}_{\delta}$ and
$\psi\in\textup{FL}[\mathcal{C}_{\delta}]$ has rank at most $\ell-1$. By
symmetry, we only prove that $w,i\models\varphi\Rightarrow
w^{\prime},i^{\prime}\models\varphi$. Hence, we assume that
$w,i\models\varphi$. By hypothesis on $\varphi$, this yields
$j\in\textup{{Pos}}(w)$ such that $i<j$, $w(i,j)\in L$ and $w,j\models\psi$.
We use $j\in\textup{{Pos}}(w)$ to construct a position
$j^{\prime}\in\textup{{Pos}}(w^{\prime})$ such that $i^{\prime}<j^{\prime}$,
$\delta(w(i^{\prime},j^{\prime}))=\delta(w(i,j))$ (which yields
$w(i^{\prime},j^{\prime})\in L$ since $L$ is recognized by $\delta$) and
$w^{\prime},j^{\prime}\models\psi$. This will imply that
$w^{\prime},i^{\prime}\models\varphi$, as desired. Since
$(w,i,w^{\prime},i^{\prime})$ is an $\ell$-candidate, we have $m\geq\ell$ and
$w_{1},w^{\prime}_{1}\in(x+y)^{*}$ such that $w=w_{1}(xy)^{m}$,
$w^{\prime}=w^{\prime}_{1}(xy)^{m}$, $i\leq|w_{1}|$,
$i^{\prime}\leq|w^{\prime}_{1}|$ and $w,i\sim_{\ell}w^{\prime},i^{\prime}$. We
consider three cases depending on the position $j\in\textup{{Pos}}(w)$.

First case: $i+1=j$. We define $j^{\prime}=i^{\prime}+1$. Clearly,
$i^{\prime}<j^{\prime}$ and
$w^{\prime}(j^{\prime},i^{\prime})=w(j,i)=\varepsilon$. Hence, we have to
verify that $w^{\prime},j^{\prime}\models\psi$. Since $\psi$ has rank at most
$\ell-1$ and $w,j\models\psi$, it suffices to prove that
$(w,j,w^{\prime},j^{\prime})$ is an $(\ell-1)$-candidate. It will then follow
from induction that $w^{\prime},j^{\prime}\models\psi$. Since $m\geq\ell$, we
have $m-1\geq\ell-1$. Moreover, we have $w=w_{1}xy(xy)^{m-1}$ and
$w^{\prime}=w^{\prime}_{1}xy(xy)^{m-1}$. Since $j^{\prime}=i+1$,
$j^{\prime}=i^{\prime}+1$, $i\leq|w_{1}|$ and
$i^{\prime}\leq|w^{\prime}_{1}|$, we have $j\leq|w_{1}xy|$ and
$j^{\prime}\leq|w^{\prime}_{1}xy|$. Finally, since
$w,i\sim_{\ell}w^{\prime},i^{\prime}$, $j=i+1$ and $j^{\prime}=i^{\prime}+1$,
one can verify that $w,j\sim_{\ell-1}w^{\prime},j^{\prime}$. Thus,
$(w,j,w^{\prime},j^{\prime})$ is indeed an $(\ell-1)$-candidate.

Second case: $i+1<j$ and $j\leq|w_{1}xy|$. We know that
$i^{\prime}\leq|w^{\prime}_{1}|$. Hence, by definition of $x,y$ and since
$\ell\leq k$, one can check that there exists
$j^{\prime}\in\textup{{Pos}}(w^{\prime})$ such that
$j^{\prime}\leq|w^{\prime}_{1}xy|$, $i^{\prime}+1<j^{\prime}$ and
$w,j\sim_{\ell-1}w^{\prime},j^{\prime}$. We have $i^{\prime}<j^{\prime}$ by
definition. Moreover, since $i+1<j$ and $i^{\prime}+1<j^{\prime}$, we know
that $w^{\prime}(i^{\prime},j^{\prime})$ and $w(i,j)$ are nonempty, which
yields $\delta(w^{\prime}(i^{\prime},j^{\prime}))=\delta(w(i,j))$ by
definition of $\delta$. Finally, it is immediate that
$(w,j,w^{\prime},j^{\prime})$ is an $(\ell-1)$-candidate. Indeed, we have
$w=w_{1}xy(xy)^{m-1}$, $w^{\prime}=w^{\prime}_{1}xy(xy)^{m-1}$,
$j\leq|w_{1}xy|$, $j^{\prime}\leq|w^{\prime}_{1}xy|$ and
$w,j\sim_{\ell-1}w^{\prime},j^{\prime}$. Thus, since $w,j\models\psi$,
induction yields $w^{\prime},j^{\prime}\models\psi$ which completes this case.

Third case: $i+1<j$ and $|w_{1}xy|<j$. In this case, $j$ is inside the suffix
$(xy)^{m-1}$ of $w=w_{1}(xy)^{m}$. We define
$j^{\prime}\in\textup{{Pos}}(w^{\prime})$ as the corresponding position in the
suffix $(xy)^{m-1}$ of $w^{\prime}=w^{\prime}_{1}(xy)^{m}$ (_i.e._ ,
$j^{\prime}=j+|w^{\prime}|-|w|$). Since $i^{\prime}\leq|w_{1}|$, it is clear
that $i^{\prime}<j^{\prime}$. In fact, we have $i^{\prime}+1<j^{\prime}$ which
means that $w^{\prime}(i^{\prime},j^{\prime})$ and $w(i,j)$ are nonempty. This
yields $\delta(w^{\prime}(j^{\prime},i^{\prime}))=\delta(w(j,i))$ by
definition of $\delta$. Finally, we have $w{j}=w^{\prime}{j^{\prime}}$ by
definition of $j^{\prime}$. Hence, since
$\psi\in\textup{FL}[\mathcal{C}_{\delta}]$ (and therefore only contains future
modalities), we get $w^{\prime},j^{\prime}\models\psi$ since we already know
that $w,j\models\psi$. This completes the proof.

We are ready to prove the characteristic property of the classes
$\textup{FL}(\mathcal{C})$. It is a simple corollary of Proposition A.4.

######  Proposition A.7.

Let $\mathcal{C}$ be a prevariety and $L\in\textup{FL}(\mathcal{C})$. There
exists a $\mathcal{C}$-morphism $\eta:A^{*}\to N$ and $k\in{\rm Nature}$ such
that for every idempotent $f\in E(N)$, every $u,v,z\in\eta^{-1}(f)$ and every
$x,y\in A^{*}$, the following property holds:

$x(z^{k}uz^{2k}vz^{k})^{k}y\in L\quad\text{if and only if}\quad
xz^{k}vz^{k}(z^{k}uz^{2k}vz^{k})^{k}y\in L.$

######  Proof A.8.

Lemma A.1 yields a $\mathcal{C}$-morphism $\eta:A^{*}\to N$ and $k\in{\rm
Nature}$ such that $L$ is a union of $\blacktriangleright_{\eta,k}$-classes.
Now, consider $u,v,z\in A^{*}$ such that $\eta(u)=\eta(v)=\eta(z)\in E(N)$ and
$x,y\in A^{*}$. We have to prove that,

$x(z^{k}uz^{2k}vz^{k})^{k}y\in L\quad\text{if and only if}\quad
xz^{k}vz^{k}(z^{k}uz^{2k}vz^{k})^{k}y\in L.$

It is immediate from Lemma A.2 and Proposition A.4 that,

$x(z^{k}uz^{2k}vz^{k})^{k}y\blacktriangleright_{\eta,k}xz^{k}vz^{k}(z^{k}uz^{2k}vz^{k})^{k}y.$

Since $L$ is a union of $\blacktriangleright_{\eta,k}$-classes, the desired
result follows.

###  A.2 Proof of Theorem 6.7

Let us first recall the statement of Theorem 6.7.

See 6.7

Fix a prevariety $\mathcal{C}$, a regular language $L\subseteq A^{*}$ and its
syntactic morphism $\alpha:A^{*}\to M$ for the proof. We start with the left
to right implication, which follows directly from Proposition A.7.

From $\textup{FL}(\mathcal{C})$ to $\mathrel{\mathscr{L}}$-triviality. Assume
that $L\in\textup{FL}(\mathcal{C})$. For every $e\in E(M)$, we prove that the
$\mathcal{C}$-orbit $M_{e}$ of $e$ for $\alpha$ is
$\mathrel{\mathscr{L}}$-trivial. We fix $e$ for the proof. Let $s,t\in M_{e}$,
we have to show that $t(st)^{\omega}=(st)^{\omega}$. Since
$L\in\textup{FL}(\mathcal{C})$, Proposition A.7 yields a
$\mathcal{C}$-morphism $\eta:A^{*}\to N$ and $k\in{\rm Nature}$ such that for
every $f\in E(N)$, every $u,v,z\in\eta^{-1}(f)$ and every $x,y\in A^{*}$, we
have,

$x(z^{k}uz^{2k}vz^{k})^{k}y\in L\quad\Leftrightarrow\quad
xz^{k}vz^{k}(z^{k}uz^{2k}vz^{k})^{k}y\in L.$ (6)

Since $\eta$ is a $\mathcal{C}$-morphism, Lemma 3.4 yields $f\\!\in\\!E(N)$
such that $M_{e}\\!\subseteq\\!\alpha(\eta^{-1}(f))$. As $e,s,t\in M_{e}$, we
get $u,v,z\in A^{*}$ such that $u,v,z\in\eta^{-1}(f)$, $\alpha(u)=s$,
$\alpha(v)=t$ and $\alpha(z)=e$. Thus, the words $u,v,z\in A^{*}$ satisfy (6)
and the words $(z^{k}uz^{k}vz^{k})^{k}$ and
$z^{k}vz^{k}(z^{k}uz^{k}vz^{k})^{k}$ are equivalent for the syntactic
congruence of $L$. Hence, they have the same image under $\alpha$. Since $e\in
E(M)$, this yields $(esete)^{k}=ete(esete)^{k}$. Hence, $(st)^{k}=t(st)^{k}$
since $e,s,t\in M_{e}$ and $e$ is neutral in $M_{e}$ by Lemma 3.2. It now
suffices to multiply by enough copies of $st$ the right to get
$(st)^{\omega}=t(st)^{\omega}$, which completes the proof.

From $\mathrel{\mathscr{L}}$-triviality to $\textup{FL}(\mathcal{C})$.
Assuming that every $\mathcal{C}$-orbit for $\alpha$ is
$\mathrel{\mathscr{L}}$-trivial, we show $L\in\textup{FL}(\mathcal{C})$. We
use induction to build a $\textup{FL}(\mathcal{C})$ formula defining $L$. The
proof is similar to that of the corresponding implication in Theorem 5.1. We
start with preliminary terminology.

Lemma 3.1 yields a $\mathcal{C}$-morphism $\eta:A^{*}\to N$ such that the
$\mathcal{C}$-pairs for $\alpha$ are exactly the $\eta$-pairs for $\alpha$. We
fix $\eta$ for the proof. We define an auxiliary alphabet $B$. Let $P\subseteq
M\times N$ be the set of all pairs $(\alpha(w),\eta(w))\in M\times N$ where
$w\in A^{+}$ is a nonempty word. For each pair $(s,r)\in P$, we create a fresh
letter $b_{s,r}\not\in A$ and define $B=\\{b_{s,r}\mid(s,r)\in P\\}$.

Let $\beta:B^{*}\to M$ and $\delta:B^{*}\to N$ be the morphisms defined by
$\beta(b_{s,r})=s$ and $\delta(b_{s,r})=r$ for $(s,r)\in P$. By definition, it
remains true that for every $w\in B^{+}$, we have $(\beta(w),\delta(w))\in P$.
Let $\mathcal{C}_{\delta}$ be the class of all languages (over $B$) recognized
by $\delta$. One can check that $\mathcal{C}_{\delta}$ is a prevariety. We