similar result exists for BPol($C$) [18], it requires going beyond separation, and is, above all, significantly more complex.

**Navigational hierarchies.** In this paper, we adopt a different point of view: to get insight on concatenation hierarchies, we study an alternate, yet closely related classification of the star-free closure SF($C$) of a class $C$. This new kind of hierarchy is called the *navigational hierarchy*. It draws inspiration from another renowned type of class of languages: those based on two-variable first-order logic and/or temporal logic [19], [20], [21], [22], [23], [24], [25], [26], [27], [28]. Its construction is similar to concatenation hierarchies: one replaces the operator $C \mapsto \text{BPol}(C)$ by an operator $C \mapsto \text{TL}(C)$ based on unary temporal logic. The class TL($C$) consists of all languages definable in a variant of *unary temporal logic* with future/past modalities built from $C$. It is defined as follows: each language in $C$ gives rise to a future modality $F_L$ and a past one $P_L$ generalizing the classic ones F and P. For instance, $F_L \varphi$ holds at position $i$ in a word $w$ if there is a position $j > i$ such that $\varphi$ holds at $j$ in $w$, and the infix of $w$ between $i$ and $j$ belongs to $L$. The operator $C \mapsto \text{TL}(C)$ seems to have more robust properties than BPol. In particular, we have a transfer result: TL($C$)-membership reduces to $C$-separation [29].

One denotes level $n$ in the navigational hierarchy of basis $C$ by $TL_n(C)$. The union of all levels remains the star-free closure of $C$, so that the navigational and concatenation hierarchies stratify the same class: SF($C$). Level one in the navigational hierarchy of basis ST = $\{\emptyset, A^*\}$ is the standard class of languages definable in *unary temporal logic* TL with the F and P modalities. Results of [30], [31], [23], [22] underscore its multiple characterizations: it consists of languages definable in two-variable first-order logic FO$^2$(<), corresponds also to the “intermediate level” $\Delta_2$(<), is the class of unambiguous languages and has a nice decidable algebraic characterization. Level one in the navigational hierarchy of basis DD = $ST^+$ is also standard: it is the class of languages definable in *unary temporal logic with between predicates*, where the link with temporal logic is also observed and considered.

**Contributions.** We carry out a general study of navigational hierarchies. We first briefly compare them with concatenation hierarchies: we show that $\text{BPol}_n(C) \subseteq \text{TL}_n(C)$ for all $n \in \mathbb{N}$ for any class $C$. Moreover, as announced above, we prove that both kinds of hierarchies classify the star-free closure of $C$.

The remainder of the paper focuses on specific bases of the form $G$ or $G^+$, where $G$ represents a class of group languages (using the basis $G^+$ instead of $G$ boils down to adding the standard “next” and “yesterday” modalities). Group languages are those recognized by a complete, deterministic and co-deterministic automaton [9]. Bases made of group languages are natural in our context. Indeed, if the basis includes no group language other than $\emptyset$ and $A^*$, then each level of the concatenation or navigational hierarchy of basis $C$ is a subclass

of SF. Thus, extending beyond star-free languages requires bases containing nontrivial group languages.

We first prove that for any class of group languages $G$, the navigational hierarchies of bases $G$ and $G^+$ are both strict and that they are strictly intertwined (if the alphabet has at least two letters). As a byproduct, we reprove the same property for concatenation hierarchies. We next sharpen the comparison between both types of hierarchies: we show that if $C = G$ or $C = G^+$, the class $\text{TL}_2(C)$ is incomparable with any level above three of the concatenation hierarchy of basis $C$. The situation is depicted in Fig. 1.

**Remark 1.** Separation is a key tool here: to prove that a language $L$ is not in level $n$ of a hierarchy, it suffices to exhibit a disjoint language $K$ and to show that $L$ and $K$ cannot be separated by this level. This approach significantly simplifies the inductive construction of languages outside each level.

<figure><img src="image_1.png" /><figcaption>Fig. 1: Comparison of the two hierarchies (bases $G$ or $G^+$)</figcaption></figure>

These results generalize those of [26], [28], which already implied that $\text{TL}_2(\text{ST})$ is incomparable with any level above three in the concatenation hierarchy of basis ST. Interestingly, this particular basis requires arbitrarily large alphabets: it is shown in [26], [28] that $\text{TL}_2(\text{ST}) \subseteq \text{BPol}_3(\text{ST})$ when the alphabet is binary. We strengthen this result by showing that $\text{TL}_2(\text{ST}) \subseteq \text{BPol}_{n+1}(\text{ST})$ when the alphabet is of size $n$. Moreover, we prove a surprising result: when the alphabet is *binary*, $\text{TL}_2(\text{ST})$ is exactly the class of languages in $\text{Pol}_3(\text{ST})$ whose complement also belong to $\text{Pol}_3(\text{ST})$ (also written $\Delta_3(\langle)$). This result is reminiscent of a famous theorem of Thérien and Wilke, which states that $\text{TL}_1(\text{ST}) = \Delta_2(\langle)$.

While we need arbitrarily large alphabets when the basis is ST, we show that a binary alphabet suffices for bases of the form $G^+$, or when $G$ includes MOD. In these cases, the classes $\text{TL}_k(C)$ and $\text{BPol}_n(C)$ are incomparable if $2 \le k < n$.

Finally, we prove that membership for both $\text{TL}_2(G)$ and $\text{TL}_2(G^+)$ reduces to $G$-separation, by combining two known transfer results of [32], [29]. This theorem applies for $G = \text{ST}$, MOD and GR as they have decidable separation [33], [34].

In the second part of the paper, we focus on the class $\text{TL}_2(\text{ST})$, proving that it has decidable separation. This result has several interesting implications. First, $\text{TL}_2(\text{ST})$ is notable because it corresponds to *two-variable first-order logic with between predicates* [28], [27], [26]. Second, by combining this result with the theorem of [29], we show that level *three* ($\text{TL}_3(\text{ST})$) has decidable membership. Third, using transfer theorems [35], [36], we lift these results to the basis $\text{DD} = \text{ST}^+$, so that $\text{TL}_2(\text{DD})$ has decidable separation and $\text{TL}_3(\text{DD})$ has decidable membership. Fourth, the separation algorithm itself is significant as it solves a more general problem: $\text{TL}_2(\text{ST})$-covering, which generalizes separation to arbitrarily many input languages [37]. This generalization
is necessary, as no specialized separation algorithm exists. Indeed, the procedure relies on a fixpoint computation and carrying it out requires more information that what is needed to decide separation alone. Notably, we use a covering algorithm for TL(ST$^+$) [35] as a subprocedure.

**Organization.** Section II introduces the notations and definitions, followed by a recall of concatenation hierarchies in Section III. Navigational hierarchies are defined in Section IV. Section V focus on group bases, proving the strictness of their navigational hierarchies and comparing them to concatenation hierarchies. The remaining sections address separation and covering: Section VI presents the framework, and Section VII shows the decidability of covering and separation for TL₂(ST).

## II. PRELIMINARIES

We fix a *finite alphabet* $A$. As usual, $A^*$ is the set of all finite words over $A$, including the empty one $\varepsilon$. A language is a subset of $A^*$. We let $A^+ = A^* \setminus \{\varepsilon\}$. For $u, v \in A^*$, we let $uv$ be the word obtained by concatenating $u$ and $v$. For $K, L \subseteq A^*$, we let $KL = \{uv \mid u \in K \text{ and } v \in L\}$. If $w \in A^*$, we write $|w| \in \mathbb{N}$ for its length. We view a word $w = a_1 \cdots a_{|w|} \in A^*$ as an *ordered set* $\text{Pos}(w) = \{0, \dots, |w| + 1\}$ of $|w| + 2$ *positions*. Position $i \in \{1, \dots, |w|\}$ carries label $a_i \in A$. We write $w[i] = a_i$. Positions 0 and $|w| + 1$ carry no label, and we write $w[0] = \min$ and $w[|w| + 1] = \max$. For $w = a_1 \cdots a_{|w|} \in A^*$ and $i, j \in \text{Pos}(w)$ such that $i < j$, we write $w(i, j) = a_{i+1} \cdots a_{j-1} \in A^*$. In particular, $w(0, |w| + 1) = w$ and $w(i, i + 1) = \varepsilon$ for $0 \le i \le |w|$.

**Classes.** A class of languages is a set of languages. A class $C$ is a *lattice* if $\emptyset \in C$, $A^* \in C$ and $C$ is closed under union and intersection: for all $K, L \in C$, we have $K \cup L \in C$ and $K \cap L \in C$. A Boolean algebra is a lattice $C$ which is also closed under complement: for all $L \in C$, we have $A^* \setminus L \in C$. Finally, $C$ is closed under quotients when for all $L \in C$ and $u \in A^*$, the languages $u^{-1}L = \{v \in A^* \mid uv \in L\}$ and $Lu^{-1} = \{v \in A^* \mid vu \in L\}$ both belong to $C$. A *prevariety* (resp. *positive prevariety*) is a Boolean algebra (resp. lattice) closed under quotients and containing only *regular languages*. Regular languages are those that can be equivalently defined by finite automata or finite monoids. Here, we use the latter.

**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$. A group is a monoid $G$ such that for all $g \in G$, there exists $g^{-1}$ such that $gg^{-1} = g^{-1}g = 1_G$. 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 is a number $\omega(M)$ (written $\omega$ when $M$ is understood) such that $s^\omega$ is idempotent for all $s \in M$.

Note that $A^*$ is a monoid whose multiplication is concatenation (its identity is $\varepsilon$). A morphism is a map $\alpha: A^* \to M$, where $M$ is a monoid, such that $\alpha(uv) = \alpha(u)\alpha(v)$ and $\alpha(\varepsilon) = 1_M$ for all $u, v \in A^*$. A language $L \subseteq A^*$ is *recognized* by a morphism $\alpha: A^* \to M$ if there exists a set $F \subseteq M$ such that $L = \alpha^{-1}(F)$. Every language $L$ is recognized by

a canonical morphism, which we recall. One associates to $L$ an equivalence relation $\equiv_L$ over $A^*$. Given $u, v \in A^*$, we let $u \equiv_L v$ if and only if $xuy \in L \Leftrightarrow xvy \in L$ for all $x, y \in A^*$. One can check that $\equiv_L$ is a congruence on $A^*$, i.e., an equivalence relation compatible with concatenation. Thus, the set of equivalence classes $M_L = A^*/\equiv_L$ is a monoid, called the *syntactic monoid* of $L$. The map $\alpha_L: A^* \to M_L$ that maps every word to its equivalence class is a morphism recognizing $L$, called the *syntactic morphism* of $L$. A language $L$ is regular if and only if $M_L$ is finite: 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$.

**Remark 2.** The only infinite monoids that we consider are of the form $A^*$. From now on, we implicitly assume that every other monoid $M, N, \dots$ appearing in the paper is finite.

**The class AT.** The class AT of *alphabet testable languages* is central in this paper. It consists of all finite Boolean combinations of languages $A^*aA^*$ where $a \in A$. One can check that AT is a prevariety. We associate a morphism to AT. Consider the monoid $2^A$ (the set of all subalphabets of $A$), with union as multiplication. We let $\eta_{\text{AT}}: A^* \to 2^A$ be the morphism defined by $\eta_{\text{AT}}(a) = \{a\}$. That is, $\eta_{\text{AT}}(w) = \{a \in A \mid w \in A^*aA^*\}$ for all $w \in A^*$. One can check that $\eta_{\text{AT}}$ recognizes exactly the languages in AT. We call $\eta_{\text{AT}}$ the *canonical AT-morphism*.

We shall also consider the class LT of *locally testable languages* [38], [39]. It consists of all finite Boolean combinations of languages $A^*wA^*$, $wA^*$ and $A^*w$ where $w \in A^*$ is a word.

**Decision problems.** We are interested in three problems that depend on a parameter class $C$. We use them as tools for analyzing $C$: intuitively, proving their decidability requires a solid understanding of $C$. The simplest one is *C-membership*. Its input is a regular language $L$. It asks whether $L \in C$.

The next problem, *C-separation*, takes two regular languages $L_1, L_2$ as input and asks whether $L_1$ is *C-separable* from $L_2$: does there exist a third language $K \in C$ such that $L_1 \subseteq K$ and $L_2 \cap K = \emptyset$? This generalizes membership: $L \in C$ if and only if it is *C-separable* from its complement (which is also regular). We need the following lemma (proved in Appendix ??): language concatenation preserves non-separability.

**Lemma 1.** Let $L_1, L_2, H_1, H_2 \subseteq A^*$ and let $C$ be a positive prevariety. If $L_1$ is not $C-separable$ from $L_2$ and $H_1$ is not $C-separable$ from $H_2$, then $L_1H_1$ is not $C-separable$ from $L_2H_2$.

Finally, *C-covering* is defined in [37]. For a language $L$, a *C-cover* of $L$ is a *finite* set of languages $\mathbf{K}$ such that all $K \in \mathbf{K}$ belong to $C$ and $L \subseteq \bigcup_{K \in \mathbf{K}} K$. The *C-covering problem* takes as input a pair $(L_1, \mathbf{L}_2)$ where $L_1$ is a regular language and $\mathbf{L}_2$ is a *finite* set of regular languages. It asks whether $(L_1, \mathbf{L}_2)$ is *C-coverable*: does there exist a *C-cover* $\mathbf{K}$ of $L_1$ such that for every $K \in \mathbf{K}$, there exists $L \in \mathbf{L}_2$ satisfying $K \cap L = \emptyset$? This generalizes separation (if $C$ is closed under union): $L_1$ is *C-separable* from $L_2$ if and only if $(L_1, \{L_2\})$ is *C-coverable*.

**The C-pair relation.** In this paper, we characterize certain classes using a binary relation, which we now define. Let $C$
be a class and let $\alpha: A^* \to M$ be a morphism. We say that a pair $(s, t) \in M^2$ is a C-pair when $\alpha^{-1}(s)$ is not C-separable from $\alpha^{-1}(t)$. Clearly, C-pairs can be computed from the morphism $\alpha$ if C-separation is decidable. Typically, C-pairs are used to characterize a class constructed on top of C.

### III. CONCATENATION HIERARCHIES

We briefly recall the definition of standard concatenation hierarchies, which is based on certain operators.

**Operators.** The polynomial closure $\text{Pol}(C)$ of a class $C$ consists of all finite unions of marked products $L_0 a_1 L_1 \cdots a_n L_n$ with $a_1, \dots, a_n \in A$ and $L_0, \dots, L_n \in C$. It is known [40], [41], [11] that if $C$ is positive prevariety, then so is $\text{Pol}(C)$. However, $\text{Pol}(C)$ may not be closed under complement. It is therefore combined with two other operators. First, for every class $D$, we write $\text{co-}D = \{A^* \setminus L \mid L \in D\}$ for the class consisting of all complements of languages in $D$. Moreover, the Boolean closure of a class $D$ is the least Boolean algebra $\text{Bool}(D)$ containing $D$. We write $\text{BPol}(C)$ for $\text{Bool}(\text{Pol}(C))$.

**Hierarchies.** A concatenation hierarchy is built as follows. One starts from an arbitrary class $C$ called its basis. We let $\text{BPol}_0(C) = C$ and for $n > 0$, $\text{BPol}_n(C) = \text{BPol}(\text{BPol}_{n-1}(C))$. Clearly, $\text{BPol}_n(C) \subseteq \text{BPol}_{n+1}(C)$ for all $n \in \mathbb{N}$. Level $n$ in the concatenation hierarchy of basis $C$ is then $\text{BPol}_n(C)$.

It is also standard to consider “intermediary” levels. First, we let $\text{Pol}_0(C) = C$ and $\text{Pol}_n(C) = \text{Pol}(\text{BPol}_{n-1}(C))$ if $n \ge 1$. Next, we let $\text{IPol}_n(C) = \text{Pol}_n(C) \cap \text{co-Pol}_n(C)$ for $n \in \mathbb{N}$ (it is therefore the greatest Boolean algebra contained in $\text{Pol}_n(C)$).

<figure><img src="image_2.png" /><figcaption>Fig. 2: The four kinds of levels in a concatenation hierarchy.</figcaption></figure>

The following standard statement was originally proved in [42] (see also [41], [11] for recent proofs).

**Proposition 2.** Let $C$ be a positive prevariety and $n \in \mathbb{N}$. Then $\text{Pol}_n(C)$ is a positive prevariety. Moreover, $\text{BPol}_n(C)$ and $\text{IPol}_n(C)$ are prevarieties.

For each class $C$, we define $\text{SF}(C) = \bigcup_{n \in \mathbb{N}} \text{BPol}_n(C)$. This union of all levels in the concatenation hierarchy of basis $C$ is the star-free closure of $C$. This is the least class containing $C$ and closed under Boolean operations and marked product.

The first concatenation hierarchy to be introduced was the dot-depth hierarchy of basis $\text{DD} = \{\emptyset, \{\epsilon\}, A^+, A^*\}$. It was defined by Brzozowski and Cohen [4] to classify star-free languages [3]. Most bases in the literature are classes of group languages. These bases will be revisited in Section V.

We complete the presentation with some useful properties. The purpose of the next two lemmas is to prove that a particular language does not belong to a given level. The first is simple and proved in [11, Lemma 33] or [14, Lemma 4.8].

**Lemma 3.** If $C$ is a prevariety, $\text{Pol}_2(C) = \text{Pol}(\text{co-Pol}(C))$.

The second lemma is proved in Appendix ?? as a corollary of a characterization of $\text{Pol}(C)$ given in [11, Theorem 54].

**Lemma 4.** Let $C$ be a positive prevariety. Let $H_1, H_2 \subseteq A^*$ be languages such that $H_1$ is not $C$-separable from $H_2$. Then, $H_1^*$ is not $\text{Pol}(C)$-separable from $H_1^* H_2 H_1^*$.

Finally, we will require the following algebraic characterization of $\text{IPol}_2(C)$. It is proved in [14, Theorem 6.7].

**Theorem 5.** Let $C$ be a positive prevariety. Let $L$ be a regular language and $\alpha: A^* \to M$ be its syntactic morphism. Then, $L \in \text{IPol}_2(C)$ if and only if $\alpha$ satisfies the following property:

$$ (esete)^{w+1} = (esete)^w \text{ete}(esete)^w \quad \text{for all C-pairs } (e, s) \in E(M) \times M \text{ for } \alpha \text{ and all } t \in M \quad (1) $$

### IV. NAVIGATIONAL HIERARCHIES

In this section, we introduce the operator $C \mapsto \text{TL}(C)$ and use it to define navigational hierarchies. Next, we compare these hierarchies with concatenation hierarchies.

#### A. Definition

**The operator.** For each class $C$, we define a set $\text{TL}[C]$ of temporal formulas. They are built inductively from the atomic formulas $\top$, $\bot$, $\min$, $\max$ and “a” for all letters $a \in A$. All Boolean connectives are allowed: if $\psi_1, \psi_2 \in \text{TL}[C]$, then $(\psi_1 \lor \psi_2) \in \text{TL}[C]$, $(\psi_1 \land \psi_2) \in \text{TL}[C]$ and $(-\psi_1) \in \text{TL}[C]$. There are two temporal modalities $F_L$ and $P_L$ for each $L \in C$: if $\psi \in \text{TL}[C]$, then $(F_L \psi) \in \text{TL}[C]$ and $(P_L \psi) \in \text{TL}[C]$. We omit parentheses when there is no ambiguity.

Evaluating a formula $\varphi \in \text{TL}[C]$ requires a word $w \in A^*$ and a position $i \in \text{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]$.

* **Boolean connectives:** $w, i \models \psi_1 \lor \psi_2$ holds if $w, i \models \psi_1$ or $w, i \models \psi_2$, $w, i \models \psi_1 \land \psi_2$ holds if $w, i \models \psi_1$ and $w, i \models \psi_2$, and $w, i \models \neg \psi$ holds if $w, i \models \psi$ does not.

* **Finally:** for $L \in C$, $w, i \models F_L \psi$ holds if there exists $j \in \text{Pos}(w)$ such that $i < j$, $w(i, j) \in L$ and $w, j \models \psi$.

* **Previously:** for $L \in C$, $w, i \models P_L \psi$ holds if there exists $j \in \text{Pos}(w)$ such that $j < i$, $w(j, i) \in L$ and $w, j \models \psi$.

If no distinguished position is specified, we evaluate formulas at the leftmost unlabeled position. For a formula $\varphi \in \text{TL}[C]$, the language defined by $\varphi$ is $L(\varphi) = \{w \in A^* \mid w, 0 \models \varphi\}$.

Finally, given a class $C$, we write $\text{TL}(C)$ for the class consisting of all languages $L(\varphi)$ where $\varphi \in \text{TL}[C]$. Clearly, $C \subseteq \text{TL}(C)$ since $L \in C$ is defined by $F_L \max \in \text{TL}[C]$.

**Remark 3.** It is well-known [22] that the standard variants TL and TLX of unary temporal logic (see Section V) correspond to the variants $\text{FO}^2(\langle\rangle)$ and $\text{FO}^2(\langle\rangle, +1)$ of two-variable first-order logic. This correspondence can be generalized: with a class $C$, we associate a set $\mathbb{I}_C$ of first-order predicates. For each $L \in C$, it contains a binary predicate $I_L(x, y)$, interpreted
as follows: if $w \in A^*$ and $i, j \in \text{Pos}(w)$, then $w \models I_L(i, j)$ if and only if $i < j$ and $w(i, j) \in L$. It is shown in [14] that for every Boolean algebra $C$, we have $\text{TL}(C) = \text{FO}^2(\mathbb{I}_C)$.

We turn to a generic algebraic characterization of the classes $\text{TL}(C)$ from [29, Theorem 12]. It will serve as a central tool.

**Theorem 6.** Let $C$ be a prevariety, let $L \subseteq A^*$ be a regular language and let $\alpha: A^* \to M$ be its syntactic morphism. Then, $L \in \text{TL}(C)$ if and only if $\alpha$ satisfies:

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

In view of Theorem 6, $\text{TL}(C)$-membership reduces to $C$-separation for every prevariety $C$. Indeed, deciding $C$-separation suffices to compute the $C$-pairs, by definition.

**Corollary 7.** Let $C$ be a prevariety. If $C$-separation is decidable, then so is $\text{TL}(C)$-membership.

We will use the next corollary of Theorem 6 (proved in Appendix ??) to show that languages do not belong to $\text{TL}(C)$.

**Lemma 8.** Let $L, U, V \subseteq A^*$, $P = L^*(U L^* V L^*)^*$ and $C$ be a prevariety. If $L$ is not $C$-separable from either $U$ or $V$, then $P$ is not $\text{TL}(C)$-separable from either $PUP$ or $PVP$.

**Navigational hierarchies.** Each such hierarchy is determined by an arbitrary initial class $C$ called its basis. For $n \in \mathbb{N}$, level $n$ is written $\text{TL}_n(C)$. Level zero is the basis $\text{TL}_0(C) = C$. Then, for all $n \ge 1$, we let $\text{TL}_n(C) = \text{TL}(\text{TL}_{n-1}(C))$. Clearly, we have $\text{TL}_n(C) \subseteq \text{TL}_{n+1}(C)$ for all $n \in \mathbb{N}$. The next proposition can be verified using Theorem 6 (see Appendix ?? for details).

**Proposition 9.** Let $C$ be a prevariety. Then, $\text{TL}_n(C)$ is a prevariety as well for all $n \in \mathbb{N}$.

## B. Connection with concatenation hierarchies

We now compare the two kinds of hierarchies. We start with a preliminary easy result.

**Proposition 10.** For every class $C$, $\text{TL}(C) = \text{TL}(\text{Pol}(C))$.

*Proof.* Clearly, $\text{TL}(C) \subseteq \text{TL}(\text{Pol}(C))$ as $C \subseteq \text{Pol}(C)$. For the converse inclusion, we show that the modalities $F_L$ and $P_L$ with $L \in \text{Pol}(C)$ can be simulated using only modalities $F_K$ and $P_K$ with $K \in C$. By symmetry, we only consider the former. For all $\varphi \in \text{TL}[C]$, we build $\langle\varphi\rangle_L \in \text{TL}[C]$ such that for all $w \in A^*$ and $i \in \text{Pos}(w)$, $w, i \models \langle\varphi\rangle_L \Leftrightarrow w, i \models F_L \varphi$.

By definition of $\text{Pol}(C)$, $L \in \text{Pol}(C)$ is built from the languages in $C$ using union and marked product. We perform an induction on this construction. If $L \in C$, it suffices to define $\langle\varphi\rangle_L = F_L \varphi$, which is a $\text{TL}[C]$ formula. If $L = L_0 \cup L_1$ with $L_0, L_1 \in \text{Pol}(C)$, we let $\langle\varphi\rangle_L = \langle\varphi\rangle_{L_0} \lor \langle\varphi\rangle_{L_1}$. Finally, if $L = L_0 a L_1$ with $L_0, L_1 \in \text{Pol}(C)$ and $a \in A$, we let $\langle\varphi\rangle_L = \langle a \land \langle\psi\rangle_{L_1}\rangle_{L_0}$. This completes the proof. □

We complete Proposition 10 with the following corollary.

**Corollary 11.** For any class $C$ and $n \in \mathbb{N}$, $\text{BPol}_n(C) \subseteq \text{TL}_n(C)$.

*Proof.* We show the inclusion $\text{BPol}(D) \subseteq \text{TL}(D)$ for every class $D$. The statement will then follow by induction. Since $\text{TL}(D) = \text{TL}(\text{Pol}(D))$ by Proposition 10, it is immediate that $\text{Pol}(D) \subseteq \text{TL}(D)$. Therefore, $\text{BPol}(D) \subseteq \text{Bool}(\text{TL}(D))$. Finally, since $\text{TL}(D)$ is a Boolean algebra by definition, we have $\text{Bool}(\text{TL}(D)) = \text{TL}(D)$, completing the proof. □

**Remark 4.** If $C$ is a positive prevariety, one can strengthen Corollary 11: one can show $\text{IPol}_{n+1}(C) \subseteq \text{TL}_n(C)$ from the characterizations of $\text{IPol}_2(C)$ and $\text{TL}(C)$ (Theorems 5 and 6).

In general, the converse inclusion $\text{TL}_n(C) \subseteq \text{BPol}_n(C)$ fails. For instance, it is shown in [28] that for the basis $\text{AT}$, level one, $\text{TL}(\text{AT})$, already intersects all levels $\text{BPol}_n(\text{AT})$. However, the union of all levels is the same: the star-free closure. Indeed, since $\text{SF}(\text{SF}(C)) = \text{SF}(C)$ for every $C$, it suffices to show that $\text{TL}(C) \subseteq \text{SF}(C)$. This follows from known results. As mentioned in Remark 3, it is shown in [14, Theorem 9.9] that for every Boolean algebra $C$, we have $\text{TL}(C) = \text{FO}^2(\mathbb{I}_C)$ where $\text{FO}^2(\mathbb{I}_C)$ is two-variable first-order logic equipped with a set of predicates built from $C$. Clearly, $\text{FO}^2(\mathbb{I}_C) \subseteq \text{FO}(\mathbb{I}_C)$ (with FO as full first-order logic). Finally, it is shown in [11, Theorem 73] that $\text{SF}(C) = \text{FO}(\mathbb{I}_C)$ when $C$ is a prevariety.

**Proposition 12.** If $C$ is a prevariety, $\text{SF}(C) = \bigcup_{n \in \mathbb{N}} \text{TL}_n(C)$.

## V. GROUP BASES

In the literature, concatenation hierarchies use a few specific bases consisting solely of group languages, which we also adopt for navigational hierarchies. In this section, we introduce and motivate such “group bases”. We prove that for the resulting hierarchies, membership at level two reduces to separation for the basis, show that the navigational hierarchies are strict, and compare them to concatenation hierarchies.

### A. Definitions

Group languages are those that can be recognized by a morphism into a finite group. A group prevariety is a prevariety $\mathcal{G}$ consisting of group languages only. We also look at a slight extension: for each class $\mathcal{G}$, we let $\mathcal{G}^+$ be the class consisting of all languages $\{\varepsilon\} \cup L$ and $A^+ \cap L$ for $L \in \mathcal{G}$. One can verify that if $\mathcal{G}$ is a prevariety, then so is $\mathcal{G}^+$.

The simplest group prevariety is $\text{ST} = \{\emptyset, A^*\}$. We let $\text{DD} = \text{ST}^+ = \{\emptyset, \{\varepsilon\}, A^+, A^*\}$. These are the bases of the two most common concatenation hierarchies: the Straubing-Thérien hierarchy [6], [7] and the dot-depth [4]. They both classify the original class SF of star-free languages [3]. By results of McNaughton-Papert [1] and Kamp [2], SF also consists of languages that can be defined in first-order logic $\text{FO}(<)$, or in full linear temporal logic LTL. Thus, the navigational hierarchies of bases ST and DD classify the languages that can be defined in LTL. The modalities $F_{A^*}$ and $P_{A^*}$ have the semantics of the classic ones F and P of unary temporal logic (for instance $w, i \models F \varphi$ when there exists $j \in \text{Pos}(w)$ such that $i < j$ and $w, j \models \varphi$). Similarly, $F_{\{\varepsilon\}}$ and $P_{\{\varepsilon\}}$ have the semantics of the classic modalities X and Y (for instance, $w, i \models X \varphi$ when $i+1 \in \text{Pos}(w)$ and $w, i+1 \models \varphi$). This means that $\text{TL}(\text{ST})$ and $\text{TL}(\text{DD})$ are exactly the standard
variants of unary temporal logic, which we denote by TL and TLX (see e.g., [22]). The levels two (i.e., TL₂(ST) and TL₂(DD)) have also been investigated [28]. Indeed, these are also the levels one for the bases AT and LT.

**Proposition 13.** $TL_2(ST) = TL(AT)$ and $TL_2(DD) = TL(LT)$.

*Proof.* One may verify that $AT \subseteq TL(ST)$ and $LT \subseteq TL(DD)$ which yields the right to left inclusions. For the converse, results of Etessami, Vardi, Thérien, Wilke, Pin and Weil yield $TL(ST) = IPol(AT)$ and $TL(DD) = IPol(LT)$ [22], [23], [31]. Thus, $TL_2(ST) \subseteq TL(Pol(AT))$ and $TL_2(DD) \subseteq TL(Pol(LT))$. This completes the proof since $TL(AT) = TL(Pol(AT))$ and $TL(LT) = TL(Pol(LT))$ by Proposition 10. □

**Proposition 13** establishes a connection with the work of Krebs, Lodaya, Pandya and Straubing [28], who investigated TL(AT) and TL(LT). They mostly work with definitions in terms of two-variable first-order logic: $FO^2(I_{AT})$ and $FO^2(I_{LT})$ (strictly speaking, they use specialized sets of predicates, not the generic ones $I_{AT}$ and $I_{LT}$. However, it is immediate that they yield the same classes of languages). They prove that both classes have decidable *membership*. In the paper, we prove decidability for separation and covering as well.

The bases ST and DD = ST⁺ give rise to hierarchies that fall within the class SF of star-free languages. More generally, if the only group languages in $C$ are $\emptyset$ and $A^*$, then all levels of the concatenation or navigational hierarchy of basis $C$ are subclasses of SF. In other words, to go beyond star-free languages, we need bases that include nontrivial group languages. This makes group prevarieties particularly appealing choices as bases for both types of hierarchies.

Besides the prevariety ST, there are three other standard examples of group prevarieties: the classes MOD of modulo languages (membership of a word depends only on its length modulo a fixed integer), AMT of alphabet modulo testable languages (membership of a word depends only on the number of occurrences of each letter modulo a fixed integer), and GR of all group languages. The concatenation hierarchies of bases MOD and MOD⁺ are important [43], [10], [44]. They classify first-order logic with modular predicates, FO(<, MOD). Level one in the navigational hierarchy of basis MOD (i.e., TL(MOD)) has also been investigated [25]. The concatenation hierarchies of bases AMT and AMT⁺ are also natural: they classify variants of first-order logic equipped with predicates counting the number of occurrences of a specific letter occurring before a position, modulo an integer. Finally, the class GR of all group languages defines a concatenation hierarchy introduced by Margolis and Pin [8]: the group hierarchy. For these three classes, separation is decidable [33], [45], [34].

## B. Membership for levels of navigational hierarchies

Membership for the levels one was handled in [14]: if $G$ is a group prevariety $G$ with decidable separation, then $TL(G)$ and $TL(G^+)$ have decidable membership (this is also immediate from Theorem 6). We prove the same for level two using concatenation hierarchies.

Since we are dealing with group based hierarchies, we have the following proposition.

**Proposition 14.** Let $G$ be a group prevariety and $C \in \{G, G^+\}$. Then, $TL_2(C) = TL(BPol(C))$.

*Proof.* We have $TL(BPol(C)) \subseteq TL_2(C)$ as $BPol(C) \subseteq TL(C)$ by Corollary 11. For the converse inclusion, it is shown in [14, Theorems 10.1 and 10.4] that $TL(C) = IPol(BPol(C))$ (this requires the hypothesis that $G$ consists of group languages). In particular, $TL(C) \subseteq Pol(BPol(C))$ which yields $TL_2(C) \subseteq TL(Pol(BPol(C)))$. Finally, Proposition 10 yields $TL(Pol(BPol(C))) = TL(BPol(C))$, completing the proof. □

**Proposition 14** can be combined with Corollary 7. We obtain that for every group prevariety $G$, if $C \in \{G, G^+\}$, then $TL_2(C)$-membership reduces to $BPol(C)$-separation. The latter problem has been extensively studied for group classes. If $C \in \{G, G^+\}$, it is shown in [32], [46] that $BPol(C)$-separation reduces to $C$-separation. This yields the following result.

**Corollary 15.** Let $G$ be a group prevariety with decidable separation, $TL_2(G)$ and $TL_2(G^+)$ have decidable membership.

Corollary 15 applies to the bases ST, MOD, AMT and GR, as they have decidable separation [33], [45], [34]. We push this for ST and DD = ST⁺ in Section VII: we prove that $TL_2(ST)$ and $TL_2(DD)$ have decidable separation. Thus, by Corollary 7, $TL_3(ST)$ and $TL_3(DD)$ have decidable membership.

## C. Strictness and strict intertwining of hierarchies

We prove that for every group prevariety $G$, the navigational hierarchies of bases $G$ and $G^+$ are strict and strictly intertwined if the alphabet contains at least two letters. Thus, we assume that the alphabet $A$ contains at least two letters, written $a$ and $b$.

We start from languages introduced by Brzozowski and Knast [5] to prove that the *dot-depth* hierarchy (i.e., the concatenation hierarchy of basis DD) is strict. We first recall these languages, before adapting them to the generic setting. Let,

$$H_0 = \{\epsilon\} \quad \text{and} \quad H_n = (aH_{n-1}b)^* \quad \text{for } n \ge 1.$$

Brzozowski and Knast proved that $H_n \in BPol_n(DD)$ for all $n \in \mathbb{N}$ and $H_n \notin BPol_{n-1}(DD)$ for all $n \ge 1$. Actually, these languages imply that the *navigational hierarchy* of basis DD is strict, as one can show that $H_n \notin TL_{n-1}(DD)$. We generalize them to handle all bases $G$ and $G^+$ simultaneously.

**Remark 5.** The languages $H_n$ themselves cannot be used in the general case. Indeed, one can show that for all $n \in \mathbb{N}$, $H_n$ belongs to level one of the group hierarchy (i.e., $BPol(GR)$).

We prove that for every prevariety $G$, the navigational hierarchies of bases $G$ and $G^+$ are strict and strictly intertwined. Since $\{\epsilon\}, A^+ \in BPol(G)$, we have $G^+ \subseteq BPol(G)$. Hence, $G \subseteq G^+ \subseteq BPol(G) \subseteq TL(G)$. Therefore, a simple induction yields the following inclusions:

$$ \begin{aligned} & TL_n(G) \subseteq TL_n(G^+) \subseteq TL_{n+1}(G), \\ & BPol_n(G) \subseteq BPol_n(G^+) \subseteq BPol_{n+1}(G). \end{aligned} \quad (3) $$
Our goal is to show that the four inclusions of (3) are strict. Since $BPol_n(C) \subseteq TL_n(C)$ for all classes $C$ by Corollary 11, it suffices to exhibit two languages $K_n, L_n$ such that,

* $K_n \in BPol_n(G^+)$, but $K_n \notin TL_n(G)$.

* $L_n \in BPol_{n+1}(G)$, but $L_n \notin TL_n(G^+)$.

We modify the languages $H_n$ by replacing the letters “a” and “b” by more involved languages.

Consider the word $x_i = ab^i$ and the language $Y_i = a^+b^i$ for all $i \ge 1$. Moreover, let $Q = x_1^+x_2^+x_1$, $R = x_3^+x_4^+x_3$, $S = Y_1^+Y_2^+Y_1$ and $T = Y_3^+Y_4^+Y_3$. Finally, we define,

$K_0 = \{\varepsilon\}$ and $K_n = (QK_{n-1}R)^*$ for $n \ge 1$,

$L_0 = a^*$ and $L_n = (a + SL_{n-1}T)^*$ for $n \ge 1$.

The strictness proof is based on two lemmas. The first one considers the operator BPol. We prove it in Appendix ??.

**Lemma 16.** For every $n \in \mathbb{N}$, we have $K_n \in BPol_n(DD)$ and $L_n \in BPol_{n+1}(ST)$.

Since $ST \subseteq G$ and $DD = ST^+ \subseteq G^+$, Lemma 16 implies that $K_n \in BPol_n(G^+)$ and $L_n \in BPol_{n+1}(G)$ for every group prevariety $G$. Since $G \subseteq GR$ and $G^+ \subseteq GR^+$, the next lemma implies that $K_n \notin TL_n(G)$ and $L_n \notin TL_n(G^+)$. Do note that in the proof of this lemma, separation plays a central role to conduct the induction, as explained in the introduction.

**Lemma 17.** For every $n \in \mathbb{N}$, we have $K_n \notin TL_n(GR)$ and $L_n \notin TL_n(GR^+)$.

*Proof.* We sketch the proof that $K_n \notin TL_n(GR)$ for all $n$ using Lemma 8 (for details and the similar proof that $L_n \notin TL_n(GR^+)$, see Appendix ??). Let $Q_0 = Q$ and $R_0 = R$. For $n \ge 1$, let $Q_n = K_nQ_{n-1}K_n$ and $R_n = K_nR_{n-1}K_n$. We use induction on $n$ to show that $K_n$ is not $TL_n(GR)$-separable from either $Q_n$ and $R_n$. This yields $K_n \notin TL_n(GR)$, since $K_n$ does not intersect $Q_n$ nor $R_n$.

When $n=0$, we have to prove that $\{\varepsilon\}$ is not GR-separable from either $Q = x_1^+x_2^+x_1$ and $R = x_3^+x_4^+x_3$. By symmetry, we only prove the former. Let $U \in GR$ such that $\varepsilon \in U$. We show that $U \cap x_1^+x_2^+x_1 \neq \emptyset$. By hypothesis, $U$ is recognized by a morphism $\alpha : A^* \to G$ into a finite group $G$. Let $p = \omega(G)$ and $w = x_1^{p-1}x_2^p x_1 \in x_1^+x_2^+x_1$. Since $G$ is a group, $\alpha(w) = 1_G = \alpha(\varepsilon)$. Therefore, $w \in U \cap x_1^+x_2^+x_1$.

Assume that $n \ge 1$. By induction, $K_{n-1}$ is not $TL_{n-1}(GR)$-separable from either $Q_{n-1}$ or $R_{n-1}$. One can check from the definition that $K_{n-1}^* = K_{n-1} \subseteq K_n$. By definition of $K_n$, this yields $K_n = K_{n-1}^*(Q_{n-1}K_{n-1}^*R_{n-1}K_{n-1}^*)^*$. Thus, Lemma 8 implies that $K_n$ is not $TL_n(GR)$-separable from either $Q_n = K_nQ_{n-1}K_n$ or $R_n = K_nR_{n-1}K_n$. $\square$

Altogether, Lemmas 16 and 17 yield the desired theorem.

**Theorem 18.** Let $G$ be a group prevariety. If $|A| \ge 2$, then,

* The navigational hierarchies of bases $G$ and $G^+$ are both strict and strictly intertwined.

* The concatenation hierarchies of bases $G$ and $G^+$ are both strict and strictly intertwined.

### D. Comparing concatenation and navigational hierarchies

We compare the two kinds of hierarchies. If $C \in \{G, G^+\}$ for a group prevariety $G$, Lemma 16 and Lemma 17 yield that for all $n \in \mathbb{N}$, $BPol_{n+1}(C)$ contains a language outside of $TL_n(C)$. Here, we prove that for all $n \in \mathbb{N}$, $TL_2(C)$ contains a language outside of $BPol_n(C)$. Altogether, it follows that for all $m \ge 2$ and all $k > m$, $TL_m(C)$ and $BPol_k(C)$ are incomparable. We depict the situation for $m=2$ in Figure 3.

<figure><img src="image_3.png" /><figcaption>Fig. 3: Level 2 (filled) in a navigational hierarchy (bases $G/G^+$)</figcaption></figure>

The precise statement differs slightly depending on the basis. We start with ST which requires arbitrarily large alphabets.

**The basis ST.** It is shown in [28] that $TL(AT)$ (i.e., $TL_2(ST)$) by Proposition 13) contains a language outside of $BPol_n(ST)$ for all $n \in \mathbb{N}$. We reprove this result using distinct languages, as we shall reuse them to handle other bases.

For each $k \in \mathbb{N}$, we define an alphabet $A_k = \{\ell_0, \dots, \ell_k\}$ of size $k+1$ and two disjoint languages $U_k, V_k \subseteq A_k^*$. We let $U_0 = \{\varepsilon\}$ and $V_0 = A_0^*$. For $k \ge 1$, we let,

$$U_k = (\ell_k V_{k-1})^* \quad \text{and} \quad V_k = (\ell_k V_{k-1})^* \ell_k U_{k-1} (\ell_k V_{k-1})^*.$$

**Lemma 19.** For every $k \in \mathbb{N}$, we have $U_k, V_k \in TL_2(ST)$.

*Proof.* We use induction on $k$. If $k=0$, then $U_0 = \{\varepsilon\}$ is defined by $\neg F \neg \max$ and $V_0 = \ell_0^+$ by $F \ell_0 \wedge \neg F (\neg(\ell_0 \vee \max))$. Hence, $U_0, V_0 \in TL_2(ST)$. Assume now that $k \ge 1$. Induction yields $U_{k-1}, V_{k-1} \in TL_2(ST)$. We get two formulas $\varphi_U, \varphi_V \in TL_2(ST)$ defining $U_{k-1}$ and $V_{k-1}$, respectively. We use them to build new formulas defining $U_k$ and $V_k$. First, we modify $\varphi_U, \varphi_V$ to constrain their evaluation to the infixes in $A_{k-1}^*$. Let $\langle\varphi_U\rangle$ and $\langle\varphi_V\rangle$ be the formulas obtained from $\varphi_U$ and $\varphi_V$ by applying the two following kinds of modification:

1) We replace every atomic formula "min" by "min $\vee \ell_k$" and every atomic formula "max" by "max $\vee \ell_k$".

2) We recursively replace every subformula of the form $F_L \varphi'$ by $F_{L \cap A_{k-1}^*} \varphi'$, and every sub-formula of the form $P_L \varphi'$ by $P_{L \cap A_{k-1}^*} \varphi'$.

These remain $TL_2(ST)$ formulas since $A_k^* \in TL(ST)$. Consider the two following formulas of $TL_2(ST)$:

$$\psi_U = F_{\{\varepsilon\}} (\ell_k \vee \max) \wedge \neg F (\ell_k \wedge \neg \langle\varphi_V\rangle),$$

$$\psi_V = F_{\{\varepsilon\}} (\ell_k) \wedge F (\ell_k \wedge \langle\varphi_U\rangle) \wedge \neg F (\ell_k \wedge \neg \langle\varphi_V\rangle) \wedge F (\ell_k \wedge \neg \langle\varphi_V\rangle).$$

One can verify that $\psi_U$ and $\psi_V$ define $U_k$ and $V_k$, respectively. Hence, $U_k, V_k \in TL_2(ST)$, which completes the proof. $\square$

Moreover, we have the following lemma. As for Lemma 17, separation plays a central role to conduct its inductive proof.

**Lemma 20.** For every $k \in \mathbb{N}$, we have $U_k \notin Pol_{k+1}(ST)$.
**Proof.** We show by induction on $k$ that $U_k$ is not $\mathrm{Pol}_{k+1}(\mathrm{ST})$-separable from $V_k$, for all $k \in \mathbb{N}$. Since we have $U_k \cap V_k = \emptyset$, this yields $U_k \not\in \mathrm{Pol}_{k+1}(\mathrm{ST})$, as desired. For $k = 0$, $U_0 = \{\varepsilon\}$ is not $\mathrm{Pol}(\mathrm{ST})$-separable from $V_0 = \ell_0^+$, since the only language in $\mathrm{Pol}(\mathrm{ST})$ containing $\varepsilon$ is $A^*$. Assume now that $k \ge 1$. By induction, $U_{k-1}$ is not $\mathrm{Pol}_k(\mathrm{ST})$-separable from $V_{k-1}$. By Lemma 1, $\ell_k U_{k-1}$ is not $\mathrm{Pol}_k(\mathrm{ST})$-separable from $\ell_k V_{k-1}$, which means that $\ell_k V_{k-1}$ is not co-$\mathrm{Pol}_k(\mathrm{ST})$-separable from $\ell_k U_{k-1}$. By Lemmas 4 and 3, it follows that $U_k = (\ell_k V_{k-1})^*$ is not $\mathrm{Pol}_{k+1}(\mathrm{ST})$-separable from $V_k = (\ell_k V_{k-1})^* \ell_k U_{k-1} (\ell_k V_{k-1})^*$. $\square$

From Lemmas 16, 17, 19 and 20, we get the next theorem.

**Theorem 21.** Let $m, k \in \mathbb{N}$ such that $2 \le m < k < |A|$. Then, the classes $\mathrm{TL}_m(\mathrm{ST})$ and $\mathrm{BPol}_k(\mathrm{ST})$ are incomparable.

**Theorem 21** involves arbitrarily large alphabets. It is shown in [28] that when $|A| = 2$, we have $\mathrm{TL}_2(\mathrm{ST}) \subseteq \mathrm{BPol}_3(\mathrm{ST})$. The authors conjecture that for a fixed alphabet, $\mathrm{TL}_2(\mathrm{ST})$ is included in some level $\mathrm{BPol}_n(\mathrm{ST})$. We prove a strengthening of this conjecture. We consider the operator “IPol”. Recall that $\mathrm{IPol}_n(C) = \mathrm{Pol}_n(C) \cap \mathrm{co-Pol}_n(C) \subseteq \mathrm{BPol}_n(C)$ for every class C.

**Theorem 22.** We have $\mathrm{IPol}_3(\mathrm{ST}) \subseteq \mathrm{TL}_2(\mathrm{ST}) \subseteq \mathrm{IPol}_{|A|+1}(\mathrm{ST})$.

**Proof.** The inclusion $\mathrm{IPol}_3(\mathrm{ST}) \subseteq \mathrm{TL}_2(\mathrm{ST})$ is shown in [28] using a result of Weil [47] (we also provide a simple proof in Appendix ??). In the main text, we only prove that $\mathrm{TL}_2(\mathrm{ST}) \subseteq \mathrm{IPol}_{|A|+1}(\mathrm{ST})$ in the special case when $|A| = 2$. The full proof is available in Appendix ??.

Let us consider an alphabet of size two, say $A = \{a, b\}$. Let $L \in A^*$ with $L \in \mathrm{TL}_2(\mathrm{ST})$. We prove that $L \in \mathrm{IPol}_3(\mathrm{ST})$. Let $\mathcal{D} = \mathrm{IPol}_2(\mathrm{ST})$. One can check that $\mathrm{BPol}(\mathcal{D}) = \mathrm{BPol}_2(\mathrm{ST})$, so that $\mathrm{IPol}_2(\mathcal{D}) = \mathrm{IPol}_3(\mathrm{ST})$. Therefore, it suffices to prove that $L \in \mathrm{IPol}_2(\mathcal{D})$. Let $\alpha : A^* \to M$ be the syntactic morphism of $L$. By Theorem 5, we have to prove that if $(e, s) \in E(M) \times M$ is a $\mathcal{D}$-pair and $t \in M$, then $(\mathrm{ese t e})^{\omega+1} = (\mathrm{ese t e})^{\omega} \mathrm{ete}(\mathrm{ese t e})^{\omega}$.

Let $H = A^*aA^* \cap A^*bA^*$. Clearly, $A^* = H \cup a^* \cup b^*$. By definition of $\mathcal{D}$-pairs, $\alpha^{-1}(e)$ is not $\mathcal{D}$-separable from $\alpha^{-1}(s)$. Hence, as $H, a^*, b^* \in \mathcal{D}$ (since $\mathrm{BPol}(\mathrm{ST}) \subseteq \mathcal{D}$ by definition), one can verify that one of the three following conditions holds:

1) $H \cap \alpha^{-1}(e)$ is not $\mathcal{D}$-separable from $H \cap \alpha^{-1}(s)$,

2) $a^* \cap \alpha^{-1}(e)$ is not $\mathcal{D}$-separable from $a^* \cap \alpha^{-1}(s)$,

3) $b^* \cap \alpha^{-1}(e)$ is not $\mathcal{D}$-separable from $b^* \cap \alpha^{-1}(s)$.

We consider three cases depending on which property holds. Assume first that $H \cap \alpha^{-1}(e)$ is not $\mathcal{D}$-separable from $H \cap \alpha^{-1}(s)$. In particular, both languages are nonempty. We get $u \in H \cap \alpha^{-1}(e)$ and $v \in H \cap \alpha^{-1}(s)$. Let $x \in \alpha^{-1}(t)$ and $w = uxu$. By definition of $H$, the two letters $a$ and $b$ of $A$ occur in $u, v$ and $w$. One can verify that this implies that $\{u\}$ is neither AT-separable from $\{v\}$ nor $\{w\}$. Thus, $(\alpha(u), \alpha(v)) = (e, s)$ and $(\alpha(u), \alpha(w)) = (e, \mathrm{ete})$ are AT-pairs. Since $L \in \mathrm{TL}_2(\mathrm{ST}) = \mathrm{TL}(\mathrm{AT})$, it then follows from Theorem 6 that $(\mathrm{ese t e})^{\omega} = (\mathrm{ese t e})^{\omega} \mathrm{ete}(\mathrm{ese t e})^{\omega}$. Finally, since $L \in \mathrm{TL}(\mathrm{AT})$, we know that $L$ is star-free. Thus, its syntactic monoid $M$ is aperiodic by Schützenberger's

theorem [3]. In particular, $(\mathrm{ese t e})^{\omega} = (\mathrm{ese t e})^{\omega+1}$ and we obtain $(\mathrm{ese t e})^{\omega+1} = (\mathrm{ese t e})^{\omega} \mathrm{ete}(\mathrm{ese t e})^{\omega}$ as desired.

It remains to handle the second case (the third one is symmetrical). Assume that $a^* \cap \alpha^{-1}(e)$ is not $\mathcal{D}$-separable from $a^* \cap \alpha^{-1}(s)$. In particular, both languages are nonempty. We prove that $e = \mathrm{ese}$, which yields the desired equality. There are two sub-cases depending on whether $a^* \cap \alpha^{-1}(e) = \{\varepsilon\}$ or $a^+ \cap \alpha^{-1}(e) \neq \emptyset$. In the first case, since $\{\varepsilon\} \in \mathcal{D}$ (this is because $\mathrm{BPol}(\mathrm{ST}) \subseteq \mathcal{D}$), the hypothesis that $a^* \cap \alpha^{-1}(e)$ is not $\mathcal{D}$-separable from $a^* \cap \alpha^{-1}(s)$ yields $\varepsilon \in a^* \cap \alpha^{-1}(s)$ and we get $e = s = 1_M$, whence $\mathrm{ese} = e$, as desired. Otherwise, $a^+ \cap \alpha^{-1}(e) \neq \emptyset$. This yields $k \ge 1$ such that $\alpha(a^k) = e$. Moreover, since $a^* \cap \alpha^{-1}(s) \neq \emptyset$, we have $\ell \in \mathbb{N}$ such that $\alpha(a^\ell) = s$. Let $r = \alpha(a)$. We have $e = r^k$ and since $e$ is idempotent, it follows that $e = r^\omega$. Moreover, $\mathrm{ese} = r^{\omega+\ell}$. Thus, since $M$ is aperiodic, we obtain again $e = \mathrm{ese}$. $\square$

**Remark 6.** Theorem 22 is specific to the level two. Indeed, the level $\mathrm{TL}_3(\mathrm{ST})$ contains a language outside of $\mathrm{BPol}_n(\mathrm{ST})$ for every $n \in \mathbb{N}$. This is implied by Theorem 29 below, as one can verify that $\mathrm{TL}_2(\mathrm{DD}) \subseteq \mathrm{TL}_3(\mathrm{ST})$.

Theorem 22 has a surprising corollary for binary alphabets.

**Corollary 23.** When $|A| = 2$, we have $\mathrm{TL}_2(\mathrm{ST}) = \mathrm{IPol}_3(\mathrm{ST})$.

Corollary 23 is reminiscent of a famous theorem by Thérien and Wilke [23] for the previous levels: $\mathrm{TL}(\mathrm{ST}) = \mathrm{IPol}_2(\mathrm{ST})$ (for every alphabet). Naturally, Corollary 23 fails in the general case (see Lemma 20). Nonetheless, $\mathrm{TL}(\mathrm{AT})$ over binary alphabets is the first special case considered by Krebs, Lodaya, Pandya and Straubing in their original paper [26].

**Groups bases.** Consider an arbitrary group basis $\mathcal{G}$ containing the modulo languages (MOD). In this case, two letters suffice. We reuse the above languages $U_k, V_k$, which we encode over a binary alphabet. Fix such an alphabet $A = \{a, b\}$. For every $k \in \mathbb{N}$, we define a morphism $\beta_k : A_k^* \to A^*$ as follows:

$$ \beta_k: \begin{array}{ccc} A_k^* & \to & A^*, \\ \ell_i & \mapsto & a^i b a^{k-i}. \end{array} $$

The following proposition (proved in Appendix ??) shows that this encoding maps $\mathrm{TL}_2(\mathrm{ST})$ to $\mathrm{TL}_2(\mathrm{MOD})$. Combined with Lemma 19, it implies that $\beta_k(U_k) \in \mathrm{TL}_2(\mathrm{MOD})$ for all $k \in \mathbb{N}$.

**Proposition 24.** Let $k \in \mathbb{N}$ and $L \subseteq A_k^*$. If $L \in \mathrm{TL}_2(\mathrm{ST})$, then $\beta_k(L) \in \mathrm{TL}_2(\mathrm{MOD})$.

The next statement serves as the counterpart of Lemma 20. Its proof is similar and given in Appendix ??.

**Lemma 25.** Let $\mathcal{G}$ be a group prevariety. For all $k \in \mathbb{N}$, we have $\beta_k(U_k) \notin \mathrm{Pol}_{k+1}(\mathcal{G})$.

Altogether, we get the following theorem.

**Theorem 26.** Let $\mathcal{G}$ be a group prevariety with $\mathrm{MOD} \subseteq \mathcal{G}$. Assume that $|A| \ge 2$. For all $m, k \in \mathbb{N}$ such that $2 \le m < k$, the classes $\mathrm{TL}_m(\mathcal{G})$ and $\mathrm{BPol}_k(\mathcal{G})$ are incomparable.

**Well-suited extensions of groups bases.** Consider the basis $\mathcal{G}^+$ for an arbitrary group prevariety $\mathcal{G}$. We again reuse the
languages $U_k, V_k$ and encode them over a binary alphabet $A = \{a, b\}$. For every $k \in \mathbb{N}$, let $B_k = A_k \cup \{b\}$. We define two morphisms $\gamma_k : B_k^* \to A_k^*$ and $\delta_k : B_k^* \to A^*$ as follows:

$$ \begin{array}{rcl} \gamma_k : & B_k^* \to A_k^* & \delta_k : B_k^* \to A^* \\ & b \mapsto \varepsilon & \text{and} \\ & \ell_i \mapsto \ell_i & \end{array} $$

By definition, if $L \subseteq A_k^*$, then $\gamma_k^{-1}(L)$ is the language consisting of all words built from a word in $L$ by inserting arbitrarily many “b”s at any position. The language $\delta_k(\gamma_k^{-1}(L))$ consists of all words built from those in $\gamma_k^{-1}(L)$ by replacing each letter $\ell_i$ with the word $ba^{i+1}$. The following proposition (proved in Appendix ??) is analogous to Proposition 24: it shows that this encoding maps $\text{TL}_2(\text{ST})$ to $\text{TL}_2(\text{DD})$. Combined with Lemma 19, it yields $\delta_k(\gamma_k^{-1}(U_k)) \in \text{TL}_2(\text{DD})$ for all $k \in \mathbb{N}$.

**Proposition 27.** Let $k \in \mathbb{N}$ and $L \subseteq A_k^*$. If $L \in \text{TL}_2(\text{ST})$, then $\delta_k(\gamma_k^{-1}(L)) \in \text{TL}_2(\text{DD})$.

The following statement serves as the counterpart of Lemma 20. Its proof is similar and given in Appendix ??.

**Lemma 28.** Let $\mathcal{G}$ be a group prevariety. For all $k \in \mathbb{N}$, we have $\delta_k(\gamma_k^{-1}(U_k)) \notin \text{Pol}_{k+1}(\mathcal{G}^+)$.

Altogether, we get the following theorem.

**Theorem 29.** Let $\mathcal{G}$ be a group prevariety and assume that $|A| \ge 2$. For all $m, k \in \mathbb{N}$ such that $2 \le m < k$, the classes $\text{TL}_m(\mathcal{G}^+)$ and $\text{BPol}_k(\mathcal{G}^+)$ are incomparable.

## VI. RATING MAPS

We use the framework of [37] to handle separation and covering. It relies on objects called *rating maps*. They “rate” covers. For each lattice $C$, each rating map $\rho$ and each language $L$, we define the optimal $C$-covers of $L$ for $\rho$. We reduce $C$-covering to the computation of optimal $C$-covers.

### A. Multiplicative rating maps

A semiring is a tuple $(R, +, \cdot)$ where $R$ is a set and “+” and “.” are two binary operations called addition and multiplication, which satisfy the following axioms:

* $(R, +)$ is a commutative monoid. Its identity is denoted by $0_R$.

* $(R, \cdot)$ is a monoid. Its identity is denoted by $1_R$.

* Distributivity: for $r, s, t \in R$, $r \cdot (s + t) = (r \cdot s) + (r \cdot t)$ and $(r + s) \cdot t = (r \cdot t) + (s \cdot t)$.

* $0_R$ is a zero for $(R, \cdot): 0_R \cdot r = r \cdot 0_R = 0_R$ for all $r \in R$.

A semiring $R$ is *idempotent* when $r+r=r$ for all $r \in R$ (there is no additional constraint on the multiplication). If $(R, +, \cdot)$ is an idempotent semiring, we define a relation $\leq$ over $R$: for all $r, s \in R$, we let $r \leq s$ if and only if $r+s=s$. One can check that $\leq$ is a partial order compatible with addition and multiplication and that every morphism between two idempotent semirings is increasing for this ordering.

**Example 1.** A key example is the set of all languages $(2^{A^*}, \cup, \cdot)$, with union as addition and language concatenation as multiplication $(\{\varepsilon\}$ is neutral). The ordering is inclusion.

When dealing with subsets of an idempotent semiring $R$, we shall often apply a *downset operation*. Given $S \subseteq R$, we write $\downarrow_R S = \{r \in R \mid r \leq s \text{ for some } s \in S\}$. We extend this notation to Cartesian products of arbitrary sets with $R$. Given some set $X$ and $S \subseteq X \times R$, we write $\downarrow_R S = \{(x, r) \in X \times R \mid \exists s \in R \text{ s.t. } r \leq s \text{ and } (x, s) \in S\}$.

**Multiplicative rating maps.** We define a multiplicative rating map as a semiring morphism $\rho : (2^{A^*}, \cup, \cdot) \to (R, +, \cdot)$ where $(R, +, \cdot)$ is a finite idempotent semiring. That is,

1) $\rho(\emptyset) = 0_R$ and for every $K_1, K_2 \subseteq A^*$, we have $\rho(K_1 \cup K_2) = \rho(K_1) + \rho(K_2)$.

2) $\rho(\{\varepsilon\}) = 1_R$ and for every $K_1, K_2 \subseteq A^*$, we have $\rho(K_1 K_2) = \rho(K_1) \cdot \rho(K_2)$.

For the sake of improved readability, for all words $w \in A^*$, we write $\rho(w)$ for $\rho(\{w\})$. Also, we write $\rho_* : A^* \to R$ for the restriction of $\rho$ to $A^*$: for all $w \in A^*$, we have $\rho_*(w) = \rho(w)$ (this notation is useful when referring to the language $\rho_*^{-1}(r) \subseteq A^*$ consisting of all words $w \in A^*$ such that $\rho(w) = r$). It is a morphism into the finite monoid $(R, \cdot)$.

**Remark 7.** As the adjective “multiplicative” suggests, there exists a more general notion of “rating map”. We do not use this notion, see [37] for the general framework.

Now, a full rating map is a multiplicative rating map $\rho : 2^{A^*} \to R$ such that for every language $K \subseteq A^*$, there exist finitely many words $w_1, \dots, w_n \in K$ such that $\rho(K) = \rho(w_1) + \dots + \rho(w_n)$. In this case, $\rho$ is fully defined by the morphism $\rho_* : A^* \to R$. Indeed, for each $K$, $\rho(K)$ is equal to the sum of all elements $\rho(w)$ for $w \in K$ (although this sum may be infinite, it simplifies to a finite one because addition is commutative and idempotent). Hence, full rating maps are finitely representable. In particular, we can discuss algorithms that take full rating maps as input.

**Optimal imprints.** Let $\rho : 2^{A^*} \to R$ be a multiplicative rating map. Given a finite set of languages $K$, the $\rho$-imprint of $K$ is the subset of $R$ defined by $\mathcal{I}[\rho](K) = \downarrow_R \{\rho(K) \mid K \in K\}$. Intuitively, when $K$ is a cover of some language $L$, this object measures the “quality” of $K$ (smaller is better).

We now define optimality. Consider a lattice $C$. For a language $L$, an *optimal* $C$-cover of $L$ for $\rho$ is a $C$-cover $K$ of $L$ with the least possible $\rho$-imprint, i.e., such that $\mathcal{I}[\rho](K) \subseteq \mathcal{I}[\rho](K')$ for every $C$-cover $K'$ of $L$. In general, there may be infinitely many optimal $C$-covers for a given multiplicative rating map $\rho$. However, at least one always exists if $C$ is a lattice. We state this property in the following lemma (proved in [37, Lemma 4.15]).

**Lemma 30.** Given a lattice $C$, a multiplicative rating map $\rho$ and a language $L$, there exists an optimal $C$-cover of $L$ for $\rho$.

By definition, given a lattice $C$, a multiplicative rating map $\rho$ and a language $L$, all optimal $C$-covers of $L$ for $\rho$ have the same $\rho$-imprint. Hence, this unique $\rho$-imprint is a *canonical* object for $C$, $\rho$ and $L$. We call it the *C*-optimal $\rho$-imprint on $L$ and we denote it by $\mathcal{I}_C[L, \rho]$. That is, $\mathcal{I}_C[L, \rho] = \mathcal{I}[\rho](K)$ for every optimal $C$-cover $K$ of $L$ for $\rho$.
## B. Application to covering

Deciding C-covering for a fixed class C reduces to finding an algorithm that computes C-optimal imprints. If C is a Boolean algebra, we have the following statement of [37].

**Proposition 31.** Let C be a Boolean algebra. There exists an effective reduction from C-covering to the following problem: "given as input a full rating map $\rho: 2^{A^*} \to R$ and $F \subseteq R$, decide whether $\mathcal{I}_C [A^*, \rho] \cap F = \emptyset$".

*Proof.* We sketch the reduction (see [37] for details). Let $(L_0, \{L_1, \dots, L_n\})$ be an input of the C-covering problem. One can compute a morphism $\alpha: A^* \to M$ recognizing all regular languages $L_i$: for each $i \le n$, there exists $F_i \subseteq M$ such that $L_i = \alpha^{-1}(F_i)$. We build a full rating map $\rho: 2^{A^*} \to 2^M$. Its rating set is the idempotent semiring $(2^M, \cup, \cdot)$ whose multiplication is obtained by lifting the one of $M$. For all $K \subseteq A^*$, we define $\rho(K) = \alpha(K)$. Now, let $F \subseteq 2^M$ be the set of all subsets $X \subseteq M$ such that $X \cap F_i \ne \emptyset$ for all $i \le n$. Using the fact that $C$ is a Boolean algebra, one can check that $(L_0, \{L_1, \dots, L_n\})$ is C-coverable if and only if $\mathcal{I}_C [A^*, \rho] \cap F = \emptyset$. $\square$

The converse is also true: if C-covering is decidable, then one can compute the C-optimal imprints (see Appendix ??).

**Proposition 32.** Let C be a Boolean algebra with decidable covering. Given as input a regular language L and a full rating map $\rho: 2^{A^*} \to R$, one can compute the set $\mathcal{I}_C [L, \rho]$.

**Pointed optimal imprints.** By Proposition 31, an algorithm computing $\mathcal{I}_C [A^*, \rho]$ from a full rating map $\rho$ yields a procedure for C-covering. In Section VII, we consider $C = \text{TL}(\text{AT})$. The procedure itself involves an object carrying more information. Let C be a Boolean algebra, $\eta: A^* \to N$ be a morphism into a finite monoid and $\rho: 2^{A^*} \to R$ be a multiplicative rating map. The $\eta$-pointed C-optimal $\rho$-imprint is the following set:

$$ \mathcal{P}_C[\eta, \rho] = \{ (t, r) \in N \times R \mid r \in \mathcal{I}_C[\eta^{-1}(t), \rho] \}. $$

Note that $\mathcal{P}_C[\eta, \rho] \subseteq N \times R$. It will be convenient to use the a functional notation here: given a subset $S \subseteq N \times R$ and $t \in N$, we write $S(t) \subseteq R$ for the set $S(t) = \{r \in R \mid (t, r) \in S\}$.

The set $\mathcal{P}_C[\eta, \rho]$ encodes the C-optimal $\rho$-imprint on $A^*$, i.e., the subset $\mathcal{I}_C [A^*, \rho]$ of $R$. Indeed, the following easy lemma is an immediate corollary of [37, Fact 4.7].

**Lemma 33.** Let C be a Boolean algebra, $\eta: A^* \to N$ be a morphism and $\rho: 2^{A^*} \to R$ be a multiplicative rating map. Then, $\mathcal{I}_C [A^*, \rho] = \bigcup_{t \in N} \mathcal{I}_C [\eta^{-1}(t), \rho] = \bigcup_{t \in N} \mathcal{P}_C[\eta, \rho](t)$.

Our goal is to compute $\mathcal{P}_{\text{TL(AT)}}[\eta_{\text{AT}}, \rho] \subseteq 2^A \times R$, in order to decide TL(AT)-covering. Recall that $\eta_{\text{AT}}: A^* \to 2^A$ is the canonical AT-morphism recognizing all languages of AT.

## VII. OPTIMAL IMPRINTS FOR TL(AT)

We turn to our main theorem. It characterizes the TL(AT)-optimal imprints. The characterization yields a least fixpoint algorithm for computing the set $\mathcal{P}_{\text{TL(AT)}}[\eta_{\text{AT}}, \rho]$ from a full rating map $\rho$. By Proposition 31 and Lemma 33, this yields

the decidability of TL(AT)-covering. Note that the algorithm uses a subprocedure from [14], [48] deciding covering for the simpler class TLX = TL(DD), which is a nontrivial question.

**Remark 8.** Considering TL(AT)-covering is mandatory even if one is solely interested in separation, as mentioned in the introduction. There does not appear to be a simpler, specialized algorithm for TL(AT)-separation. This is unsurprising, as performing a fixpoint computation often requires extra information (see, for example the case of star-free languages [49]). Finally, the framework itself seems indispensable: there is no clear way to formulate TL(AT)-operation without rating maps.

**Preliminaries.** We use a construction taking as input an idempotent semiring $R$ and an arbitrary subset $Q \subseteq R$ to build a full rating map $\pi_{R,Q}: 2^{Q^*} \to R$ on the alphabet $Q$.

**Remark 9.** Given $q_1, \dots, q_n \in Q$, the notation $q_1 \cdots q_n$ is ambiguous: it could either denote a word of length $n$ in $Q^*$ or the multiplication of $n$ elements in $Q$. For the sake of avoiding confusion, given an element $q \in Q$, we shall write $(q)$ when we use it as a letter: we denote by $(q_1)(q_2) \cdots (q_n) \in Q^n$ the word made of the $n$ letters $q_1, \dots, q_n \in Q$.

Since we are defining a full rating map, it suffices to specify the image of single letters $(q) \in Q$. Since $Q \subseteq R$, we simply define $\pi_{R,Q}((q)) = q$ for all $q \in Q$. Our characterization uses TLX-optimal $\pi_{R,Q}$-imprints (see TL(AT)-operation below).

**Characterization.** Consider a full rating map $\rho: 2^{A^*} \to R$. We define the TL(AT)-saturated subsets of $2^A \times R$ for $\rho$. We shall prove that $\mathcal{P}_{\text{TL(AT)}}[\eta_{\text{AT}}, \rho]$ is the least such set (with respect to inclusion). Let $S \subseteq 2^A \times R$. We say that $S$ is TL(AT)-saturated for $\rho$ when the following conditions hold:

1) **Trivial elements.** $(\eta_{\text{AT}}(w), \rho(w)) \in S$ for all $w \in A^*$.

2) **Downset.** We have $\downarrow_R S = S$.

3) **Multiplication.** For every $(B_1, r_1), (B_2, r_2) \in S$, we have $(B_1 \cup B_2, r_1 r_2) \in S$.

4) **TL(AT)-operation.** For all $B \in 2^A$ and $Q \subseteq S(B)$, we have $\mathcal{I}_{\text{TLX}} [Q^+, \pi_{R,Q}] \subseteq S(B)$.

**Theorem 34.** Let $\rho: 2^{A^*} \to R$ be a full rating map, Then, $\mathcal{P}_{\text{TL(AT)}}[\eta_{\text{AT}}, \rho]$ is the least TL(AT)-saturated subset of $2^A \times R$.

Theorem 34 provides an algorithm computing the set $\mathcal{P}_{\text{TL(AT)}}[\eta_{\text{AT}}, \rho]$ from an input full rating map $\rho: 2^{A^*} \to R$. Indeed, the least TL(AT)-saturated subset of $2^A \times R$ for $\rho$ can be computed using a least fixpoint procedure. It starts from the set of trivial elements and saturates it with the three operations in the definition. Clearly, downset and multiplication can be implemented. For TL(AT)-operation, one needs to compute the set $\mathcal{I}_{\text{TLX}} [Q^+, \pi_{R,Q}]$ from the full rating map $\pi_{R,Q}$. In view of Proposition 32, this boils down to deciding TLX-covering and it is shown in [14], [48] that this problem is decidable.

In view of Lemma 33, this yields a procedure that computes $\mathcal{I}_{\text{TLX}} [A^*, \rho] \subseteq R$ from an input full rating map $\rho: 2^{A^*} \to R$. Thus, TL(AT) has decidable covering by Proposition 31.

**Corollary 35.** Separation and covering are decidable for the class TL$_2$(ST) = TL(AT).
Corollary 35 also implies the decidability of separation and covering for the class TL(LT). It is shown in [28, Theorem 8.1] that the classes TL(AT) and TL(LT) are connected by an operator called “enrichment” or “wreath product”. It combines two classes into a larger one: TL(LT) = TL(AT) ∠ SU. Here, SU stands for the class of “suffix languages”: it consists of all Boolean combinations of languages $A^*w$ with $w \in A^*$.

**Remark 10.** The presentation in [28] differs from the one above. The authors consider the algebraic varieties characterizing TL(AT) and SU rather than the classes themselves. Their theorem states that the variety characterizing TL(LT) is exactly the wreath product of the variety $M_eDA$ (which characterizes TL(AT)) with the variety $D$ (which characterizes SU).

It is known that the operator $C \mapsto C \circ SU$ preserves the decidability of both separation and covering [48]. Therefore, we obtain the following additional corollary.

**Corollary 36.** Separation and covering are decidable for the class TL<sub>2</sub>(DD) = TL(LT).

Finally, Corollary 7 yields that level three in both hierarchies has decidable membership.

**Corollary 37.** Membership is decidable for the classes TL<sub>3</sub>(ST) and TL<sub>3</sub>(DD).

*Proof of Theorem 34.* We fix a full rating map $\rho: 2^{A^*} \to R$. There are two directions corresponding to soundness and completeness in the fixpoint procedure computing $\mathcal{P}_{\text{TL(AT)}}[\eta_{\text{AT}}, \rho]$.

**Proposition 38.** $\mathcal{P}_{\text{TL(AT)}}[\eta_{\text{AT}}, \rho]$ is TL(AT)-saturated for $\rho$.

**Proposition 39.** Let $S \subseteq 2^A \times R$ be TL(AT)-saturated for $\rho$. For all $B \subseteq A$, there exists a TL(AT)-cover $\mathbf{K}_B$ of $\eta_{\text{AT}}^{-1}(B)$ such that $\mathcal{I}[\rho](\mathbf{K}_B) \subseteq S(B)$.

We first complete the main proof. By Proposition 38, $\mathcal{P}_{\text{TL(AT)}}[\eta_{\text{AT}}, \rho]$ is TL(AT)-saturated. We need to prove that it the least such set. Let $S \subseteq 2^A \times R$ which is TL(AT)-saturated for $\rho$. We prove that $\mathcal{P}_{\text{TL(AT)}}[\eta_{\text{AT}}, \rho] \subseteq S$. Clearly, it suffices to show that $\mathcal{P}_{\text{TL(AT)}}[\eta_{\text{AT}}, \rho](B) \subseteq S(B)$ for all $B \in 2^A$. Proposition 39 yields a TL(AT)-cover $\mathbf{K}_B$ of $\eta_{\text{AT}}^{-1}(B)$ such that $\mathcal{I}[\rho](\mathbf{K}_B) \subseteq S(B)$. This completes the proof as $\mathcal{P}_{\text{TL(AT)}}[\eta_{\text{AT}}, \rho](B) = \mathcal{I}_{\text{TL(AT)}}[\eta_{\text{AT}}^{-1}(B), \rho]$ and $\mathcal{I}_{\text{TL(AT)}}[\eta_{\text{AT}}^{-1}(B), \rho] \subseteq \mathcal{I}[\rho](\mathbf{K}_B)$ by definition.

We now prove Proposition 39, which is the most interesting. Proposition 38 is easier and proved in Appendix ???. We fix a TL(AT)-saturated set for $\rho$, say $S \subseteq 2^A \times R$.

We use induction to prove a more general statement involving auxiliary alphabets. A good triple is a tuple $(\mathbb{A}, \beta, \tau)$ where $\mathbb{A}$ is an alphabet, $\beta: \mathbb{A}^* \to 2^A$ is a morphism such that $\beta^{-1}(\emptyset) = \{\varepsilon\}$ and $\tau: 2^{\mathbb{A}^*} \to R$ is a full rating map such that for every letter $\ell \in \mathbb{A}$, we have $(\beta(\ell), \tau(\ell)) \in S$. Moreover, we write $C_\beta$ for the class consisting of all languages over $\mathbb{A}$ recognized by $\beta$. A TL$(C_\beta)$-partition is a TL$(C_\beta)$-cover that is a partition. Our goal is to build a specific TL$(C_\beta)$-partition of $\mathbb{A}^*$, which we do in the following lemma.

**Lemma 40.** Let $(\mathbb{A}, \beta, \tau)$ be a good triple. There is a TL$(C_\beta)$-partition $\mathbf{K}$ of $\mathbb{A}^*$ such that,

$$ \text{for all } K \in \mathbf{K}, \text{ there exists } B \in 2^A \text{ such that} \\ K \subseteq \beta^{-1}(B) \text{ and } (B, \tau(K)) \in S. \qquad (4) $$

We first use Lemma 40 to complete the main proof. Since $S$ is TL(AT)-saturated for $\rho$, we have $(\eta_{\text{AT}}(a), \rho(a)) \in S$ for all $a \in A$ (this is a trivial element). Thus, $(A, \eta_{\text{AT}}, \rho)$ is a good triple. Also, $C_{\eta_{\text{AT}}} = \text{AT}$ by definition of $\eta_{\text{AT}}$. Thus, Lemma 40 yields a TL(AT)-partition $\mathbf{K}$ of $\mathbb{A}^*$ such that for all $K \in \mathbf{K}$, there exists $B \in 2^A$ such that $K \subseteq \eta_{\text{AT}}^{-1}(B)$ and $(B, \tau(K)) \in S$. For each $B \in 2^A$, we let $\mathbf{K}_B = \{K \in \mathbf{K} \mid K \subseteq \eta_{\text{AT}}^{-1}(B)\}$. It follows from our hypotheses on $\mathbf{K}$ that $\mathbf{K}_B$ is a TL(AT)-partition of $\eta_{\text{AT}}^{-1}(B)$ such that $\tau(K) \in S(B)$ for all $K \in \mathbf{K}_B$. By closure under downset, we get $\mathcal{I}[\rho](\mathbf{K}_B) \subseteq S(B)$, completing the proof.

We now prove Lemma 40. We fix a good triple $(\mathbb{A}, \beta, \tau)$ and use induction on the size of the set $\{\beta(w) \mid w \in \mathbb{A}^+\} \subseteq 2^A$ to build a TL$(C_\beta)$-partition $\mathbf{K}$ of $\mathbb{A}^*$ satisfying (4).

Assume first that $\mathbb{A} = \emptyset$. Since $\mathbb{A}^* = \{\varepsilon\}$, it suffices to define $\mathbf{K} = \{\varepsilon\}$. This is clearly a TL$(C_\beta)$-partition of $\{\varepsilon\}$ (the language $\{\varepsilon\}$ is defined by the TL$[C_\beta]$ formula "$\neg\text{F}(\neg\text{max})$"). Moreover, $\{\varepsilon\} \subseteq \beta^{-1}(\emptyset)$ and $(\emptyset, \tau(\varepsilon)) = (\emptyset, 1_R) \in S$ since $S$ is TL(AT)-saturated for $\rho$ (this is the trivial element $(\eta_{\text{AT}}(\varepsilon), \rho(\varepsilon)) \in S$). Hence, $\mathbf{K}$ satisfies (4).

We assume from now on that $\mathbb{A} \neq \emptyset$. Consider the sets $D \in 2^A$ such that $D = \beta(\ell)$ for a letter $\ell \in \mathbb{A}$. We fix such a set $D \in 2^A$ which is minimal with respect to inclusion: there is no $\ell \in \mathbb{A}$ such that $\beta(\ell) \subseteq D$. Let $\mathbb{A}_D = \{\ell \in \mathbb{A} \mid \beta(\ell) = D\}$ and $\overline{\mathbb{A}}_D = \{\ell \in \mathbb{A} \mid \beta(\ell) \neq D\}$. Since $\mathbb{A} = \mathbb{A}_D \cup \overline{\mathbb{A}}_D$, we can split each word in $\mathbb{A}^*$ into two parts (each possibly empty): a prefix in $\mathbb{A}_D^*$ and a suffix in $(\overline{\mathbb{A}}_D^*\mathbb{A}_D^*)^*$ (starting at the first letter in $\overline{\mathbb{A}}_D^*$). We partition $\mathbb{A}_D^*$ and $(\overline{\mathbb{A}}_D^*\mathbb{A}_D^*)^*$ independently and combine the partitions to build that of $\mathbb{A}^*$.

**Step 1: partitioning $\mathbb{A}_D^*$.** We construct a TL(AT)-partition $\mathbf{U}$ of $\mathbb{A}_D^*$ satisfying (4). We rely on TL(AT)-operation (we cannot use induction as it may happen that $\mathbb{A}_D = \mathbb{A}$). Let $Q = S(D)$. We use $Q$ as an alphabet. Let $\mathbf{H}$ be an optimal TLX-cover of $Q^+$ for the full rating map $\pi_{R,Q}: 2^{Q^*} \to R$: we have $\mathcal{I}[\pi_{R,Q}](\mathbf{H}) = \mathcal{I}_{\text{TLX}}[Q^+, \pi_{R,Q}]$. Since TLX is a Boolean algebra and $Q^+ \in \text{TLX}$, we may assume without loss of generality that $\mathbf{H}$ is a partition of $Q^+$. Moreover, since $S$ is TL(AT)-saturated, TL(AT)-operation yields $\mathcal{I}[\pi_{R,Q}](\mathbf{H}) \subseteq S(D)$. We use $\mathbf{H}$ to build the desired TL$(C_\beta)$-partition $\mathbf{U}$ of $\mathbb{A}_D^*$. To this aim, we define a morphism $\delta: \mathbb{A}_D^* \to Q^*$. Let $\ell \in \mathbb{A}_D$. By definition of $\mathbb{A}_D$, we have $\beta(\ell) = D$. Since the triple $(\mathbb{A}, \beta, \tau)$ is good, this yields $(D, \tau(\ell)) \in S$. Thus, $\tau(\ell) \in S(D) = Q$ and we may define $\delta(\ell) = (\tau(\ell)) \in Q$ (here, $(\tau(\ell))$ is viewed as a letter of the alphabet $Q$). The fact is proved in Appendix ??.

**Fact 41.** Let $H \subseteq Q^*$. If $H \in \text{TLX}$, then $\delta^{-1}(H) \in \text{TL}(C_\beta)$.

Let $\mathbf{U} = \{\delta^{-1}(H) \mid H \in \mathbf{H}\} \cup \{\{\varepsilon\}\}$. Since $\mathbf{H}$ is a TLX-partition of $Q^+$ and $\delta: \mathbb{A}_D^* \to Q^*$ is a morphism, Fact 41 implies that $\mathbf{U}$ is TL$(C_\beta)$-partition of $\mathbb{A}_D^*$. We prove that it
satisfies (4). Let $U \in \mathbf{U}$. If $U = \{\varepsilon\}$, then $\{\varepsilon\} \subseteq \beta^{-1}(\emptyset)$ and $(\emptyset, \tau(\varepsilon)) = (\emptyset, 1_R) \in S$, as desired. Otherwise, $U = \delta^{-1}(H)$ for some $H \in \mathbf{H}$. Since $H \subseteq \mathcal{Q}^+$, this yields $U \subseteq \mathbb{A}_D^+$ and since $\beta(\ell) = D$ for all $\ell \in \mathbb{A}_D$, this implies that $U \subseteq \beta^{-1}(D)$. It now suffices to prove that $(D, \tau(U)) \in S$. We show that $\tau(U) \le \pi_{R,Q}(H)$. By definition, this implies that $\tau(U) \in \mathcal{I}[\pi_{R,Q}](\mathbf{H})$ and since we already know that $\mathcal{I}[\pi_{R,Q}](\mathbf{H}) \subseteq S(D)$, this yields $(D, \tau(U)) \in S$ as desired. Since $\tau$ is full, it suffices to prove that for every $w \in U$, we have $\tau(w) \le \pi_{R,Q}(H)$. Since $U = \delta^{-1}(H)$, we have $\delta(w) \in H$ which yields $\pi_{R,Q}(\delta(w)) \le \pi_{R,Q}(H)$. Moreover, it is immediate from the definition of $\delta$ that $\pi_{R,Q}(\delta(w)) = \tau(w)$. Hence, we obtain $\tau(w) \le \pi_{R,Q}(H)$, as desired.

**Step 2: partitioning $(\overline{\mathbb{A}}_D \mathbb{A}_D^*)^*$.** We reuse the TL$(\mathbb{C}_\beta)$-partition $\mathbf{U}$ of $\mathbb{A}_D^*$. We build a new good triple $(\mathbb{B}, \gamma, \zeta)$ and abstract the words in $(\overline{\mathbb{A}}_D \mathbb{A}_D^*)^*$ by words in $\mathbb{B}^*$. Let $\mathbb{B} = \overline{\mathbb{A}}_D \times \mathbf{U}$. We define a morphism $\gamma : \mathbb{B}^* \to 2^A$ and a full rating map $\zeta : 2^{\mathbb{B}^*} \to \mathbf{R}$. Consider a letter $(\ell, U) \in \overline{\mathbb{A}}_D \times \mathbf{U} = \mathbb{B}$. Since $\mathbf{U}$ satisfies (4) by definition, there exists $B_U \in 2^A$ such that $U \subseteq \beta^{-1}(B_U)$ and $(B_U, \tau(U)) \in S$. We define $\gamma((\ell, U)) = \beta(\ell) \cup B_U$ and $\zeta((\ell, U)) = \tau(\ell)\tau(U)$. Observe that since $(\beta(\ell), \tau(\ell)) \in S$ (recall that $(\mathbb{A}, \beta, \tau)$ is a good triple) and $(B_U, \tau(U)) \in S$, closure under multiplication for $S$ yields $(\gamma((\ell, U)), \zeta((\ell, U))) \in S$. Hence, $(\mathbb{B}, \gamma, \zeta)$ is a good triple. The next fact can be verified using the hypothesis that $D$ is a minimal set such that $D \in \{\beta(\ell) \mid \ell \in \mathbb{A}\}$ (the details are available in Appendix ??).

**Fact 42.** We have $\{\gamma(w) | w \in \mathbb{B}^+\} \subseteq \{\beta(w) | w \in \mathbb{A}^+\} \setminus \{D\}$.

Fact 42 yields $|\{\gamma(w) \mid w \in \mathbb{B}^+\}| < |\{\beta(w) \mid w \in \mathbb{A}^+\}|$. Therefore, induction in the proof of Lemma 40 yields a TL$(\mathbb{C}_\gamma)$-partition $\mathbb{K}_\mathbb{B}$ of $\mathbb{B}^*$ satisfying (4).

We use $\mathbb{K}_\mathbb{B}$ to build a TL$(\mathbb{C}_\beta)$-partition $\mathbf{V}$ of $(\overline{\mathbb{A}}_D \mathbb{A}_D^*)^*$ satisfying (4). We first define a map $\mu : (\overline{\mathbb{A}}_D \mathbb{A}_D^*)^* \to \mathbb{B}^*$. Let $w \in (\overline{\mathbb{A}}_D \mathbb{A}_D^*)^*$. We have $w = \ell_1 u_1 \cdots \ell_n u_n$ with $\ell_1, \dots, \ell_n \in \mathbb{A}_D$ and $u_1, \dots, u_n \in \mathbb{A}_D^*$. Recall that $\mathbf{U}$ is a partition of $\mathbb{A}_D^*$. Thus, for each $h \le n$, there exists a unique $U_h \in \mathbf{U}$ such that $u_h \in U_h$. We let $\mu(w) = (\ell_1, U_1) \cdots (\ell_n, U_n) \in \mathbb{B}^*$. The fact can be verified.

**Fact 43.** For every $w \in (\overline{\mathbb{A}}_D \mathbb{A}_D^*)^*$, we have $\beta(w) = \gamma(\mu(w))$ and $\tau(w) \le \zeta(\mu(w))$.

We say that a position $i \in \text{Pos}(w)$ is distinguished if $w[i] \in \overline{\mathbb{A}}_D \cup \{\text{min}, \text{max}\}$. There exists a natural bijection between the distinguished positions of $w$ and all positions of $\mu(w)$. We abuse terminology and also write $\mu$ for the bijection: we have $\mu(0) = 0$, $\mu(|w|+1) = |w|+1$ and if $i \in \text{Pos}(w)$ is the distinguished position of $w$ corresponding to the highlighted letter $\ell_h \in \overline{\mathbb{A}}_D$, then $\mu(i) = h$. The following fact can be verified using the hypothesis that $D$ is a minimal set such that $D \in \{\beta(\ell) \mid \ell \in \mathbb{A}\}$ (we present a proof in Appendix ??).

**Fact 44.** Let $w \in (\overline{\mathbb{A}}_D \mathbb{A}_D^*)^*$ and $i, j \in \text{Pos}(w)$ such that $i < j$. Then, there exists no distinguished position $k \in \text{Pos}(w)$ such that $i < k < j$ if and only if $\beta(w(i, j)) \in \{D, \emptyset\}$.

For every letter $(\ell, U) \in \mathbb{B} = \overline{\mathbb{A}}_D \times \mathbf{U}$, Fact 44 can be used to construct a formula $\psi_{\ell, U} \in \text{TL}(\mathbb{C}_\beta)$ such that for every $w \in (\overline{\mathbb{A}}_D \mathbb{A}_D^*)^*$ and every distinguished position $i \in \text{Pos}(w)$, we have $w, i \models \psi_{\ell, U} \iff \mu(i)$ has label $(\ell, U)$. Indeed, $\psi_{\ell, U}$ has to check that $i$ has label $\ell$ (this is achieved by the TL[$\mathbb{C}_\beta$] formula “$\ell$”) and that $w(i, j) \in U$ for the next distinguished position $j$ of $w$. By hypothesis on $\mathbf{U}$, $\mathbf{U}$ is defined by a TL[$\mathbb{C}_\beta$] formula $\varphi_{\mathbf{U}}$. In view of Fact 44, we can modify $\varphi_{\mathbf{U}}$ in order to constrain its evaluation so that it stays in the infinx $w(i, j) \in \mathbb{A}_D^*$. Roughly speaking, this boils down to modifying all occurrences of $F_L$ and $P_L$ for $L \in \mathbb{C}_\beta$: one replaces $L$ by $L \cap \beta^{-1}(\{D, \emptyset\}) \in \mathbb{C}_\beta$. We detail this construction in Appendix ??, where it is used to prove the following lemma.

**Lemma 45.** For all $K \in \text{TL}(\mathbb{C}_\gamma)$, $\mu^{-1}(K) \in \text{TL}(\mathbb{C}_\beta)$.

We let $\mathbf{V} = \{\mu^{-1}(K) \mid K \in \mathbb{K}_\mathbb{B}\}$. Since $\mathbb{K}_\mathbb{B}$ is a TL$(\mathbb{C}_\gamma)$-partition of $\mathbb{B}^*$, $\mathbf{V}$ is a TL$(\mathbb{C}_\beta)$-partition of $(\overline{\mathbb{A}}_D \mathbb{A}_D^*)^*$ by Lemma 45. Let us verify that it satisfies (4). Let $V \in \mathbf{V}$. By definition, $V = \mu^{-1}(K)$ for some $K \in \mathbb{K}_\mathbb{B}$. Hence, since $\mathbb{K}_\mathbb{B}$ satisfies (4), we get $B \in 2^A$ such that $K \subseteq \gamma^{-1}(B)$ and $(B, \zeta(K)) \in S$. Since $K \subseteq \gamma^{-1}(B)$, Fact 43 implies that $V = \mu^{-1}(K) \subseteq \beta^{-1}(B)$. Moreover, Fact 45 also implies that $\tau(V) = \tau(\mu^{-1}(K)) \le \zeta(K)$. Altogether, we obtain $(B, \tau(V)) \in S$ by closure under downset. Hence, (4) holds.

**Step 3: partitioning $\mathbb{A}^*$.** We have two TL$(\mathbb{C}_\beta)$-partitions $\mathbf{U}$ and $\mathbf{V}$ of $\mathbb{A}_D^*$ and $(\overline{\mathbb{A}}_D \mathbb{A}_D^*)^*$ respectively satisfying (4). We combine them using a standard concatenation principle for unary temporal logic (see Appendix ?? for the proof).

**Lemma 46.** Let $U, V \in \text{TL}(\mathbb{C}_\beta)$ such that $U \subseteq \mathbb{A}_D^*$ and $V \subseteq (\overline{\mathbb{A}}_D \mathbb{A}_D^*)^*$. Then, $UV \in \text{TL}(\mathbb{C}_\beta)$.

We now build the TL$(\mathbb{C}_\beta)$-partition $\mathbf{K}$ of $\mathbb{A}^*$ described in Lemma 40. We let $\mathbf{K} = \{UV \mid U \in \mathbf{U}$ and $V \in \mathbf{V}\}$. Since $\mathbf{U}$ and $\mathbf{V}$ are partitions of $\mathbb{A}_D^*$ and $(\overline{\mathbb{A}}_D \mathbb{A}_D^*)^*$ and $\mathbb{A}_D \cap \overline{\mathbb{A}}_D = \emptyset$, one can verify that $\mathbf{K}$ is a partition of $\mathbb{A}^* = \mathbb{A}_D^*(\overline{\mathbb{A}}_D \mathbb{A}_D^*)^*$. Thus, it is a TL$(\mathbb{C}_\beta)$-partition of $\mathbb{A}^*$ by Lemma 46.

It remains to prove that $\mathbf{K}$ satisfies (4). Let $K \in \mathbf{K}$. We have $K = UV$ for $U \in \mathbf{U}$ and $V \in \mathbf{V}$. Since $\mathbf{U}, \mathbf{V}$ satisfy (4), we get $B, C \in 2^A$ such that $U \subseteq \beta^{-1}(B)$, $V \subseteq \beta^{-1}(C)$, $(B, \tau(U)) \in S$ and $(C, \tau(V)) \in S$. Consequently, we obtain $K = UV \subseteq \beta^{-1}(B \cup C)$ and since $S$ is closed under multiplication, we get $(B \cup C, \tau(UV)) \in S$ as desired. $\square$

VIII. CONCLUSION

We defined navigational hierarchies using the “unary temporal logic” operator $C \mapsto \text{TL}(C)$. We focused on bases of the form $C = \mathcal{G}$ or $\mathcal{G}^+$, where $\mathcal{G}$ is a group prevariety. In this context, we proved that the navigational hierarchies of basis $C$ are strict and strictly intertwined, and we compared them with the associated concatenation hierarchies. Additionally, we proved that if $\mathcal{G}$ has decidable separation, then membership is decidable for levels one and two in both hierarchies. Our main theorem provides a stronger result for the particular bases ST and DD = ST$^+$. Specifically, it implies that level two in both hierarchies has decidable covering, which in turn ensures that level three has decidable membership.
Several follow-up questions arise. A natural one is whether our results can be extended to higher levels in navigational hierarchies. Addressing this would require studying the operator $C \mapsto TL(C)$ in a broader context, as our main theorem heavily relies on the specific properties of the class AT. Another question is to generalize the link existing between the hierarchies of bases ST and DD. As seen in Section VII, we have $TL_2(DD) = TL_2(ST) \circ SU$ and we used this connection to get the decidability of covering for $TL_2(DD)$. It turns out that this can be generalized: we have $TL_n(DD) = TL_n(ST) \circ SU$ for all $n \ge 1$. We leave the proof for further work.

## REFERENCES

[1] R. McNaughton and S. A. Papert, *Counter-Free Automata*. MIT Press, 1971.

[2] H. W. Kamp, "Tense logic and the theory of linear order," PhD thesis, Computer Science Department, University of California at Los Angeles, USA, 1968.

[3] M. P. Schützenberger, "On finite monoids having only trivial subgroups," *Information and Control*, vol. 8, no. 2, pp. 190-194, 1965.

[4] J. A. Brzozowski and R. S. Cohen, "Dot-depth of star-free events," *Journal of Computer and System Sciences*, vol. 5, no. 1, pp. 1-16, 1971.

[5] J. A. Brzozowski and R. Knast, "The dot-depth hierarchy of star-free languages is infinite," *Journal of Computer and System Sciences*, vol. 16, no. 1, pp. 37-55, 1978.

[6] H. Straubing, "A generalization of the schützenberger product of finite monoids," *Theoretical Computer Science*, vol. 13, no. 2, pp. 137-150, 1981.

[7] D. Thérien, "Classification of finite monoids: The language approach," *Theoretical Computer Science*, vol. 14, no. 2, pp. 195-208, 1981.

[8] S. W. Margolis and J. Pin, "Products of group languages," in *FCT'85*. Springer, 1985.

[9] G. Thierrin, "Permutation automata," *Theory of Computing Systems*, vol. 2, no. 1, pp. 83-90, 1968.

[10] L. Chaubard, J.-É. Pin, and H. Straubing, "First order formulas with modular predicates," in *Proceedings of the 21st IEEE Symposium on Logic in Computer Science (LICS'06)*, 2006, pp. 211-220.

[11] T. Place and M. Zeitoun, "Generic results for concatenation hierarchies," *Theory of Computing Systems (ToCS)*, vol. 63, no. 4, pp. 849-901, 2019, selected papers from CSR'17.

[12] W. Thomas, "Classifying regular events in symbolic logic," *Journal of Computer and System Sciences*, vol. 25, no. 3, pp. 360-376, 1982.

[13] T. 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.

[14] T. Place and M. Zeitoun, "All about unambiguous polynomial closure," *TheoretiCS*, vol. 2, no. 11, pp. 1-74, 2023. [Online]. Available: https://theoretics.episciences.org/12847

[15] I. Simon, "Piecewise testable events," in *Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages*. Springer, 1975, pp. 214-222.

[16] R. Knast, "A semigroup characterization of dot-depth one languages," *RAIRO - Theoretical Informatics and Applications*, vol. 17, no. 4, pp. 321-330, 1983.

[17] T. Place and M. Zeitoun, "Going higher in first-order quantifier alternation hierarchies on words," *Journal of the ACM*, vol. 66, no. 2, pp. 12:1-12:65, 2019.

[18] —, "Dot-depth three, return of the J-class," in *Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024*, Tallinn, Estonia, July 8-11, 2024, P. Sobocinski, U. D. Lago, and J. Esparza, Eds. ACM, 2024, pp. 64:1-64:15. [Online]. Available: https://doi.org/10.1145/3661814.3662082

[19] N. Immerman and P. Weis, "Structure theorem and strict alternation hierarchy for fo2 on words," in *Proceedings of the 16th International Conference on Computer Science Logic*, ser. CSL'07, 2007, pp. 343-357.

[20] A. Krebs and H. Straubing, "An effective characterization of the alternation hierarchy in two-variable logic," in *Proceedings of the 32nd Annual Conference on Foundations of Software Technology and Theoretical Computer Science*, ser. FSTTCS'12, 2012, pp. 86-98.

[21] M. Kufleitner and P. Weil, "The FO2 alternation hierarchy is decidable," in *Proceedings of the 21st International Conference on Computer Science Logic*, ser. CSL'12, 2012, pp. 426-439.

[22] K. Etessami, M. Y. Vardi, and T. Wilke, "First-order logic with two variables and unary temporal logic," *Information and Computation*, vol. 179, no. 2, pp. 279-295, 2002.

[23] D. Thérien and T. 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*. New York, NY, USA: ACM, 1998, pp. 234-240.

[24] V. Diekert, P. Gastin, and M. Kufleitner, "A survey on small fragments of first-order logic over finite words," *International Journal of Foundations of Computer Science*, vol. 19, no. 3, pp. 513-548, 2008.

[25] L. Dartois and C. 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*, ser. Leibniz International Proceedings in Informatics (LIPIcs), vol. 20. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2013, pp. 329-340.

[26] A. Krebs, K. Lodaya, P. K. Pandya, and H. Straubing, "Two-variable logic with a between relation," in *Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'16*, 2016, pp. 106-115.

[27] —, "An algebraic decision procedure for two-variable logic with a between relation," in *27th EACSL Annual Conference on Computer Science Logic, CSL'18*, ser. Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018.

[28] —, "Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership," *Logical Methods in Computer Science*, vol. 16, no. 3, 2020.

[29] T. Place and M. Zeitoun, "A generic characterization of generalized unary temporal logic and two-variable first-order logic," in *Proceedings of the 32nd EACSL Annual Conference on Computer Science Logic*, ser. CSL'24, 2024.

[30] M. P. Schützenberger, "Sur le produit de concaténation non ambigu," *Semigroup Forum*, vol. 13, pp. 47-75, 1976.

[31] J.-E. Pin and P. Weil, "Polynomial closure and unambiguous product," *Theory of Computing Systems*, vol. 30, no. 4, pp. 383-422, 1997.

[32] T. Place and M. Zeitoun, "Separation and covering for group based concatenation hierarchies," in *Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'19*. IEEE Computer Society, 2019, pp. 1-13.

[33] C. J. Ash, "Inevitable graphs: a proof of the type II conjecture and some related decision procedures," *International Journal of Algebra and Computation*, vol. 1, no. 1, pp. 127-146, 1991.

[34] T. Place and M. Zeitoun, "Group separation strikes back," in *38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'23*. IEEE Computer Society, 2023, pp. 1-13. [Online]. Available: https://doi.ieeecomputersociety.org/10.1109/LICS56636.2023.10175683

[35] —, "Separation and the successor relation," in *32nd International Symposium on Theoretical Aspects of Computer Science, STACS'15*, ser. Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015, pp. 662-675.

[36] H. Straubing, "Finite semigroup varieties of the form $V \ast D$," *Journal of Pure and Applied Algebra*, vol. 36, pp. 53-94, 1985.

[37] T. Place and M. Zeitoun, "The covering problem," *Logical Methods in Computer Science*, vol. 14, no. 3, 2018.

[38] J. A. Brzozowski and I. Simon, "Characterizations of locally testable events," *Discrete Mathematics*, vol. 4, no. 3, pp. 243-271, 1973.

[39] Y. Zalcstein, "Locally testable languages," *Journal of Computer and System Sciences*, vol. 6, no. 2, pp. 151-167, 1972.

[40] M. Arfi, "Polynomial operations on rational languages," in *Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science, STACS'87*, ser. Lect. Notes Comp. Sci., vol. 247. Springer, 1987, pp. 198-206.

[41] J.-E. 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*, ser. Lect. Notes Comp. Sci., vol. 7907. Springer, 2013, pp. 31-45.

[42] M. Arfi, "Opérations polynomiales et hiérarchies de concaténation," *Theoretical Computer Science*, vol. 91, no. 1, pp. 71-84, 1991.

[43] A. Maciel, P. Péladeau, and D. Thérien, "Programs over semigroups of dot-depth one," *Theoretical Computer Science*, vol. 245, no. 1, pp. 135-148, 2000.
[44] M. Kufleitner and T. Walter, "One quantifier alternation in first-order logic with modular predicates." *RAIRO Theoretical Informatics and Applications*, vol. 49, no. 1, pp. 1-22, 2015.

[45] M. Delgado, "Abelian poinlikes of a monoid," *Semigroup Forum*, vol. 56, no. 3, pp. 339-361, 1998.

[46] T. Place and M. Zeitoun, "A generic polynomial time approach to separation by first-order logic without quantifier alternation," in *42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022, December 18-20, 2022, IIT Madras, Chennai, India*, ser. LIPIcs, vol. 250. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, pp. 43:1-43:22.

[47] P. Weil, "Some results on the dot-depth hierarchy," *Semigroup Forum*, vol. 46, no. 1, pp. 352-370, 1993.

[48] T. Place and M. Zeitoun, "Adding successor: A transfer theorem for separation and covering," *ACM Transactions on Computational Logic*, vol. 21, no. 2, pp. 9:1-9:45, 2020.

[49] ——, "Separating regular languages with first-order logic," *Logical Methods in Computer Science*, vol. 12, no. 1, 2016.