We first apply Lemma 10.13 to complete the proof of Proposition 10.12. We define $L = \eta^{-1}(1_G)$. It is clear that $\epsilon \in L$ and $L \in \mathcal{G}$ since $\eta$ is a $\mathcal{G}$-morphism. Moreover, since $S' = \text{SF}$-saturated for $\eta$ and $\rho$, Proposition 9.6 yields an $\eta$-pointed SF($\mathcal{G}$)-cover $\mathbf{H}$ of $A^*$ such that $\mathcal{P}[\eta, \rho](\mathbf{H}) \subseteq S'$. We define $\mathbf{K} = \{K \mid (1_G, K) \in \mathbf{H}\}$. By definition, $\mathbf{K}$ is an SF($\mathcal{G}$)-cover of $L = \eta^{-1}(1_G)$. Moreover, since $S = \{r \mid (1_G, r) \in S'\}$ and $\mathcal{P}[\eta, \rho](\mathbf{H}) \subseteq S'$, it is immediate from the definition that $\mathcal{J}[\rho](\mathbf{K}) \subseteq S$, which completes the proof.

It remains to prove Lemma 10.13. Let us first define $\eta$. We let $L$ be an optimal $\mathcal{G}$-identity for the nice multiplicative rating map $\mu_{\rho,S} : 2^{A^*} \to 2^R$. That is, we have $L \in \mathcal{G}$, $\epsilon \in L$ and $\mu_{\rho,S}(L) = \mathbb{1}_{\mathcal{G}}[\mu_{\rho,S}]$. Proposition 2.4 yields a $\mathcal{G}$-morphism $\eta : A^* \to G$ recognizing $L$. By hypothesis on $\mathcal{G}$, Lemma 3.5 implies that $G$ is a group. Also since $\epsilon \in L$ and $L$ is recognized by $\eta$, it is immediate that $\eta^{-1}(1_G) \subseteq L$. Finally, we define $S' \subseteq G \times R$ as the following set:

$$S' = \{(1_G, s) \mid s \in S\} \cup \{(t, r) \mid r \in \downarrow_R \mu_{\rho,S}(\eta^{-1}(t))\}.$$

Let us first prove that $S = \{r \mid (1_G, r) \in S'\}$. The left to right inclusion is immediate by definition: if $r \in S$, then $(1_G, r) \in S'$. We turn to the converse inclusion. Let $r \in R$ such that $(1_G, r) \in S'$. By definition of $S'$, either $r \in S$ or $r \in \downarrow_R \mu_{\rho,S}(\eta^{-1}(1_G))$. In the former case, we are done. Hence, we assume that $r \in \downarrow_R \mu_{\rho,S}(\eta^{-1}(1_G))$. By definition, $\eta^{-1}(1_G) \subseteq L$ ($L$ is recognized by $\eta$ and $\epsilon \in L$). Hence, since $\mu_{\rho,S}(L) = \mathbb{1}_{\mathcal{G}}[\mu_{\rho,S}]$ we get $r \in \downarrow_R \mathbb{1}_{\mathcal{G}}[\mu_{\rho,S}]$. Finally, since $S$ is SF-complete for $\mathcal{G}$ and $\rho$, we have $\downarrow_R \mathbb{1}_{\mathcal{G}}[\mu_{\rho,S}] \subseteq S$ and we get $r \in S$, as desired.

It remains to prove that $S'$ is SF-saturated for $\eta$ and $\rho$. This involves four properties. Let us start with trivial elements. Consider $w \in A^*$, we show that $(\eta(w), \rho(w)) \in S'$. By definition of $S'$, it suffices to prove that $\rho(w) \in \downarrow_R \mu_{\rho,S}(\eta^{-1}(\eta(w)))$. Clearly, $w \in \eta^{-1}(\eta(w))$. Hence, it now suffices to prove that $\rho(w) \in \mu_{\rho,S}(w)$. If $w = \epsilon$, then $\rho(w) = 1_R$ and $\mu_{\rho,S}(\epsilon) = \{1_R\}$ (this is the neutral element of $2^R$). Thus, it is immediate that $\rho(w) \in \mu_{\rho,S}(w)$. Assume now that $w \in A^+$. We have $a_1, \dots, a_n \in A$ such that $w = a_1 \cdots a_n$. Since $S$ is SF-complete, we have $1_R \in S$ (see Remark 10.7). Hence, we get $\rho(a_i) \in S \cdot \{\rho(a_i)\} \cdot S = \mu_{\rho,S}(a_i)$ for every $i \le n$. It then follows that $\rho(w) \in \mu_{\rho,S}(w)$ which concludes this case.

We turn to downset. Consider $(t, r) \in S'$ and $q \le r$. We show that $(t, q) \in S'$. By definition, there are two possible cases. First, it may happen that $t = 1_G$ and $r \in S$. In that case, $q \in S$ since $\downarrow_R S = S$ ($S$ is complete) and we get that $(1_G, q) \in S'$ by definition. Otherwise, $r \in \downarrow_R \mu_{\rho,S}(\eta^{-1}(t))$ which yields $q \in \downarrow_R \mu_{\rho,S}(\eta^{-1}(t))$ as well and we get $(t, q) \in S'$, concluding the proof for downset.

We turn to closure under multiplication. Let $(s, q), (t, r) \in S'$. We have to show that $(st, qr) \in S'$. There are several cases. Assume first that $s = t = 1_G$. In that case, we proved above that $q, r \in S$. Since $S$ is complete, this implies that $qr \in S$ and we obtain that $(st, qr) = (1_G, qr) \in S'$. We now assume that either $s$ or $t$ is distinct from $1_G$ for the remainder of this case. If both $s$ and $t$ are distinct from $1_G$, we have $q \in \downarrow_R \mu_{\rho,S}(\eta^{-1}(s))$ and $r \in \downarrow_R \mu_{\rho,S}(\eta^{-1}(t))$ by definition of $S'$. It follows that $qr \in \downarrow_R \mu_{\rho,S}(\eta^{-1}(s)\eta^{-1}(t))$. Since $\eta^{-1}(s)\eta^{-1}(t) \subseteq \eta^{-1}(st)$, this yields $qr \in \downarrow_R \mu_{\rho,S}(\eta^{-1}(st))$ and we get $(st, qr) \in S'$. Finally, we handle the case when $s = 1_G$ and $t \ne 1_G$ (the symmetrical case is left to the reader). Since $S = S'(1_G)$, the hypothesis that $t = 1_G$ yields $q \in S$. Moreover, we have $r \in \downarrow_R \mu_{\rho,S}(\eta^{-1}(t))$ since $t \ne 1_G$. Note that $t \ne 1_G$ also implies that $\eta^{-1}(t) \subseteq A^+$. Thus, since $SS \subseteq S$ ($S$ is complete), one can check from the definition of $\mu_{\rho,S}$ that $S \cdot \mu_{\rho,S}(\eta^{-1}(t)) \subseteq \mu_{\rho,S}(\eta^{-1}(t))$. Thus, since $q \in S$ and $r \in \downarrow_R \mu_{\rho,S}(\eta^{-1}(t))$, we obtain that $qr \in \downarrow_R \mu_{\rho,S}(\eta^{-1}(t))$. Finally, $1_G t = t$. Thus, $qr \in \downarrow_R \mu_{\rho,S}(\eta^{-1}(1_G t))$ which yields $(1_G t, qr) \in S'$, concluding the proof.

It remains to prove that $S'$ satisfies SF-closure. Since $G$ is a group, $1_G$ is the only idempotent of $G$. Hence, we have to show that for $r \in R$ such that $(1_G, r) \in S'$, we have $(1_G, r^\omega + r^{\omega+1}) \in S'$. Since $S = \{r \mid (1_G, r) \in S'\}$, we know that $r \in S$. Hence, since $S$ is SF-complete, we get $r^\omega + r^{\omega+1} \in S$ which implies $(1_G, r^\omega + r^{\omega+1}) \in S'$ since $S = \{r \mid (1_G, r) \in S'\}$. This completes the proof. □
We can now combine Proposition 10.10 and Proposition 10.12 to prove Theorem 10.8.

PROOF OF THEOREM 10.8. Let $\mathcal{G}$ be a group prevariety and $\rho : 2^{\mathcal{G}} \to \mathcal{R}$ be a nice multiplicative rating map. We prove that $\mathring{\mathcal{I}}_{\mathcal{G}}[\xi_{\mathcal{SF}(\mathcal{G})}[\rho]]$ is the least $\mathcal{SF}$-complete subset of $\mathcal{R}$ for $\mathcal{G}$ and $\rho$. Proposition 10.10 implies that $\mathring{\mathcal{I}}_{\mathcal{G}}[\xi_{\mathcal{SF}(\mathcal{G})}[\rho]]$ is $\mathcal{SF}$-complete. We show that it is the least such set.

Let $S \subseteq \mathcal{R}$ be $\mathcal{SF}$-complete for $\mathcal{G}$ and $\rho$. We prove that $\mathring{\mathcal{I}}_{\mathcal{G}}[\xi_{\mathcal{SF}(\mathcal{G})}[\rho]] \subseteq S$. Proposition 10.12 yields $L \in \mathcal{G}$ such that $\varepsilon \in L$ and an $\mathcal{SF}(\mathcal{G})$-cover $\mathbf{K}$ of $L$ such that $\mathcal{J}[\rho](\mathbf{K}) \subseteq S$. By definition of optimal $\mathcal{G}$-identities, we have $\mathring{\mathcal{I}}_{\mathcal{G}}[\xi_{\mathcal{SF}(\mathcal{G})}[\rho]] \subseteq \xi_{\mathcal{SF}(\mathcal{G})}[\rho](L)$. Hence, it suffices to show that $\xi_{\mathcal{SF}(\mathcal{G})}[\rho](L) \subseteq S$. By definition, we have $\xi_{\mathcal{SF}(\mathcal{G})}[\rho](L) = \mathcal{J}_{\mathcal{SF}(\mathcal{G})}[L, \rho] \subseteq \mathcal{J}[\rho](\mathbf{K}) \subseteq S$. This concludes the proof. $\square$

# 11 Conclusion

We investigated the star-free closure operator $\mathcal{C} \mapsto \mathcal{SF}(\mathcal{C})$ applied to prevarieties of regular languages. First, we presented several equivalent ways of defining $\mathcal{SF}(\mathcal{C})$, including a generic algebraic characterization that generalizes earlier results [41, 45, 29]. It implies that $\mathcal{SF}(\mathcal{C})$-membership is decidable when $\mathcal{C}$-separation is decidable. A key proof ingredient for all these results is an alternative definition of star-free closure: the operator $\mathcal{C} \mapsto \mathcal{SD}(\mathcal{C})$, which we prove to coincide with star-free closure. This correspondence generalizes the work of Schützenberger [42] who introduced a single class $\mathcal{SD}$ (i.e., $\mathcal{SD}(\mathcal{ST})$) corresponding to the star-free languages (i.e., $\mathcal{SF}(\mathcal{ST}))$. Moreover, we presented two generic logical characterizations of star-free closure. The first one is based on first-order logic and generalizes the work of McNaughton and Papert on the star-free languages [24]: we have $\mathcal{SF}(\mathcal{C}) = \text{FO}(\mathbb{I}_{\mathcal{C}})$ for every prevariety $\mathcal{C}$. The second one is based on linear temporal logic and generalizes Kamp's theorem [17]: we have $\mathcal{SF}(\mathcal{C}) = \text{LTL}(\mathcal{C}) = \text{LTLP}(\mathcal{C})$ for every prevariety $\mathcal{C}$. Finally, we gave two generic characterizations of optimal imprints for $\mathcal{SF}(\mathcal{C})$, for two particular kinds of prevariety $\mathcal{C}$: the *finite prevarieties* and the *group prevarieties*. They imply that $\mathcal{SF}(\mathcal{C})$ has decidable separation and covering when $\mathcal{C}$ is a finite prevariety and that $\mathcal{SF}(\mathcal{G})$ has decidable separation and covering when $\mathcal{G}$ is a group prevariety with decidable separation.

# References

[1] Douglas Albert, Robert Baldinger, and John Rhodes. "Undecidability of the Identity Problem for Finite Semigroups". In: *The Journal of Symbolic Logic* 57.1 (1992), pp. 179–192.

[2] Jorge Almeida. "Some Algorithmic Problems for Pseudovarieties". In: *Publicaciones Matemáticas Debrecen* 54 (1999), pp. 531–552.

[3] Christopher J. Ash. "Inevitable Graphs: a Proof of the Type II Conjecture and some Related Decision Procedures". In: *International Journal of Algebra and Computation* 1.1 (1991), pp. 127–146.

[4] David A. Mix Barrington et al. "Regular languages in NC1". In: *Journal of Computer and System Sciences* 44.3 (1992), pp. 478–499.

[5] Jean Berstel, Dominique Perrin, and Christophe Reutenauer. *Codes and Automata*. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2009.

[6] Laura Chaubard, Jean-Éric Pin, and Howard Straubing. "First Order Formulas with Modular Predicates". In: *Proc. 21th IEEE Symposium on Logic in Computer Science, LICS'06*. 2006, pp. 211–220.

[7] Luc Dartois and Charles Paperman. "Two-variable first order logic with modular predicates over words". In: *STACS'13*. Vol. 20. Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 329–340.

[8] Manuel Delgado. "Abelian Poinlikes of a Monoid". In: *Semigroup Forum* 56.3 (1998), pp. 339–361.
[9] Volker Diekert and Manfred Kufleitner. "Omega-Rational Expressions with Bounded Synchronization Delay". In: *Theory Comput. Syst.* 56.4 (2015), pp. 686-696.

[10] Volker Diekert and Tobias Walter. "Characterizing classes of regular languages using prefix codes of bounded synchronization delay". In: *Proc. 43rd International Colloquium on Automata, Languages, and Programming, ICALP'16*. 2016, 129:1-129:14.

[11] Volker Diekert and Tobias Walter. "Characterizing classes of regular languages using prefix codes of bounded synchronization delay". In: *IJAC* 27.6 (2017), pp. 561-590.

[12] Samuel Eilenberg. *Automata, Languages, and Machines*. Vol. B. Academic Press, Inc., 1976.

[13] Paul Gastin and Dietrich Kuske. "Satisfiability and Model Checking for MSO-Definable Temporal Logics Are in PSPACE". In: *CONCUR'03*. Springer, 2003, pp. 222-236.

[14] Christian Glaßer and Heinz Schmitz. "Languages of Dot-Depth 3/2". In: *Theory of Computing Systems* 42.2 (2007), pp. 256-286.

[15] Karsten Henckell. "Pointlike sets: the finest aperiodic cover of a finite semigroup". In: *Journal of Pure Applied Algebra* 55.1-2 (1988), pp. 85-126.

[16] Karsten Henckell et al. "Ash's type II theorem, profinite topology and Malcev products". In: *International Journal of Algebra and Computation* 1 (1991), pp. 411-436.

[17] Hans W. Kamp. "Tense Logic and the Theory of Linear Order". PhD thesis. Computer Science Department, University of California at Los Angeles, USA, 1968.

[18] Joel Karnofsky and John Rhodes. "Decidability of complexity one-half for finite semigroups". In: *Semigroup Forum* 24.1 (1982), pp. 55-66.

[19] Robert Knast. "A Semigroup Characterization of Dot-Depth One Languages". In: *RAIRO - Theoretical Informatics and Applications* 17.4 (1983), pp. 321-330.

[20] Andreas Krebs et al. "Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership". In: *Logical Methods in Computer Science* 16.3 (2020).

[21] Manfred Kufleitner and Tobias Walter. "One Quantifier Alternation in First-Order Logic with Modular Predicates". In: *RAIRO - Theoretical Informatics and Applications* 49 (2013), pp. 1-22.

[22] D. Lippert and Wolfgang Thomas. "Relativized star-free expressions, first-order logic, and a concatenation game". In: *Semigroups Theory and Applications*. Springer, 1988, pp. 194-204.

[23] Stuart Margolis and Jean-Éric Pin. "Product of Group Languages". In: *FCT Conference*. Vol. 199. Springer, 1985, pp. 285-299.

[24] Robert McNaughton and Seymour A. Papert. *Counter-Free Automata*. MIT Press, 1971.

[25] Jean-Éric Pin. "Bridges for Concatenation Hierarchies". In: *Proc. 25th International Colloquium on Automata, Languages and Programming, ICALP'98*. Springer, 1998, pp. 431-442.

[26] Jean-Éric Pin. "Mathematical Foundations of Automata Theory". In preparation. 2025. url: http://www.irif.fr/~jep/PDF/MPRI/MPRI.pdf.

[27] Jean-Éric Pin. "PG = BG, a success story". In: *NATO Advanced Study Institute, Semigroups, Formal Languages and Groups* (1995), pp. 33-47.

[28] Jean-Éric Pin. "The dot-depth hierarchy, 45 years later". In: *The Role of Theory in Computer Science. Essays Dedicated to Janusz Brzozowski*. World Scientific, 2017. Chap. 8, pp. 177-202.

[29] Jean-Éric Pin, Howard Straubing, and Denis Thérien. "Locally trivial categories and unambiguous concatenation". In: *Journal of Pure and Applied Algebra* 52.3 (1988), pp. 297-311.

[30] Jean-Éric Pin and Pascal Weil. "Polynomial Closure and Unambiguous Product". In: *Theory of Computing Systems* 30.4 (1997), pp. 383-422.

[31] Thomas Place. "Separating regular languages with two quantifier alternations". In: *Logical Methods in Computer Science* 14.4 (2018).

[32] Thomas Place and Marc Zeitoun. "All about unambiguous polynomial closure". In: *TheoretiCS* 2.11 (2023), pp. 1-74. doi: 10.46298/theoretics.23.11.
[33] Thomas Place and Marc Zeitoun. "Generic results for concatenation hierarchies". In: *Theory of Computing Systems (ToCS)* 63.4 (2019). Selected papers from CSR'17, pp. 849–901.

[34] Thomas Place and Marc Zeitoun. "Group separation strikes back". In: *Proc. 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'23*. 2023.

[35] Thomas Place and Marc Zeitoun. "On All Things Star-Free". In: *Proc. 46th International Colloquium on Automata, Languages, and Programming, ICALP'19*. 2019, 126:1–126:14.

[36] Thomas Place and Marc Zeitoun. "Separating Regular Languages with First-Order Logic". In: *Logical Methods in Computer Science* 12.1 (2016).

[37] Thomas Place and Marc Zeitoun. "Separating Regular Languages with First-order Logic". In: *Proc. 23rd EACSL Annual Conference on Computer Science Logic (CSL'14) and 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'14*. ACM, 2014, 75:1–75:10.

[38] Thomas Place and Marc Zeitoun. "Separation and covering for group based concatenation hierarchies". In: *Proc. 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'19*. 2019, pp. 1–13.

[39] Thomas Place and Marc Zeitoun. "Separation for dot-depth two". In: *Logical Methods in Computer Science* 17.3 (2021).

[40] Thomas Place and Marc Zeitoun. "The Covering Problem". In: *Logical Methods in Computer Science* 14.3 (2018).

[41] Marcel Paul Schützenberger. "On Finite Monoids Having Only Trivial Subgroups". In: *Information and Control* 8.2 (1965), pp. 190–194.

[42] Marcel Paul Schützenberger. "Sur certaines opérations de fermeture dans les langages ra- tionnels". In: *Symposia Mathematica* XV (1975), pp. 245–253.

[43] Imre Simon. "Piecewise Testable Events". In: *Proc. 2nd GI Conference on Automata Theory and Formal Languages*. Springer, 1975, pp. 214–222.

[44] Howard Straubing. "A Generalization of the Schützenberger Product of Finite Monoids". In: *Theoretical Computer Science* 13.2 (1981), pp. 137–150.

[45] Howard Straubing. "Aperiodic homomorphisms and the concatenation product of recognizable sets". In: *Journal of Pure and Applied Algebra* 15.3 (1979), pp. 319–327.

[46] Howard Straubing. "On Logical Descriptions of Regular Languages". In: *LATIN 2002: Theoretical Informatics, 5th Latin American Symposium*. 2002, pp. 528–538.

[47] Howard Straubing and Pascal Weil. "Varieties". In: *Handbook of Automata Theory*. Ed. by Jean-Éric Pin. European Mathematical Society Publishing House, 2021, pp. 569–614.

[48] Denis Thérien. "Classification of Finite Monoids: The Language Approach". In: *Theoretical Computer Science* 14.2 (1981), pp. 195–208.

[49] Denis Thérien and Thomas Wilke. "Over Words, Two Variables Are As Powerful As One Quantifier Alternation". In: *Proc. 30th Annual ACM Symposium on Theory of Computing*. STOC'98. ACM, 1998, pp. 234–240.

[50] Gabriel Thierrin. "Permutation automata". In: *Theory of Computing Systems* 2.1 (1968), pp. 83–90.

[51] Thomas Wilke. "Classifying Discrete Temporal Properties". In: *Proc. 16th Annual Conference on Theoretical Aspects of Computer Science*. STACS'99. Springer, 1999, pp. 32–46.
# Appendix

We present the proofs of results omitted from the main text due to space constraints. Each statement is restated before its proof.

## A Proofs of Section 2

This appendix is devoted to proving statements of Section 2. We start with Proposition 2.3.

**PROPOSITION 2.3.** Let $\mathcal{C}$ be a prevariety. A regular language $L$ belongs to $\mathcal{C}$ if and only if its syntactic morphism $\alpha_L : A^* \to M_L$ is a $\mathcal{C}$-morphism.

**PROOF.** The “if” implication is immediate since $L$ is recognized by its syntactic morphism. We prove the converse one: assuming that $L \in \mathcal{C}$, we prove that every language recognized by $\alpha_L : A^* \to M_L$ belongs to $\mathcal{C}$ (recall that syntactic morphisms are surjective by definition). Clearly, every such language is a union of $\equiv_L$-classes. Hence, as $\mathcal{C}$ is a prevariety, it suffices to prove that all $\equiv_L$-classes belong to $\mathcal{C}$. For every $s \in M_L$, we fix a word $x_s \in A^*$ such that $\alpha_L(x_s) = s$. Consider the following equivalence ~ on $A^*$:

$$u \sim v \text{ if and only if } x_s u x_t \in L \Leftrightarrow x_s v x_t \in L \text{ for every } s, t \in M_L.$$

We first show that $\sim$ and $\equiv_L$ are the same relation. It is immediate by definition that $\equiv_L \subseteq \sim$. For the converse inclusion, let $u, v \in A^*$ be such that $u \sim v$. We prove that $u \equiv_L v$. Given $x, y \in A^*$, we need to prove that $xuy \in L \Leftrightarrow xvy \in L$. Let $s = \alpha_L(x)$ and $t = \alpha_L(y)$. By definition, we have $\alpha_L(xuy) = \alpha_L(x_s u x_t)$ and $\alpha_L(xvy) = \alpha_L(x_s v x_t)$. Consequently, $xuy \in L \Leftrightarrow x_s u x_t \in L$ and $xvy \in L \Leftrightarrow x_s v x_t \in L$. Finally, since $u \sim v$, we know that $x_s u x_t \in L \Leftrightarrow x_s v x_t \in L$. Altogether, this yields $xuy \in L \Leftrightarrow xvy \in L$, as desired.

It remains to prove that every $\sim$-class belongs to $\mathcal{C}$. Let $w \in A^*$. We define the following subset $P_w$ and $N_w$ of $M_L^2$:

$$P_w = \{(s, t) \in M_L^2 \mid x_s w x_t \in L\} \quad \text{and} \quad N_w = \{(s, t) \in M_L^2 \mid x_s w x_t \notin L\}.$$

One can now verify from the definition of $\sim$ that the $\sim$-class of $w$ is the following language:

$$\left( \bigcap_{(s,t) \in P_w} \left(x_s^{-1} L x_t^{-1}\right) \right) \setminus \left( \bigcup_{(s,t) \in N_w} \left(x_s^{-1} L x_t^{-1}\right) \right).$$

Since $L \in \mathcal{C}$ and $\mathcal{C}$ is a prevariety, it follows that the $\sim$-class of $w$ belongs to $\mathcal{C}$, which completes the proof. $\square$

We turn to the proof of Proposition 2.4, which is standard.

**PROPOSITION 2.4.** Let $\mathcal{C}$ be a prevariety and consider finitely many languages $L_1, \dots, L_k$ of $\mathcal{C}$. There exists a $\mathcal{C}$-morphism $\eta : A^* \to N$ such that $L_1, \dots, L_k$ are all recognized by $\eta$.

**PROOF.** For every $i \le k$, let $\alpha_i : A^* \to M_i$ be the syntactic morphism of $L_i$. We know from Proposition 2.3 that $\alpha_i$ is a $\mathcal{C}$-morphism. Let $M = M_1 \times \dots \times M_k$ be the monoid equipped with the componentwise multiplication. Moreover, let $\alpha : A^* \to M$ be the morphism defined by $\alpha(w) = (\alpha_1(w_1), \dots, \alpha_k(w))$ for every $w \in A^*$. One can check from the definition of $\alpha$ that all languages recognized by $\alpha$ are finite intersections of languages recognized by $\alpha_1, \dots, \alpha_k$ (in particular, $\alpha$ recognizes each $L_i$). Hence, all languages recognized by $\alpha$ belong to $\mathcal{C}$. It now suffices to let $\eta : A^* \to N$ be the surjective restriction of $\alpha$ to complete the proof. $\square$

Finally, we provide a proof for Lemma 2.5.

**LEMMA 2.5.** Let $\mathcal{C}$ be a finite prevariety and let $\alpha : A^* \to M$ and $\eta : A^* \to N$ be two $\mathcal{C}$-morphisms. If $\alpha$ recognizes all languages in $\mathcal{C}$, then there exists a morphism $\gamma : M \to N$ such that $\eta = \gamma \circ \alpha$.
PROOF. Assume that $\alpha$ recognizes all languages in $\mathcal{C}$. We define $\gamma : M \to N$. For every $s \in M$, we fix a word $w_s \in \alpha^{-1}(s)$ (recall that $\mathcal{C}$-morphisms are surjective by definition) and define $\gamma(s) = \eta(w_s)$. It remains to prove that $\gamma$ is a morphism and that $\eta = \gamma \circ \alpha$. It suffices to prove the latter: since $\alpha$ is surjective, the former is an immediate consequence. Let $v \in A^*$. We show that $\eta(v) = \gamma(\alpha(v))$. Let $s = \alpha(v)$. By definition, $\gamma(s) = \eta(w_s)$. Hence, we need to prove that $\eta(v) = \eta(w_s)$. Since $\eta$ is a $\mathcal{C}$-morphism, we have $\eta^{-1}(\eta(w_s)) \in \mathcal{C}$. Hence, our hypothesis implies that $\eta^{-1}(\eta(w_s))$ is recognized by $\alpha$. Since it is clear that $w_s \in \eta^{-1}(\eta(w_s))$ and $\alpha(v) = \alpha(w_s) = s$, it follows that $v \in \eta^{-1}(\eta(w_s))$ which exactly says that $\eta(v) = \eta(w_s)$, completing the proof. $\square$

B Proofs of Section 3

This appendix provides proofs for statements that establish fundamental properties of the class SF($\mathcal{C}$).
We begin by proving its key closure properties.

PROPOSITION 3.2. If $\mathcal{C}$ is a prevariety, then SF($\mathcal{C}$) is a prevariety closed under concatenation.

PROOF. It is immediate by definition that SF($\mathcal{C}$) is a Boolean algebra closed under concatenation and containing only regular languages (indeed, it is well-known that regular languages are closed under Boolean operations and concatenation). Hence, it suffices to prove that SF($\mathcal{C}$) is quotient-closed. By symmetry, we only present a proof for left quotients. Let $w \in A^*$. We use induction on the length of $w$ to prove that for every $L \in SF(\mathcal{C})$, we have $w^{-1}L \in SF(\mathcal{C})$. When $w = \varepsilon$, we have $w^{-1}L = L$ for every $L \subseteq A^*$. Hence, the result is trivial. Assume now that $w \in A^+$ and consider $L \in SF(\mathcal{C})$. By hypothesis, there exist $u \in A^*$ and $a \in A$ such that $w = ua$. Hence, $w^{-1}L = u^{-1}(a^{-1}L)$. We use a sub-induction on the construction of $L$ to prove that $a^{-1}L \in SF(\mathcal{C})$. It will then be immediate by induction on the length of $w$ that $w^{-1}L = u^{-1}(a^{-1}L) \in SF(\mathcal{C})$.

Since $L \in SF(\mathcal{C})$, it is built from languages in $\mathcal{C}$ and the singletons $\{b\}$ for $b \in A$ using only union, complement and concatenation. We use induction on this construction to prove that $a^{-1}L \in SF(\mathcal{C})$. Assume first that $L \in \mathcal{C}$. In this case, $a^{-1}L \in \mathcal{C} \subseteq SF(\mathcal{C})$ since $\mathcal{C}$ is a prevariety. Assume now that $L = \{b\}$ for some $b \in A$. Then, either $b \neq a$ and $L = \emptyset \in \mathcal{C} \subseteq SF(\mathcal{C})$, or $b = a$ and $L = \{\varepsilon\}$, which also belongs to SF($\mathcal{C}$) since it is the complement of the union of all languages $A^*cA^*$ for $c \in A$.

We turn to the inductive cases. First, assume that $L = L_1 \cup L_2$ for languages $L_1, L_2 \in SF(\mathcal{C})$ for which, by induction, we have $a^{-1}L_1 \in SF(\mathcal{C})$ and $a^{-1}L_2 \in SF(\mathcal{C})$. Since $a^{-1}L = a^{-1}L_1 \cup a^{-1}L_2$, we get $a^{-1}L \in SF(\mathcal{C})$, as desired. Assume now that $L = A^* \setminus H$ for $H \in SF(\mathcal{C})$ such that, by induction, $a^{-1}H \in SF(\mathcal{C})$. One can verify that $a^{-1}L = A^* \setminus (a^{-1}H)$. Hence, we get $a^{-1}L \in SF(\mathcal{C})$, as desired. Finally, assume that $L = L_1L_2$ for languages $L_1, L_2 \in SF(\mathcal{C})$ for which, by induction, we have $a^{-1}L_1 \in SF(\mathcal{C})$ and $a^{-1}L_2 \in SF(\mathcal{C})$. It is easy to check that,

$$a^{-1}L = \begin{cases} (a^{-1}L_1)L_2 & \text{if } \varepsilon \notin L_1, \\ (a^{-1}L_1)L_2 \cup a^{-1}L_2 & \text{if } \varepsilon \in L_1. \end{cases}$$

Since $a^{-1}L_1 \in SF(\mathcal{C})$ and $a^{-1}L_2 \in SF(\mathcal{C})$ by induction, we get $a^{-1}L \in SF(\mathcal{C})$, as desired. $\square$

We now turn to the characteristic algebraic property of SF($\mathcal{C}$).

PROPOSITION 3.3. Let $\mathcal{C}$ be a prevariety and let $\alpha : A^* \to M$ be an $\mathcal{C}(\mathcal{C})$-morphism. There exists a $\mathcal{C}$-morphism $\eta : A^* \to N$ such that for every $u \in A^*$, if $\eta(u)$ is idempotent, then $(\alpha(u))^{\omega+1} = (\alpha(u))^{\omega}$.

PROOF. Since $\alpha$ is an $\mathcal{C}(\mathcal{C})$-morphism, we have $\alpha^{-1}(s) \in SF(\mathcal{C})$ for every $s \in M$. This means that $\alpha^{-1}(s)$ is built from finitely many languages of $\mathcal{C}$ and from the singletons $\{a\}$ (for $a \in A$) using union, complement and concatenation. Since $\mathcal{C}$ is a prevariety of regular languages, Proposition 2.4 yields a $\mathcal{C}$-morphism $\eta : A^* \to N$ recognizing all the languages in $\mathcal{C}$ used in the construction of the languages $\alpha^{-1}(s)$ for $s \in M$. Let $C_\eta = SF(\{\eta^{-1}(t) \mid t \in N\})$. By definition of $\eta$, we know that $\alpha^{-1}(s) \in SF(C_\eta)$ for every $s \in M$. We prove that for every language $L \in SF(C_\eta)$, there exists
an integer $k \ge 1$ such that the following property holds (recall that $\equiv_L$ denotes the syntactic congruence of $L$):

$$ \text{for every } u \in A^*, \text{ if } \eta(u) \text{ is idempotent, then } u^{k+1} \equiv_L u^k. \quad (11) $$

Let us first explain why this implies the statement of the proposition: $(\alpha(u))^{\omega+1} = (\alpha(u))^{\omega}$ for any $u \in A^*$ such that $\eta(u)$ is idempotent. Let $u$ be such a word and let $s = (\alpha(u))^{\omega}$. Since $\alpha^{-1}(s) \in SF(C_{\eta})$, there exists $k \ge 1$ such that (11) holds for $L = \alpha^{-1}(s)$. Let $p = \omega(M)$. Note that $\alpha(u^{pk}) = s$. This yields $u^{(p-1)k} \cdot u^k \cdot \varepsilon = u^{pk} \equiv \alpha^{-1}(s)$, whence by (11), $u^{pk+1} = u^{(p-1)k} \cdot u^{k+1} \cdot \varepsilon \equiv \alpha^{-1}(s)$. We get $(\alpha(u))^{\omega+1} = \alpha(u^{pk+1}) = s = (\alpha(u))^{\omega}$, as desired.

If remains to prove that for every language $L \in SF(C_{\eta})$, there exists $k \ge 1$ such that (11) holds. We argue by induction on the construction of $L$. The base cases are when $L = \eta^{-1}(t)$ for $t \in N$ and when $L$ is a singleton $\{a\}$. If $L = \eta^{-1}(t)$ for $t \in N$, then, (11) holds for $k = 1$. Indeed, given $u, x, y \in A^*$ such that $\eta(u)$ is idempotent, we have $\eta(xuuy) = \eta(xuy)$. Since $L$ is recognized by $\eta$, this yields $xuuy \in L \Leftrightarrow xuy \in L$, i.e., $u^2 \equiv_L u$. Assume next that $L = \{a\}$ for $a \in A$. In this case, (11) holds for $k = 2$. Indeed, let $u, x, y \in A^*$ such that $\eta(u)$ is idempotent. If $u = \varepsilon$, then $xu^{2+1}y = xy = xu^2y$ hence we get $xu^{2+1}y \in L \Leftrightarrow xu^2y \in L$. Otherwise, $u \in A^+$ and we have $|xu^2y| > 1$ and $|xu^{2+1}y| > 1$. Therefore, since $L = \{a\}$, we have $xu^2y \notin L$ and $xu^{2+1}y \notin L$. In all cases, $u^3 \equiv_L u^2$, concluding the proof of (11) in the base cases.

We turn to the inductive cases. Assume first that $L = L_1 \cup L_2$ is a union of two simpler languages $L_1, L_2$ of $SF(C_{\eta})$. By induction, this yields $k_1, k_2 \ge 1$ such that for $i = 1, 2$, if $u \in A^*$ is such that $\eta(u)$ is idempotent, we have $u^{k_i+1} \equiv_{L_i} u^{k_i}$. Hence, (11) holds for $L$ with $k = \max(k_1, k_2)$. We turn to complement: assume that $L = A^* \setminus H$ where $H$ is a simpler language of $SF(C_{\eta})$. By induction, we get $k \ge 1$ such that if $u \in A^*$ is such that $\eta(u)$ is idempotent, we have $u^{k+1} \equiv_H u^k$, i.e., $xu^k y \in H \Leftrightarrow xu^{k+1} y \in H$ for all $x, y \in A^*$. Since $L = A^* \setminus H$, the contrapositive states that $xu^k y \in L \Leftrightarrow xu^{k+1} y \in L$, and (11) holds for $L$ with the same integer $k$ as for $H$.

Finally, assume that the last operation used to construct $L$ is concatenation. We have $L = L_1 L_2$ where $L_1, L_2$ are simpler languages of $SF(C_{\eta})$. By induction, this yields $k_1, k_2 \ge 1$ such that for $i = 1, 2$, if $u \in A^*$ is such that $\eta(u)$ is idempotent, we have $u^{k_i+1} \equiv_{L_i} u^{k_i}$. Let $m = \max(k_1, k_2)$. We prove that (11) holds for $k = 2m + 1$. Let $u, x, y \in A^*$ with $\eta(u)$ idempotent. We have to show that $xu^{k+1}y \in L \Leftrightarrow xu^k y \in L$. We concentrate on the left to right implication (the converse one is symmetrical): assuming that $xu^{k+1}y \in L$, we show that $xu^k y \in L$. Since $L = L_1 L_2$, we get $w_1 \in L_1$ and $w_2 \in L_2$ such that $xu^{k+1}y = w_1 w_2$. Since $k \ge 2m + 1$, it follows that either $xu^{m+1}$ is a prefix of $w_1$ or $u^{m+1}y$ is a suffix of $w_2$. By symmetry, we assume that the former property holds: we have $w_1 = xu^{m+1}z$ for some $z \in A^*$. Observe that since $xu^{k+1}y = w_1 w_2$, it follows that $zw_2 = u^{k-m}y$. Moreover, we have $m \ge k_1$ by definition of $m$. Since $xu^{m+1}z = w_1 \in L_1$, we know therefore that $xu^m z \in L_1$ by definition of $k_1$. Thus, $xu^m z w_2 \in L_1 L_2 = L$. Since $zw_2 = u^{k-m}y$, this yields $xu^k y \in L$, concluding the proof. $\square$

We conclude this appendix by a direct proof of Lemma 3.5, which is easy.

**LEMMA 3.5.** Let $\mathcal{G}$ be a group prevariety and let $\alpha : A^* \to G$ be a $\mathcal{G}$-morphism. Then, $G$ is a group.

**PROOF.** Let $g \in G$, we exhibit an inverse $g^{-1} \in G$ for $g$ (i.e, such that $gg^{-1} = g^{-1}g = 1_G$). By hypothesis, $\alpha^{-1}(1_G) \in \mathcal{G}$. Since $\mathcal{G}$ is a group prevariety, there exists a morphism $\eta : A^* \to H$ into a finite group $H$ recognizing $\alpha^{-1}(1_G)$. Let $n = \omega(H)$. We define $g^{-1} = g^{n-1}$. Since $gg^{-1} = g^{-1}g = g^n$, it remains to prove that $g^n = 1_G$. Let $w \in \alpha^{-1}(g)$ (recall that $\mathcal{G}$-morphisms are surjective). Clearly, $\eta(w^n) = (\eta(w))^n$ is an idempotent of $H$ since $n = \omega(H)$. Hence, $\eta(w^n) = 1_H$ since $H$ is a group. Hence, $\eta(w^n) = \eta(\varepsilon)$. Since $\varepsilon \in \alpha^{-1}(1_G)$ and since $\alpha^{-1}(1_G)$ is recognized by $\eta$, we get $w^n \in \alpha^{-1}(1_G)$, i.e., $\alpha(w^n) = g^n = 1_G$, as desired. $\square$
C Proofs of Section 4

This appendix presents proofs of stabdard and basic results concerning prefix codes. We begin with
the fundamental property of such a code.

FACT 4.2. Let $K$ be a prefix code. Consider $m, n \in \mathbb{N}$, $u_1, \dots, u_m \in K$ and $v_1, \dots, v_n \in K$. The two following properties hold:

• If $u_1 \cdots u_m$ is a prefix of $v_1 \cdots v_n$, then $m \le n$ and $u_i = v_i$ for every $i \le m$.

• If $u_1 \cdots u_m = v_1 \cdots v_n$, then $m = n$ and $u_i = v_i$ for every $i \le m$.

PROOF. The second property is an immediate corollary of the first one. Hence, it suffices to show that if $u_1 \cdots u_m$ is a prefix of $v_1 \cdots v_n$, then $m \le n$ and $u_i = v_i$ for every $i \le m$. We proceed by induction on $m \in \mathbb{N}$. If $m=0$, then the property is immediate. Otherwise, $m \ge 1$. Clearly, $u_1 \cdots u_{m-1}$ is a prefix of $v_1 \cdots v_n$. Hence, induction yields that $m-1 \le n$ and $u_i = v_i$ for every $i \le m-1$. Now, since $u_1 \cdots u_m$ is a prefix of $v_m \cdots v_n$, it follows that $u_m$ is a prefix of $v_m \cdots v_n$. Since $u_m \in K$ and $K$ is a prefix code, we have $u_m \ne \epsilon$, which implies that $v_m \cdots v_n \ne \epsilon$, i.e., $m \le n$. Moreover, since $K$ is a prefix code and $u_m, v_m \in K$ we know that $u_m$ is not a strict prefix of $v_m$ and $v_m$ is not a strict prefix of $u_m$. Together with the hypothesis that $u_m$ is a prefix of $v_m \cdots v_n$, this yields $u_m = v_m$, concluding the proof. $\square$

We now prove two facts that facilitate the construction of new prefix codes from a given one.

FACT 4.6. Let $d \ge 1$ and let $K \subseteq A^+$ be a prefix code with synchronization delay $d$. Then, every language $H \subseteq K$ is also a prefix code with synchronization delay $d$.

PROOF. It is immediate from the definitions that $H$ is itself a prefix code. It remains to prove that $H$ has synchronization delay $d$. Consider $u, v, w \in A^*$ such that $uvw \in H^+$ and $v \in H^d$. We show that $uv \in H^+$. Since $H \subseteq K$, we have $uvw \in K^+$ and $v \in K^d$. Since $K$ has synchronization delay $d$, we obtain $uv \in K^+$. Moreover, since $K$ is a prefix code and $uvw \in K^+$, it follows from the second property in Fact 4.2 that $uvw$ admits a unique decomposition into factors of $K$. Additionally, since $uvw \in H^+$ with $H \subseteq K$, all factors in this unique decomposition belong to $H$. Finally, since $uv \in K^+$, the first property in Fact 4.2 yields that $uv$ is a concatenation of factors in this unique decomposition. Hence, we have $uv \in H^+$, which concludes the proof. $\square$

FACT 4.7. Let $d \ge 1$ and let $K \subseteq A^+$ be a prefix code with synchronization delay $d$. Let $H \subseteq K$. Then, the language $(K \setminus H)^*H$ is a prefix code with synchronization delay $d+1$.

PROOF. We first verify that $(K \setminus H)^*H$ is a prefix code. Clearly, $(K \setminus H)^*H \subseteq A^+$ since $H \subseteq K \subseteq A^+$. Hence, we have to show that $(K \setminus H)^*H \cap (K \setminus H)^*HA^+ = \emptyset$. Assume by contradiction that there exists $w \in (K \setminus H)^*H \cap (K \setminus H)^*HA^+$. In particular, we have $w \in (K \setminus H)^*H \subseteq K^*$. Since $K$ is a prefix code, $w$ admits a *unique* decomposition $w = w_1 \cdots w_n$ with $w_1, \dots, w_n \in K$. Since $w \in (K \setminus H)^*H$, the factor $w_n$ is the only one to be in $H$ among all the $w_i$'s. However, since $w \in (K \setminus H)^*HA^+$, the first property in Fact 4.2 implies that one of the factors $w_i$ for $i \le n-1$ must belong to $H$. This is a contradiction. Therefore, $(K \setminus H)^*H$ is a prefix code.

It remains to show that $(K \setminus H)^*H$ has synchronization delay $d+1$. Let $u, v, w \in A^*$ such that $uvw \in ((K \setminus H)^*H)^+$ and $v \in ((K \setminus H)^*H)^{d+1}$. We prove that $uv \in ((K \setminus H)^*H)^+$. Clearly $v = xy$ with $x \in ((K \setminus H)^*H)^d$ and $y \in (K \setminus H)^*H$. Observe that $x \in K^n$ for some $n \ge d$. Hence, since $uxyw = uvw \in K^+$ and $K$ has synchronization delay $d$, it follows that $ux \in K^+$. Consequently $uv = uxy \in K^+(K \setminus H)^*H$, whence $uv \in K^*H \subseteq ((K \setminus H)^*H)^+$. This concludes the proof. $\square$
## D Proofs of Section 5

This appendix is devoted to proving general results used in the characterization of SF($C$). These concern $C$-pairs and $C$-morphisms. As noted in the main text, some of these proofs also appear in [32]. We begin with a key property: the existence of a $C$-morphism that determines whether a given pair is a $C$-pair.

**LEMMA 5.3.** Let $C$ be a prevariety and let $\alpha : A^* \to M$ be a morphism into a finite monoid. The two following properties hold:

(1) For every $C$-morphism $\eta : A^* \to N$ and every $C$-pair $(s, t) \in M^2$ for $\alpha$, there exist $u, v \in A^*$ such that $\eta(u) = \eta(v)$, $\alpha(u) = s$ and $\alpha(v) = t$.

(2) There exists a $C$-morphism $\eta : A^* \to N$ such that for all $u, v \in A^*$, if $\eta(u) = \eta(v)$, then $(\alpha(u), \alpha(v))$ is a $C$-pair for $\alpha$.

**PROOF.** Let us start with the first assertion. Let $\eta : A^* \to N$ be a $C$-morphism and let $(s, t) \in M^2$ be a $C$-pair for $\alpha$. Let $F = \eta(\alpha^{-1}(s)) \subseteq N$. We have $\eta^{-1}(F) \in C$ since $\eta$ is a $C$-morphism. Moreover, it is immediate from the definition of $F$ that $\alpha^{-1}(s) \subseteq \eta^{-1}(F)$. Since $(s, t)$ is a $C$-pair (meaning that $\alpha^{-1}(s)$ cannot be separated from $\alpha^{-1}(t)$ by a language in $C$), it follows that $\eta^{-1}(F) \cap \alpha^{-1}(t) \neq \emptyset$. This yields $v \in A^*$ such that $\eta(v) \in F$ and $\alpha(v) = t$. Finally, since $\eta(v) \in F = \eta(\alpha^{-1}(s))$, we get $u \in A^*$ such that $\eta(u) = \eta(v)$ and $\alpha(u) = s$. This concludes the proof of the first assertion.

Let us turn to the second assertion. Let $P \subseteq M^2$ be the set of all pairs $(s, t) \in M^2$ which are not $C$-pairs. For every $(s, t) \in P$, there exists $K_{s,t} \in C$ separating $\alpha^{-1}(s)$ from $\alpha^{-1}(t)$. Proposition 2.4 yields a $C$-morphism $\eta : A^* \to N$ such that every language $K_{s,t}$ for $(s, t) \in P$ is recognized by $\eta$. It remains to prove that for every $u, v \in A^*$, if $\eta(u) = \eta(v)$, then $(\alpha(u), \alpha(v))$ is a $C$-pair. We prove the contrapositive. Assuming that $(\alpha(u), \alpha(v))$ is a not a $C$-pair, we show that $\eta(u) \neq \eta(v)$. By hypothesis, $(\alpha(u), \alpha(v)) \in P$, which means that $K_{\alpha(u),\alpha(v)} \in C$ is defined and separates $\alpha^{-1}(\alpha(u))$ from $\alpha^{-1}(\alpha(v))$. In particular, $u \in K_{\alpha(u),\alpha(v)}$ and $v \notin K_{\alpha(u),\alpha(v)}$. Since $K_{\alpha(u),\alpha(v)}$ is recognized by $\eta$, this implies that $\eta(u) \neq \eta(v)$. $\square$

An important corollary of Lemma 5.3 is that the set of $C$-pairs is closed under products.

**LEMMA 5.4.** Let $C$ be a prevariety and let $\alpha : A^* \to M$ be a morphism into a finite monoid. If $(s_1, t_1)$, $(s_2, t_2) \in M^2$ are $C$-pairs, then $(s_1s_2, t_1t_2)$ is a $C$-pair as well.

**PROOF.** Item 2 of Lemma 5.3 yields a $C$-morphism $\eta : A^* \to N$ such that for all $u, v \in A^*$, if $\eta(u) = \eta(v)$, then $(\alpha(u), \alpha(v))$ is a $C$-pair. Let $(s_1, t_1)$, $(s_2, t_2) \in M^2$ be $C$-pairs. Since $\eta$ is a $C$-morphism, it follows from Item 1 of Lemma 5.3 that there exist $u_i, v_i \in A^*$ for $i = 1, 2$ such that $\eta(u_i) = \eta(v_i)$, $\alpha(u_i) = s_i$ and $\alpha(v_i) = t_i$. This yields $\eta(u_1u_2) = \eta(v_1v_2)$, $\alpha(u_1u_2) = s_1s_2$ and $\alpha(v_1v_2) = t_1t_2$. Hence, $(s_1s_2, t_1t_2)$ is a $C$-pair by definition of $\eta$. $\square$

We now prove that, under suitable hypotheses of $C$, the set of $C$-orbits is a monoid.

**LEMMA 5.5.** Let $C$ be a prevariety and let $\alpha : A^* \to M$ be a surjective morphism into a finite monoid. For every $e \in E(M)$, the $C$-orbit of $e$ for $\alpha$ is a subsemigroup of $M$. Moreover, it is a monoid whose neutral element is $e$.

**PROOF.** We write $N_e \subseteq M$ for the $C$-orbit of $e$. Observe that $N_e$ is nonempty: $e = eee \in N_e$ since $(e, e)$ is a $C$-pair (note that here, we need the hypothesis that $\alpha$ is surjective, as it implies that $\alpha^{-1}(e) \neq \emptyset$). Moreover, since $e$ is idempotent, it is clear that for every $q \in N_e$, we have $eq = qe = q$ since $q = ese$ for some $s \in M$. It remains to prove that $N_e$ is a subsemigroup of $M$. Let $q, r \in N_e$. We show that $qr \in N_e$. By definition, we get $s, t \in M$ such that $(e, s)$ and $(e, t)$ are $C$-pairs, $q = ese$ and $r = ete$. Since $(e, e)$ is also a $C$-pair and $C$ is a prevariety, Lemma 5.4 implies that $(e, set)$ is a $C$-pair. Hence, we have $qr = eseete = esete \in N_e$, as desired. $\square$
We end this appendix by connecting $\mathcal{G}$-orbits with the $\mathcal{G}$-kernel of a surjective morphism, when $\mathcal{G}$ is a group prevariety.

LEMMA 5.10. Let $\mathcal{G}$ be a group prevariety and let $\alpha : A^* \to M$ be a surjective morphism into a finite monoid. Let $N$ be the $\mathcal{G}$-kernel of $\alpha$. The two following properties hold:

* Every $\mathcal{G}$-orbit for $\alpha$ is a subset of $N$.

* N is exactly the $\mathcal{G}$-orbit of $1_M$ for $\alpha$.

PROOF. First, let $e \in E(M)$ and let $N_e$ be the $\mathcal{G}$-orbit of $e$. We prove that $N_e \subseteq N$. Let $q \in N_e$. This yields $s \in M$ such that $(e, s)$ is a $\mathcal{G}$-pair and $q = ese$. By contradiction, assume that $q \notin N$. By definition, we get a language $K \in \mathcal{G}$ separating $\{\varepsilon\}$ from $\alpha^{-1}(q)$. That is, $\varepsilon \in K$ and $K \cap \alpha^{-1}(q) = \emptyset$. We exhibit an element $x \in K \cap \alpha^{-1}(q)$, yielding a contradiction. Since $K \in \mathcal{G}$, Proposition 2.4 yields a $\mathcal{G}$-morphism $\eta : A^* \to G$ recognizing $K$. Moreover, Lemma 3.5 implies that $G$ is a group since $\mathcal{G}$ is a group prevariety. Since $(e, s)$ is a $\mathcal{G}$-pair, Lemma 5.3 yields $u, v \in A^*$ such that $\eta(u) = \eta(v)$, $\alpha(u) = e$ and $\alpha(v) = s$. Let $k = \omega(G)$ and $x = u^k v u^{k-1}$. Since $\eta(u) = \eta(v)$ and $G$ is a group, we have $\eta(x) = (\eta(u))^k = 1_G = \eta(\varepsilon)$. Hence, since $\varepsilon \in K$ and $K$ is recognized by $\eta$, we have $x \in K$. This a contradiction since $\alpha(x) = e^k s e^{k-1} = ese = q$ and $K \cap \alpha^{-1}(q) = \emptyset$ by hypothesis.

It remains to prove that $N$ is exactly the $\mathcal{G}$-orbit of $1_M$ for $\alpha$. Since we already proved that the latter is included in the former, it suffices to show that every $s \in N$ belongs to the $\mathcal{G}$-orbit of $1_M$. Since $s \in N$, we know that $\{\varepsilon\}$ is not $\mathcal{G}$-separable from $\alpha^{-1}(s)$. Since $\varepsilon \in \alpha^{-1}(1_M)$, it follows that $\alpha^{-1}(1_M)$ is not $\mathcal{G}$-separable from $\alpha^{-1}(s)$, i.e., $(1_M, s)$ is a $\mathcal{G}$-pair. Hence, $s = 1_M s 1_M$ belongs to the $\mathcal{G}$-orbit of $1_M$, as desired. $\square$

E Proofs of Section 6

This section presents the proofs omitted from the main text concerning first-order logic and its general connection with the start-free closure operator. We begin by showing that when $\mathcal{G}$ is a group prevariety, two equivalent signatures can be used for our purposes.

LEMMA 6.4. Let $\mathcal{G}$ be a group prevariety. Then, $\mathrm{FO}(\mathbb{I}_{\mathcal{G}}) = \mathrm{FO}(\langle\cdot, \mathbb{P}_{\mathcal{G}}\rangle)$.

PROOF. The inclusion $\mathrm{FO}(\langle\cdot, \mathbb{P}_{\mathcal{G}}\rangle) \subseteq \mathrm{FO}(\mathbb{I}_{\mathcal{G}})$ is immediate since all predicates in $\{\langle\cdot\rangle \cup \mathbb{P}_{\mathcal{G}}\}$ can be simulated using those in $\mathbb{I}_{\mathcal{G}}$. Indeed, $x < y$ is equivalent to $I_{A^*}(x, y)$ and $P_L(x)$ (for $L \in \mathcal{G}$) is equivalent to $I_L(\min, x)$. We now prove that $\mathrm{FO}(\mathbb{I}_{\mathcal{G}}) \subseteq \mathrm{FO}(\langle\cdot, \mathbb{P}_{\mathcal{G}}\rangle)$. By definition, it suffices to prove that for every language $L \in \mathcal{G}$, the atomic formula $I_L(x, y)$ is equivalent to a formula of $\mathrm{FO}(\langle\cdot, \mathbb{P}_{\mathcal{G}}\rangle)$. Proposition 2.4 yields a $\mathcal{G}$-morphism $\alpha : A^* \to G$ recognizing $L$. Since $\mathcal{G}$ is a group prevariety, Lemma 3.5 implies that $G$ is a group. Let $F \subseteq G$ be the set such that $\alpha^{-1}(F) = L$.

For every $g \in G$, the language $\alpha^{-1}(g)$ belongs to $\mathcal{G}$, whence $P_{\alpha^{-1}(g)}$ is a predicate in $\mathbb{P}_{\mathcal{G}}$. Since $G$ is a group, it is immediate that $\alpha(v) = (\alpha(ua))^{-1}\alpha(uav)$ for all $u, v \in A^*$ and $a \in A$. Therefore, one can check that $I_L(x, y)$ is equivalent to the following formula of $\mathrm{FO}(\langle\cdot, \mathbb{P}_{\mathcal{G}}\rangle)$, where $T \subseteq G \times A \times G$ is the set of all triples $(g, a, h) \in G \times A \times G$ such that $(g\alpha(a))^{-1}h \in F$:

$$ (x < y) \wedge \left( (x = \min \wedge P_L(y)) \vee \bigvee_{(g,a,h) \in T} (P_{\alpha^{-1}(g)}(x) \wedge a(x) \wedge P_{\alpha^{-1}(h)}(y)) \right). $$

This concludes the proof. $\square$

<figure><img src="image_3.png" /></figure>

The rest of this appendix is devoted to the proof of Theorem 6.6, that establishes a correspondence between star-free closure and extended star-free logic.

THEOREM 6.6. Let $\mathcal{C}$ be a prevariety. Then, $\mathrm{SF}(\mathcal{C}) = \mathrm{FO}(\mathbb{I}_{\mathcal{C}})$.
**PROOF.** We fix a prevariety $\mathcal{C}$ and show that $SF(\mathcal{C}) = FO(\mathbb{I}_e)$. The two inclusions are proved independently. We start with $SF(\mathcal{C}) \subseteq FO(\mathbb{I}_e)$, which is simpler.

**Inclusion** $SF(\mathcal{C}) \subseteq FO(\mathbb{I}_e)$. By definition of $SF(\mathcal{C})$, it suffices to prove that $\mathcal{C} \subseteq FO(\mathbb{I}_e)$, that $\{a\} \in FO(\mathbb{I}_e)$ for every $a \in A$ and that $FO(\mathbb{I}_e)$ is closed under union, complement and concatenation. It is clear that every $L \in \mathcal{C}$ is defined by the sentence $I_L(min, max)$ of $FO(\mathbb{I}_e)$. Therefore, $\mathcal{C} \subseteq FO(\mathbb{I}_e)$. Moreover, for every letter $a \in A$, the language $\{a\}$ is defined by the sentence $\exists x (a(x) \land (min + 1 = x) \land (x + 1 = max))$. It is also clear that $FO(\mathbb{I}_e)$ is closed under union and complement since Boolean connectives can be used freely in $FO(\mathbb{I}_e)$ sentences. It remains to prove that $FO(\mathbb{I}_e)$ is closed under concatenation. The argument is based on the following lemma.

**LEMMA E.1.** Let $L \in FO(\mathbb{I}_e)$. There exists an $FO(\mathbb{I}_e)$ formula $\varphi_L(x, y)$ with two free variables $x$ and $y$ such that for every $w \in A^*$ and every positions $i, j \in \text{Pos}(w)$ in $w$ such that $i < j$, we have $w \models \varphi_L(i, j)$ if and only if $w(i, j) \in L$

**PROOF.** By hypothesis, there exists a sentence $\psi$ of $FO(\mathbb{I}_e)$ defining $L$. We build $\varphi_L(x, y)$ from $\psi$ by restricting quantifications with respect to the free variables $x, y$: we only allow quantification over positions between $x$ and $y$. Moreover, we use $x$ and $y$ themselves as substitutes for the unlabeled positions. More precisely, $\varphi_L(x, y)$ is defined by applying the following modifications to $\psi$:

(1) Every subformula of the form $\exists z \Gamma$ is recursively replaced by,

$$ \exists z (( (z = x) \lor (x < z \land z < y) \lor (z = y) ) \land \Gamma ). $$

(2) All occurrences of the constant $min$ are replaced by the free variable $x$ and all occurrences of the constant $max$ are replaced by $y$.

(3) Every atomic subformula of the form $a(z)$ for some $a \in A$ is replaced by,

$$ a(z) \land (x < z) \land (z < y). $$

One can verify that $\varphi_L(x, y)$ satisfies the desired property. $\square$

We can now prove that $FO(\mathbb{I}_e)$ is closed under concatenation. Let $K, L \in FO(\mathbb{I}_e)$. We prove that $KL \in FO(\mathbb{I}_e)$. Lemma E.1 yields two formulas $\varphi_K(x, y)$ and $\varphi_L(y, z)$ such that for every $w \in A^*$ and every positions $i, j \in \text{Pos}(w)$ in $w$ such that $i < j$, we have $w \models \varphi_K(i, j)$ if and only if $w(i, j) \in K$ and $w \models \varphi_L(i, j)$ if and only if $w(i, j) \in L$. It is now immediate that $KL$ is defined by the following sentence of $FO(\mathbb{I}_e)$:

$$ \exists x \exists y (x + 1 = y) \land \varphi_K(min, y) \land \varphi_L(x, max). $$

We obtain $KL \in FO(\mathbb{I}_e)$, as desired. This completes the proof of the first inclusion: $SF(\mathcal{C}) \subseteq FO(\mathbb{I}_e)$.

**Inclusion** $FO(\mathbb{I}_e) \subseteq SF(\mathcal{C})$. The proof of this inclusion is more involved. Yet, it is constructive as well: starting from an $FO(\mathbb{I}_e)$ sentence $\varphi$, we use structural induction on $\varphi$ to prove that the language it defines may be built from basic languages in $\mathcal{C}$ using Boolean combinations and concatenations. Of course, this means that we shall have to deal with formulas that are not sentences. We start with preliminary definitions.

Let $n \in \mathbb{N}$. An $n$-scheme is a tuple $\bar{L} = (L_0, a_1, L_1, \dots, a_n, L_n)$ where $L_0, \dots, L_n \subseteq A^*$ and $a_1, \dots, a_n \in A$. Note that 0-schemes are well-defined: they are simply languages. We write $\bar{L} \in SF(\mathcal{C})$ to indicate that $L_0, \dots, L_n \in SF(\mathcal{C})$. Additionally, we define an $n$-blueprint as a finite set $L$ of $n$-schemes. We write $L \in SF(\mathcal{C})$ to indicate that $\bar{L} \in SF(\mathcal{C})$ for every $n$-scheme $\bar{L} \in L$. Let us provide semantics for $n$-blueprints.

Given $n \in \mathbb{N}$, an $n$-split is a *linearly ordered set* $\mathcal{X}$ of exactly $n+2$ first-order variables. For the sake of avoiding clutter, we often make the linear ordering implicit. For example, if we say that the set $\mathcal{X} = \{x_0, \dots, x_{n+1}\}$ is an $n$-split, we implicitly mean that the ordering is $x_0 < x_1 < \dots < x_n < x_{n+1}$.
Moreover, given an $n$-split $\mathcal{X} = \{x_0, \dots, x_{n+1}\}$ and a word $w \in A^*$, we say that an assignment $\mu : \mathcal{X} \to \mathrm{Pos}(w)$ is correct to indicate that,

$$0 = \mu(x_0) < \mu(x_1) < \dots < \mu(x_{n+1}) = |w| + 1.$$

Now, consider an $n$-blueprint $\mathcal{L}$ and an $n$-split $\mathcal{X} = \{x_0, \dots, x_{n+1}\}$, a word $w \in A^*$ and a correct assignment $\mu : \mathcal{X} \to \mathrm{Pos}(w)$. We say that $(w, \mu)$ satisfies $\mathcal{L}$ and write $w, \mu \models \mathcal{L}$ if and only if there exists an $n$-scheme $(L_0, a_1, L_1, \dots, a_n, L_n) \in \mathcal{L}$ which satisfies the two following conditions:

(1) For all $1 \le i \le n$, the position $\mu(x_i) \in \mathrm{Pos}(w)$ is labeled by $a_i$.

(2) For all $0 \le i \le n$, we have $w(\mu(x_i), \mu(x_{i+1})) \in L_i$.

Observe that when $n = 0$, there exists only one correct assignment $\mu : \mathcal{X} \to \mathrm{Pos}(w)$: we have $\mu(x_0) = 0$ and $\mu(x_1) = |w| + 1$. Moreover, in that case, $w, \mu \models \mathcal{L}$ if and only there exists a language $L \in \mathcal{L}$ such that $w \in L$.

The argument is based on the next proposition, proved by induction on the size of $\mathrm{FO}(\mathbb{I}_c)$ formulas. The statement only applies to constant-free formulas (i.e., which do not involve symbols “min” and “max”), a restriction we shall deal with when using it to complete the main proof.

**PROPOSITION E.2.** Let $n \in \mathbb{N}$, $\mathcal{X}$ be an $n$-split and $\varphi$ be a constant-free $\mathrm{FO}(\mathbb{I}_c)$-formula whose free variables are contained in $\mathcal{X}$. Then, there exists an $n$-blueprint $\mathcal{L}_\varphi \in \mathrm{SF}(\mathbb{C})$ such that for all $w \in A^*$ and for all correct assignment $\mu : \mathcal{X} \to \mathrm{Pos}(w)$, we have:

$$w, \mu \models \mathcal{L}_\varphi \iff w, \mu \models \varphi. \qquad (12)$$

We first apply Proposition E.2 to prove that $\mathrm{FO}(\mathbb{I}_c) \subseteq \mathrm{SF}(\mathbb{C})$. Let $L \in \mathrm{FO}(\mathbb{I}_c)$. We prove that $L \in \mathrm{SF}(\mathbb{C})$. The hypothesis $L \in \mathrm{FO}(\mathbb{I}_c)$ means that there is an $\mathrm{FO}(\mathbb{I}_c)$-sentence $\psi$ defining $L$. Consider the 0-split $\mathcal{X} = \{x_0, x_1\}$. Since variables can be renamed, we can assume without loss of generality that $x_0$ and $x_1$ do not occur in $\psi$. Let $\varphi$ be the formula obtained from $\psi$ by replacing all occurrences of the constant symbols $\min$ and $\max$ by $x_0$ and $x_1$, respectively. It follows from Proposition E.2 that there exists a 0-blueprint $\mathcal{L}_\varphi \in \mathrm{SF}(\mathbb{C})$ satisfying (12). By definition $\mathcal{L}_\varphi$ is a finite set of languages in $\mathrm{SF}(\mathbb{C})$. We let $H = \bigcup_{K \in \mathcal{L}_\varphi} K \in \mathrm{SF}(\mathbb{C})$ and show that $H = L$ to complete the proof. Consider a word $w \in A^*$ and let $\mu : \mathcal{X} \to \mathrm{Pos}(w)$ be the only correct assignment: $\mu(x_0) = 0$ and $\mu(x_1) = |w| + 1$. By definition of $\varphi$ from $\psi$, it is immediate that $w \in L \Leftrightarrow w, \mu \models \varphi$. It then follows from (12) that $w \in L \Leftrightarrow w, \mu \models \mathcal{L}_\varphi$. Finally by definition of $H$, we obtain $w \in L \Leftrightarrow w \in H$, as desired. This concludes the main argument. It remains to prove Proposition E.2.

**PROOF OF PROPOSITION E.2.** Let $n \in \mathbb{N}$, $\mathcal{X}$ be an $n$-split and $\varphi$ be a constant-free $\mathrm{FO}(\mathbb{I}_c)$ formula whose free variables are contained in $\mathcal{X}$. We write $\mathcal{X} = \{x_0, \dots, x_{n+1}\}$. Moreover, we can assume without loss of generality that $\varphi$ does not contain the equality predicate, as subformulas of the form “$y = z$” may be replaced by the equivalent formula “$\neg(y < z \lor z < y)$” (recall from Remark 6.1 that the linear ordering is available in $\mathbb{I}_c$). We use induction on the size of $\varphi$ (i.e., on the number of nodes in its syntax tree) to construct an $n$-blueprint $\mathcal{L}_\varphi \in \mathrm{SF}(\mathbb{C})$ satisfying (12).

**Atomic Formulas.** By hypothesis on $\varphi$ there are only two kinds of atomic formulas: those involving the label predicates and those involving the predicates in $\mathbb{I}_c$. Note that since $\varphi$ is constant-free, there are no atomic formulas involving the constants $\min$ and $\max$.

Assume first that $\varphi := \text{"a}(x_h)$ for some $a \in A$ and $h$ such that $0 \le h \le n + 1$. There are two cases. If $h = 0$ or $h = n + 1$, then it suffices to define $\mathcal{L}_\varphi = \emptyset \in \mathrm{SF}(\mathbb{C})$. Otherwise, we have $1 \le h \le n$. We define $\mathcal{L}_\varphi$ as the set of all $n$-schemes $(A^*, a_1, A^*, \dots, a_n, A^*)$ where $a_1, \dots, a_n \in A$ are letters such that $a_h = a$. It is clear that $\mathcal{L}_\varphi \in \mathrm{SF}(\mathbb{C})$ and one can check from the definitions that it satisfies (12).

Assume now that $\varphi := \text{"I}_L(x_g, x_h)$ for $g, h$ such that $0 \le g, h \le n + 1$ and $L \in \mathbb{C}$. Recall that for a word $w \in A^*$ and two positions $i, j$ within $w$, the property $I_L(i, j)$ holds if and only if $i < j$
and $w(i, j) \in L$. Hence, there are two cases. First, if $h \le g$, it suffices to define $L_{\varphi} = \emptyset \in SF(C)$. Assume now that $g < h$. Since $C$ is a prevariety, Proposition 2.4 yields a $C$-morphism $\eta: A^* \to N$ recognizing $L$. Let $F \subseteq M$ such that $L = \alpha^{-1}(F)$. We define a set of tuples $T \subseteq M \times (A \times M)^n$ (when $n=0$, we have $T \subseteq M$) as follows:

$$T = \{(s_0, a_1, s_1, \dots, a_n, s_n) \mid s_g \alpha(a_{g+1}) s_{g+1} \cdots \alpha(a_{h-1}) s_{h-1} \in F\}.$$

We define $L_{\varphi}$ as the set of all $n$-schemes $(\eta^{-1}(s_0), \{a_1\}, \eta^{-1}(s_1), \dots, \{a_n\}, \eta^{-1}(s_n))$ such that the tuple $(s_0, a_1, s_1, \dots, a_n, s_n)$ belongs to $T$. Since $\eta$ is a $C$-morphism, it is immediate that $L_{\varphi} \in C \subseteq SF(C)$. One can now check from the definitions that $L_{\varphi}$ satisfies (12).

**Disjunction.** Let us now assume that $\varphi := \psi_1 \lor \psi_2$. For $i = 1, 2$, induction yields an $n$-blueprint $L_i \in SF(C)$ which satisfies (12) for $\psi_i$. It is now immediate from the definitions that $L_{\varphi} = L_1 \cup L_2 \in SF(C)$ satisfies (12) for $\varphi$.

**Negation.** We assume that $\varphi := \neg \psi$. Induction yields an $n$-blueprint $L_{\psi} \in SF(C)$ such that if $w \in A^*$ and $\mu: \mathcal{X} \to \mathrm{Pos}(w)$ is a correct assignment, then $w, \mu \in L_{\psi} \Leftrightarrow w, \mu \models \psi$. Let $\tilde{L}_1, \dots, \tilde{L}_k \in SF(C)$ be the $n$-schemes such that $L_{\psi} = \{\tilde{L}_1, \dots, \tilde{L}_k\}$. Finally, for every $j \le k$, we let $(L_{0,j}, a_{1,j}, L_{1,j}, \dots, a_{n,j}, L_{n,j}) = \tilde{L}_j$. Let $J \subseteq \{1, \dots, k\}$. We define,

$$H_{i,J} = A^* \setminus \left( \bigcup_{j \in J} L_{i,j} \right) \text{ for } 0 \le i \le n.$$

Note that $H_{i,\emptyset} = A^*$. Moreover, since $SF(C)$ is closed under union and complement by definition, we have $H_{i,J} \in SF(C)$. We now define $L_{\varphi}$ as the set of all $n$-schemes $(H_{0,j_0}, b_1, H_{1,j_1}, \dots, b_n, H_{n,j_n})$ where $b_1, \dots, b_n \in A$ and $J_0, \dots, J_n \subseteq \{1, \dots, k\}$ are such that for every $j \le k$, either $b_i \ne a_{i,j}$ for some $i$ such that $1 \le i \le n$, or $j \in J_i$ for some $i$ such that $0 \le i \le n$. By definition, $L_{\varphi}$ is an $n$-blueprint satisfying $L_{\varphi} \in SF(C)$. Moreover, it is straightforward to verify that if $w \in A^*$ and $\mu: \mathcal{X} \to \mathrm{Pos}(w)$ is a correct assignment, then $w, \mu \models L_{\varphi}$ if and only if $w, \mu \not\models L_{\psi}$. Since $\varphi := \neg \psi$, it is immediate that $L_{\varphi}$ satisfies (12), as desired.

**First-order quantification.** Finally, assume that $\varphi := \exists y \psi$. Since variables may be renamed, we can assume without loss of generality that $y \notin \mathcal{X} = \{x_0, \dots, x_{n+1}\}$. We define $L_{\varphi}$ as the union of some $n$-blueprints that we build by induction. We use two kinds of $n$-blueprints in this union.

For every $i$ such that $0 \le i \le n+1$, let $\psi_i$ be the formula obtained from $\psi$ by replacing every free occurrence of the variable $y$ with $x_i$. By definition all free variables in $\psi_i$ belong to $\mathcal{X}$. Moreover, the size of $\psi_i$ is the same as the one of $\psi$ which is strictly smaller than the size of $\varphi := \exists y \psi$. Consequently, induction yields an $n$-blueprint $L_i \in SF(C)$ such that if $w \in A^*$ and $\mu: \mathcal{X} \to \mathrm{Pos}(w)$ is a correct assignment, then $w, \mu \models L_i \Leftrightarrow w, \mu \models \psi_i$.

We turn to the second kind of $n$-blueprint. Let $i$ such that $0 \le i \le n$. We consider the linearly ordered set of first-order variables $Y_i = \{x_0, \dots, x_i, y, x_{i+1}, \dots, x_{n+1}\}$ (i.e., $Y_i = \mathcal{X} \cup \{y\}$ and $y$ is placed between $x_i$ and $x_{i+1}$ for the linear ordering). Since the size of $\psi$ is strictly smaller than the one of $\varphi := \exists y \psi$, induction yields an $(n+1)$-blueprint $G_i \in SF(C)$ such that if $w \in A^*$ and $\gamma: Y_i \to \mathrm{Pos}(w)$ is a correct assignment, then $w, \mu \models G_i \Leftrightarrow w, \gamma \models \psi$. We use $G_i$ to define an $n$-blueprint $H_i$. Let $\tilde{G} = (G_0, c_1, G_1, \dots, c_{n+1}, G_{n+1})$ be an arbitrary $(n+1)$-scheme. We associate to $\tilde{G}$ an $n$-scheme $f_i(\tilde{G}) = (H_0, d_1, H_1, \dots, d_n, H_n)$ as follows:

* for every $j$ such that $0 \le j \le i-1$, we let $H_j = G_j$ and $d_{j+1} = c_{j+1}$.

* we let $H_i = G_i c_{i+1} G_{i+1}$.

* for every $j$ such that $i+1 \le j \le n$, we let $d_j = c_{j+1}$ and $H_j = G_{j+1}$.

Finally, we define $H_i = \{f_i(\tilde{G}) | \tilde{G} \in G_i\}$. Observe that since $G_i \in SF(C)$, $\{c_{i+1}\} \in SF(C)$ and $SF(C)$ is closed under concatenation, it is immediate that $H_i \in SF(C)$.
We can now define the n-blueprint L_φ. We let,

$$L_{\varphi} = \left( \bigcup_{0 \le i \le n+1} L_i \right) \cup \left( \bigcup_{0 \le i \le n} H_i \right).$$

It is clear that L_φ is an n-blueprint such that L_φ ∈ SF(C) since this is the case for all sets L_i and H_i by definition. Hence, it remains to verify that (12) is satisfied. Let w ∈ A* and μ : X → Pos(w) a correct assignment. We prove that w, μ |= L_φ ⇔ w, μ |= φ. There are two directions.

First, assume that w, μ |= φ. We prove that w, μ |= L_φ. Since φ := “∃y ψ”, there exists an assignment γ : X ∪ {y} → Pos(w) such that γ(x) = μ(x) for all x ∈ X and w, γ |= ψ (note that at this stage, γ is not a “correct assignment”: indeed, this is not well-defined since we have not specified any linear ordering on X ∪ {y} yet. We distinguish two cases. First, assume that there exists i satisfying 0 ≤ i ≤ n + 1 and γ(y) = γ(x_i) = μ(x_i). In that case, one can check from the definitions that w, γ |= ψ entails w, μ |= ψ_i. By definition of ψ_i, it follows that w, μ |= L_i and therefore that w, μ |= L_φ as desired, since L_i ⊆ L_φ. In the second case, since μ(x_0) = 0 and μ(x_{n+1}) = |w| + 1 (by definition of increasing assignments), there exists i such that 0 ≤ i ≤ n and μ(x_i) < γ(y) < μ(x_{i+1}). Hence, γ can be viewed as a correct assignment γ : Y_i → Pos(w). Since w, γ |= ψ, it follows that w, γ |= G_i by definition of G_i. One can then verify from the definition of H_i from G_i that w, μ |= H_i. Consequently, w, μ |= L_φ again, since H_i ⊆ L_φ by definition.

We turn to the converse implication. Assume that w, μ |= L_φ. We prove that w, μ |= φ. By definition of L_φ as the union of smaller n-blueprints, there are two cases. In the first case, we assume that there exists i such that 0 ≤ i ≤ n + 1 and w, μ |= L_i. By definition of L_i, it follows that w, μ |= ψ_i. Moreover, by definition of ψ_i from ψ, this implies that w, γ |= ∃y ψ where γ : X ∪ {y} → Pos(w) is the assignment defined by γ(x) = μ(x) for every x ∈ X and γ(y) = μ(x_i). Thus, since φ := “∃y ψ”, it follows that w, μ |= φ, as desired. In the second case, we assume that there exists i such that 0 ≤ i ≤ n and w, μ |= H_i. By definition of H_i from G_i, one can verify that there exists a correct assignment γ : Y_i → Pos(w) such that μ(x) = γ(x) for every x ∈ X and w, γ |= G_i. By definition of G_i, it follows that w, γ |= ψ. Since φ := “∃y ψ”, it follows that w, μ |= φ, concluding the proof of Proposition E.2. □

In view of the discussion following the statement of Proposition E.2, this concludes the inclusion FO(Ι<sub>C</sub>) ⊆ SF(C), and therefore the proof of Theorem 6.6. □

## F Proofs of Section 7

This appendix provides the proofs for statements that connect the expressiveness of the generic version of linear time temporal logic with star-free closure. We start with two useful lemmas for building LTL[C]-formulas.

**LEMMA 7.3.** Let B be an alphabet, η : B* → N be a morphism into a finite monoid and L ∈ LTL(η). There exists a formula φ ∈ LTL[η] such that for every w ∈ B* and i ∈ Pos(w) we have w, i |= φ if and only if w(i, |w| + 1) ∈ L.

**PROOF.** By definition, there exists a formula φ ∈ LTL[η] such that L(φ) = L. Moreover, as φ is evaluated at the leftmost unlabeled position in words, we may assume without loss of generality that φ is a Boolean combination of formulas of the form ψ_1 U_H ψ_2. Since LTL[η] formulas only contain “until” modalities by definition, it can now be verified that for every w ∈ B* and i ∈ Pos(w) we have w, i |= φ if and only if w(i, |w| + 1) ∈ L. □

**LEMMA 7.4.** Let B be an alphabet, η : B* → N be a morphism into a finite monoid, L ∈ LTL(η) and ζ ∈ LTL[η]. There exists a formula φ ∈ LTL[η] such that for all w ∈ B* and i ∈ Pos(w), we have w, i |= φ if and only if there exists j ∈ Pos(w) satisfying the three following conditions:
(1) $i < j$ and for all $k \in \text{Pos}(w)$ such that $i < k < j$, we have $w, k \not\models \zeta$,

(2) $w, j \models \zeta$, and

(3) $w(i, j) \in L$.

PROOF. Lemma 7.3 yields a formula $\psi \in \text{LTL}[\eta]$ such that for every $w \in B^*$ and $i \in \text{Pos}(w)$ we have $w, i \models \psi$ if and only if $w(i, |w| + 1) \in L$. We build a new formula $\psi'$ by applying the two following modifications to $\psi$:

* we replace every occurrence of the atomic formula $\max$ by $\zeta$.

* we recursively replace every sub-formula of the form $\psi_1 U_H \psi_2$ by $\neg\zeta \wedge ((\psi_1 \wedge \neg\zeta) U_H \psi_2)$.

It can now be verified that the formula $\varphi := (\text{F } \zeta) \wedge \psi'$ satisfies the property described in the lemma. $\square$

We now proceed to the main result of this section, which provides a characterization of the expressiveness of the generic version of linear time temporal logic, whether or not past operators are included.

THEOREM 7.5. Let $\mathcal{C}$ be a prevariety. Then, $\text{SF}(\mathcal{C}) = \text{LTL}(\mathcal{C}) = \text{LTLP}(\mathcal{C})$.

PROOF. We fix a prevariety $\mathcal{C}$ for the proof. The inclusion $\text{LTL}(\mathcal{C}) \subseteq \text{LTLP}(\mathcal{C})$ is trivial. We prove that $\text{LTLP}(\mathcal{C}) \subseteq \text{SF}(\mathcal{C})$ and $\text{SF}(\mathcal{C}) \subseteq \text{LTL}(\mathcal{C})$. Let us start with the former, which is simpler.

**Inclusion** $\text{LTLP}(\mathcal{C}) \subseteq \text{SF}(\mathcal{C})$. The proof is based on Theorem 6.6. It states the equality $\text{SF}(\mathcal{C}) = \text{FO}(\mathbb{I}_e)$. Thus, it suffices to prove that $\text{LTLP}(\mathcal{C}) \subseteq \text{FO}(\mathbb{I}_e)$. Let $\varphi$ be an $\text{LTLP}[\mathcal{C}]$ formula. We use structural induction on $\varphi$ to build an $\text{FO}(\mathbb{I}_e)$ formula $[\varphi](x)$ with at most one free variable $x$ which satisfies the following condition:

$$ \text{for all } w \in A^* \text{ and } i \in \text{Pos}(w), \quad w, i \models \varphi \quad \text{if and only if} \quad w, x \mapsto i \models [\varphi](x), \quad (13) $$

where $x \mapsto i$ denotes the assignment that maps $x$ to $i$. It will then be immediate that the language $L \subseteq A^*$ defined by the $\text{LTL}[\mathcal{C}]$ formula $\varphi$ (i.e., $L = \{w \in A^* | w \models \varphi\}$) is defined by the $\text{FO}(\mathbb{I}_e)$ sentence $[\varphi](\text{min})$ (which is obtained from $[\varphi](x)$ by replacing every free occurrence of the variable $x$ by the constant $\text{min}$). Hence, we obtain $\text{LTLP}(\mathcal{C}) \subseteq \text{FO}(\mathbb{I}_e)$ as desired.

If $\varphi = \top$, then we let $[\varphi](x) := (\text{min} = \text{min})$. If $\varphi = \text{min}$ or $\varphi = \text{max}$, then we define $[\varphi](x) := (x = \text{min})$ or $[\varphi](x) := (x = \text{max})$, respectively. If $\varphi = a$ for some $a \in A$, then we let $[\varphi](x) := a(x)$. Logical connectives are handled in the usual way. It remains to treat the temporal operators *until* and *since*.

(1) If $\varphi = \varphi_1 U_L \varphi_2$ for some $L \in \mathcal{C}$, we define:

$$ [\varphi](x) := \exists x_2 I_L(x, x_2) \wedge [\varphi_2](x_2) \wedge \forall x_1 (x < x_1 \wedge x_1 < x_2) \Rightarrow [\varphi_1](x_1). $$

(2) If $\varphi = \varphi_1 S_L \varphi_2$ for some $L \in \mathcal{C}$, we define:

$$ [\varphi](x) := \exists x_2 I_L(x_2, x) \wedge [\varphi_2](x_2) \wedge \forall x_1 (x_2 < x_1 \wedge x_1 < x) \Rightarrow [\varphi_1](x_1). $$

It is simple to check that this construction satisfies (13), as desired.

**Inclusion** $\text{SF}(\mathcal{C}) \subseteq \text{LTL}(\mathcal{C})$. Let $L \in \text{SF}(\mathcal{C})$. We prove that $L \in \text{LTL}(\mathcal{C})$. The argument is based on Theorem 5.11 which implies that all the $\mathcal{C}$-orbits for the syntactic morphism $\alpha : A^* \to M$ of $L$ are aperiodic. We use this hypothesis and induction to construct an $\text{LTL}[\mathcal{C}]$ formula defining $L$. This implies that $L \in \text{LTL}(\mathcal{C})$, as desired.

The construction borrows ideas from the argument of Theorem 5.11, which proves that under the same hypotheses on $L$, we have $L \in \text{SD}(\mathcal{C})$. Yet, there are key differences, as $\text{LTL}(\mathcal{C})$ and $\text{SD}(\mathcal{C})$ are distinct formalisms. In particular, as mentioned above, we shall consider auxiliary alphabets independent from $A$. We start with preliminary definitions aimed at manipulating them.
First, each time we consider an auxiliary alphabet $B$, we shall have to recast the morphism $\alpha : A^* \to M$ into a morphism $\beta : B^* \to M$ and reformulate on $\beta$ the hypothesis that all $C$-orbits for $\alpha$ are aperiodic. For this, we consider another morphism $\eta : B^* \to N$ into a finite monoid. Roughly, $\eta$ is used as an abstraction of the class $C$ over the alphabet $B$. We say that the pair $(\beta, \eta)$ is *tame* to indicate that the following property holds:

$$ \text{For all } u, v \in B^*, \text{ if } \eta(u) = \eta(v) \text{ and } \beta(u) \in E(M), \text{ then } (\beta(uvu))^\omega = (\beta(uvu))^\omega + 1. \quad (14) $$

We first connect this definition to our hypothesis in the following simple fact.

**FACT F.1.** *There exists a $C$-morphism $\eta : A^* \to N$ such that the pair $(\alpha, \eta)$ is tame.*

**PROOF.** Lemma 5.3 yields a $C$-morphism $\eta : A^* \to N$ such that for every $u, v \in A^*$, if $\eta(u) = \eta(v)$, then $(\alpha(u), \alpha(v))$ is a $C$-pair. Since all $C$-orbits for $\alpha$ are aperiodic by hypothesis, it follows that if we additionally know that $\alpha(u) \in E(M)$, then $(\alpha(uvu))^\omega = (\alpha(uvu))^\omega + 1$. Hence, (14) holds and $(\alpha, \eta)$ is tame. $\square$

Given an alphabet $B$, a morphism $\eta : B^* \to N$ into a finite monoid and $P \subseteq B^*$, we define an LTL($\eta$)-partition of $P$ as a finite partition $K$ of $P$ into languages of LTL($\eta$). Moreover, given a morphism $\beta : B^* \to M$ (where $M$ is the original finite monoid used in $\alpha$) and $s \in M$, we say that $K$ is $(\eta, \beta, s)$-safe to indicate that for every $K \in K$ and every $w, w' \in K$, we have $\eta(w) = \eta(w')$ and $\beta(w)s = \beta(w')s$. We can now start the proof. The argument is based on the following lemma.

**LEMMA F.2.** *Let $B$ be an alphabet and consider a morphism $\beta : B^* \to M$ into the fixed monoid $M$ and another morphism $\eta : B^* \to N$ into a finite monoid such that $(\beta, \eta)$ is tame. Let $C \subseteq B$ and $s \in M$. Then, there exists an $(\eta, \beta, s)$-safe LTL($\eta$)-partition of $C$.*

Let us first apply Lemma F.2 to prove that $L \in \text{LTL}(C)$. Fact F.1 yields a $C$-morphism $\eta : A^* \to N$ such that the pair $(\alpha, \eta)$ is tame. Since $\eta$ is a $C$-morphism, LTL($\eta$) $\subseteq$ LTL($C$). Hence, it suffices to prove that $L \in \text{LTL}(\eta)$. We apply the lemma for $B = C = A$, $\beta = \alpha$ and $s = 1_M$. This yields an $(\eta, \alpha, 1_M)$-safe LTL($\eta$)-partition $K$ of $A^*$. Now, $K$ being $(\eta, \alpha, 1_M)$-safe implies that for every $K \in K$, there exists $s \in M$ such that $K \subseteq \alpha^{-1}(s)$. Since $K$ is a partition of $A^*$ and $L$ is recognized by $\alpha$, it follows that $L$ is a union of languages of $K$. Since LTL($\eta$) is closed under union, it follows that $L$ itself belongs to LTL($\eta$), which completes the main argument.

It remains to prove Lemma F.2. Let $B$ be an alphabet and consider two morphisms $\beta : B^* \to M$ and $\eta : B^* \to N$ such that $(\beta, \eta)$ is tame. Moreover, let $C \subseteq B$ and $s \in M$. We build an LTL($\eta$)-partition of $C^*$ which is $(\eta, \beta, s)$-safe using induction on the three following parameters listed by order of importance:

(1) The size of $\beta(C^+) \subseteq M$.

(2) The size of $C$.

(3) The size of $\beta(C^*) \cdot s \subseteq M$.

**REMARK F.3.** As already mentioned, the proof is similar to that of Theorem 5.11. In particular, the current proof resembles to that of Corollary 5.13. The reader may wonder why the element $s$, which serves as a buffer in these proofs, is not on the same side. The reason is that it was easier to consider $\alpha(C^*)$ in Corollary 5.13, due to the fact that $P$ is a prefix code, while it is easier to consider $\beta(C^*) \cdot s$ here, due to the fact that we are dealing with pure future linear time temporal logic.

We distinguish two cases depending on the following property of $\beta$, $C$ and $s$. We say that $s$ is $(\beta, C)$-stable when the following holds:

$$ \text{for every } c \in C, \quad \beta(C^*) \cdot s = \beta(cC^*) \cdot s. \quad (15) $$
We first consider the case when $s$ is $(\beta, C)$-stable. This is the base case. Otherwise, we use induction on our three parameters.

**Base case:** $s$ is $(\beta, C)$-stable. In that case, we define $K = \{C^* \cap \eta^{-1}(t) \mid t \in N\}$. Clearly, this is a finite partition of $C^*$. Moreover, it is clear that $C^* \cap \eta^{-1}(t) \in \text{LTL}(\eta)$ for every $t \in N$. Indeed, it is defined by the LTL$[\eta]$ formula $((\bigvee_{c \in C} c) \text{U}_{\eta^{-1}(t)} \max)$.

It remains to show that $K$ is $(\eta, \beta, s)$-safe. We use the hypothesis that $(\beta, \eta)$ is tame. First, we use the hypothesis that $s$ is $(\beta, C)$-stable to prove the following statement, analogous to Fact 5.17.

**FACT F.4.** Let $q, f \in \beta(C^*)$ such that $f$ is idempotent. Then, we have $fqs = qs$.

**PROOF.** The proof is based on the following preliminary result. For $u, v \in C^*$, we show that, there exists $r \in \beta(C^*)$ such that $\beta(u)rs = \beta(v)s$. (16)

We fix $u, v \in C^*$ for the proof of (16). We use induction on the length of $u$. If $u = \varepsilon$, it suffices to choose $r = \beta(v) \in \beta(C^*)$. Otherwise, $u = u'c$ with $u' \in C^*$, $c \in C$. Induction yields $r' \in \beta(C^*)$ such that $\beta(u')r's = \beta(v)s$. Moreover, since $s$ is $(\beta, C)$-stable and $r' \in \beta(C^*)$, it follows from (15) that there exists $r \in \beta(C^*)$ such that $r's = \beta(c)rs$. Altogether, this yields $\beta(u')\beta(c)rs = \beta(v)s$ and as $u = u'c$, we get $\beta(u)rs = \beta(v)s$, concluding the proof of (16).

We now prove the fact. Let $q, f \in \beta(C^*)$ such that $f$ is idempotent. By definition, we $u, v \in C^*$ such that $q = \beta(v)$ and $f = \beta(u)$. Thus, (16) yields $r \in \alpha(C^*)$ such that $frs = qs$. As $f$ is idempotent, this implies that $fqs = ffrs = frs = qs$. $\square$

We now prove that every $K \in K$ is $(\eta, \beta, s)$-safe. By definition, $K = C^* \cap \eta^{-1}(t)$ for $t \in N$. Given $u, v \in K$, we have to show that $\eta(u) = \eta(v)$ and $\beta(u)s = \beta(v)s$. Let $n = \omega(M)$. Since $u, v \in K$, we have $\eta(u) = \eta(v) = t$. Hence, $\eta(u^n) = \eta(u^{n-1}v)$ and since $\beta(u^n)$ is idempotent, the hypothesis that $(\beta, \eta)$ is tame yields $(\beta(u^{2n-1}vu^n))^n = (\beta(u^{2n-1}vu^n))^{n+1}$. We now multiply by $s$ on the right to obtain $(\beta(u^{2n-1}vu^n))^{ns} = (\beta(u^{2n-1}vu^n))^{n+1}s$. Since $n = \omega(M)$, we know that $(\beta(u^{2n-1}vu^n))^n$ is an idempotent of $\beta(C^*)$. Therefore, Fact F.4 yields $(\beta(u^{2n-1}vu^n))^{ns} = s$. Altogether, we obtain that $s = \beta(u^{2n-1}vu^n)s$. We now multiply by $\beta(u)$ on the left to get $\beta(u)s = \beta(u^{2n}vu^n)s$. Finally, as $\beta(u^n) \in \beta(C^*)$ is an idempotent, we may apply Fact F.4 twice to get $\beta(u^{2n}vu^n)s = \beta(v)s$. Altogether, this yields $\beta(u)s = \beta(v)s$, as desired.

**Inductive case:** $s$ is not $(\beta, C)$-stable. By hypothesis, there exists some letter $c \in C$ such that the following property holds:

$$ \beta(cC^*) \cdot s \subsetneq \beta(C^*) \cdot s. \quad (17) $$

We fix this letter $c \in C$ for the rest of the argument and we let $D$ be the sub-alphabet $D = C \setminus \{c\}$.

The restrictions $\beta: D^* \to M$ and $\eta: D^* \to N$ still form a tame pair $(\beta, \eta)$. Therefore, we may apply induction in Lemma F.2 when replacing $C$ by $D$. Indeed, the first induction parameter (the size of $\beta(C^*)$) has not increased here since $D \subseteq C$ and $\beta$ remains unchanged, while the second parameter has decreased: $|D| < |C|$. This yields an $(\eta, \beta, 1_M)$-safe LTL$(\eta)$-partition $\mathbf{H}$ of $D^*$. We can assume without loss of generality that $H \neq \emptyset$ for every $H \in \mathbf{H}$.

**FACT F.5.** There exists an $(\eta, \beta, 1_M)$-safe LTL$(\eta)$-partition $\mathbf{H}$ of $D^*$ made of nonempty languages.

We distinguish two independent subcases. Observe that the inclusion $\beta(cC^*) \subseteq \beta(C^+)$ holds. The argument differs depending on whether it is strict or not.

**Subcase 1:** $\beta(cC^*) = \beta(C^+)$. We use induction on our third parameter (i.e., the size of $\beta(C^*)s$). Let $H \in \mathbf{H}$. Since $\mathbf{H}$ is a partition of $D^*$ which is $(\eta, \beta, 1_M)$-safe by definition and $H \neq \emptyset$, there exists a unique element $t_H \in \beta(D^*)$ such that $\beta(x) = t_H$ for every $x \in \mathbf{H}$. The construction of $K$ is based on the following fact (this is where we use induction).
FACT F.6. For all $H \in \mathbf{H}$, there exists an $(\eta, \beta(c)t_{HS})$-safe LTL$(\eta)$-partition $U_H$ of $C^*$.

PROOF. We fix $H \in \mathbf{H}$. Since $t_H \in \beta(D^*)$, we have $\beta(c)t_{HS} \in \beta(cD^*)s$. Therefore, we have $\beta(C^*)\beta(c)t_{HS} \subseteq \beta(C^+)s$. Combined with our hypothesis in Subcase 1 (i.e., $\beta(cC^*) = \beta(C^+$)), this yields $\beta(C^*)\beta(c)t_{HS} \subseteq \beta(cC^*)s$. Finally, we obtain from (5) (i.e., $\beta(cC^*)s \subseteq \beta(C^*)s$) that the strict inclusion $\beta(C^*)\beta(c)t_{HS} \subseteq \beta(C^*)s$ holds. Hence, we may apply induction on our third parameter in Lemma F.2 (i.e., the size of $\beta(C^*)s$) to obtain the desired finite partition $U_H$ of $C^*$ which is $(\eta, \beta(c)t_{HS})$-safe. Note that here, our first two parameters have not increased as $\beta$ and $C$ remain unchanged. $\square$

We can now define the desired partition $K$ of $C^*$. Using the partitions $U_H$ given by Fact F.6, we define,

$$K = H \cup \{UcH \mid H \in H \text{ and } U \in U_H\}.$$

It remains to show that $K$ is indeed an LTL$(\eta)$-partition of $C^*$ which is $(\eta, \beta, s)$-safe. One can verify that $K$ is a partition of $C^*$ since $H$ is a partition of $D^*$ and $U_H$ is a partition of $C^*$ for every $H \in \mathbf{H}$ (recall that $D = C \setminus \{c\}$). Let us prove that every $K \in K$ belongs to LTL$(\eta)$. This is immediate if $K \in H$ by hypothesis on $H$. Otherwise, there exist $H \in H$ and $U \in U_H$ such that $K = UcH$. Since $H \in LTL(\eta)$, it follows from Lemma 7.3 that there exists a formula $\psi_H \in LTL[\eta]$ such that for every $w \in B^*$ and every $i \in \text{Pos}(w)$, we have $w, i \models \psi_H$ if and only if $w(i, |w|+1) \in H$. Moreover, let $\zeta \in \text{LTL}[\eta]$ be the formula $\zeta := c \wedge \neg F c$ (given a word $w \in B^*$ and $i \in \text{Pos}(w)$, we have $w, i \models \zeta$ if and only if $i$ is the rightmost position in $w$ carrying the letter $c$). Since $U \in \text{LTL}(\eta)$ (by definition of $U_H$), Lemma 7.4 yields a formula $\psi_U \in \text{LTL}[\eta]$ such that for every $w \in B^*$, we have $w \models \psi_U$ if and only if there exists $j \in \text{Pos}(w)$ such that $w, j \models \zeta$ (by definition of $\zeta$, $j$ must be unique) and $w(0, j) \in U$. Since $c \notin D$ and $H \subseteq D^*$, one can now check that $K = UcH$ is defined by the formula $\psi_U \wedge F(\zeta \wedge \psi_H)$. Hence, we get $K \in \text{LTL}(\eta)$, as desired.

It remains to prove that $K$ is $(\eta, \beta, s)$-safe. Consider $K \in K$ and $w, w' \in K$. We have to show that $\eta(w) = \eta(w')$ and $\beta(w)s = \beta(w')s$. By definition of $K$, there are two cases: first, if $K \in H$ we know by Fact F.5 that $H$ is an $(\eta, \beta, 1_M)$-safe LTL$(\eta)$-partition of $D^*$. Therefore, we obtain $\eta(w) = \eta(w')$ and $\beta(w) = \beta(w')$, whence $\beta(w)s = \beta(w')s$, as desired. Otherwise, $K = UcH$ with $H \in H$ and $U \in U_H$. Thus, we get $x, x' \in H$ and $u, u' \in U$ such that $w = ucx$ and $w' = u'cx'$. By definition of $t_H$, we have $\beta(x) = \beta(x') = t_H$. Moreover, since $H$ is $(\eta, \beta, 1_M)$-safe and $U_H$ is $(\eta, \beta(c)t_{HS})$-safe by Fact F.6, we also have $\eta(x) = \eta(x')$ and $\eta(u) = \eta(u')$, whence $\eta(w) = \eta(w')$. Finally, $\beta(w)s = \beta(u)\beta(c)t_{HS}$ and $\beta(w')s = \beta(u')\beta(c)t_{HS}$ and since $U_H$ is $(\eta, \beta(c)t_{HS})$-safe, we obtain $\beta(w)s = \beta(w')s$. This concludes the proof of this subcase.

**Subcase 2:** $\beta(cC^*) \subseteq \beta(C^+)$. We use induction on our first parameter (i.e., the size of $\beta(C^+)$$^*$). Consider a word $w \in C^*$. Since $D = C \setminus \{c\}$, $w$ admits a unique decomposition $w = uv$ such that $u \in D^*$ and $v \in (cD^*)^*$ (i.e., $u$ is the largest prefix of $w$ in $D^*$ and $v$ is the corresponding suffix). Using induction, we construct LTL$(\eta)$-partitions of the possible prefixes and suffixes. Then, we combine them to construct a partition of the whole set $C^*$. Actually, note that we already partitioned the set of prefixes: we have an LTL$(\eta)$-partition $H$ of $D^*$ which is $(\eta, \beta, 1_M)$-safe. It remains to partition the set of suffixes: this is where we use induction.

LEMMA F.7. There exists an LTL$(\eta)$-partition $V$ of $(cD^*)^*$ which is $(\eta, \beta, 1_M)$-safe.

PROOF. For each language $H \in \mathbf{H}$, we create a letter $\mathbb{D}_H$ and let $\mathbb{B} = \{\mathbb{D}_H \mid H \in \mathbf{H}\}$ be a new alphabet. Moreover, we define new morphisms $\gamma : \mathbb{B}^* \to M$ and $\delta : \mathbb{B}^* \to N$. Let $H \in \mathbf{H}$ and consider the letter $\mathbb{D}_H$. Since $H$ is a partition of $D^*$ which is $(\eta, \beta, 1_M)$-safe by definition and $H \neq \emptyset$, there exist unique elements $t_H \in \beta(D^*)$ and $q_H \in \eta(D^*)$ such that $\eta(x) = q_H$ and $\beta(x) = t_H$ for every $x \in H$. We let $\gamma(\mathbb{D}_H) = \beta(c)t_H$ and $\delta(\mathbb{D}_H) = \eta(c)q_H$.
Observe that the pair $(\gamma, \delta)$ is tame. Indeed, let $u, v \in \mathbb{B}^*$ such that $\delta(u) = \delta(v)$ and $\gamma(u) \in E(M)$. By definition of $\mathbb{B}$, there exist $w_u, w_v \in (cD^*)^*$ such that $\gamma(u) = \beta(w_u)$, $\gamma(v) = \beta(w_v)$, $\delta(u) = \eta(w_u)$ and $\delta(v) = \eta(w_v)$. Hence, $\eta(w_u) = \eta(w_v)$ and $\beta(w_u) \in E(M)$. Since $(\beta, \eta)$ is tame, it then follows from (14) that $(\beta(w_u w_v w_u))^\omega = (\beta(w_u w_v w_u))^{\omega+1}$. This exactly says that $(\gamma(uvu))^\omega = (\gamma(uvu))^{{\omega+1}}$, as desired. Moreover, by definition of $\mathbb{B}$, one can verify that $\gamma(\mathbb{B}^+) = \beta((cD)^+) \subseteq \beta(cC^*)$. Hence, since $\beta(cC^*) \subseteq \beta(C^+)$ (this is our hypothesis in Subcase 2), we get $|\gamma(\mathbb{B}^+)| < |\beta(C^+)|$. Consequently, we may apply induction on the first parameter in Lemma F.2 (i.e., the size of $\beta(C^+)$) to get an LTL($\delta$)-partition $G$ of $\mathbb{B}^*$ which is $(\delta, \gamma, 1_M)$-safe. We use it to construct $V$.

First, we define a map $\mu : (cD^*)^* \to \mathbb{B}^*$. Observe that since $c \notin D$, every word $u \in (cD^*)^*$ admits a unique decomposition $u = cu_1 \cdots cu_n$ with $u_1, \dots, u_n \in D^*$. For every $i \le n$, we let $H_i$ be the unique language in $H$ such that $u_i \in H_i$ (recall that $H$ is partition of $D^*$). We then define $\mu(w) = \mathbb{D}_{H_1} \cdots \mathbb{D}_{H_n}$. Note that by definition, each position $i \in \text{Pos}(w)$ which is labeled by a “c” corresponds to a unique position in $\mu(w)$. We can now define $V = \{\mu^{-1}(G) \mid G \in G\}$. It remains to show that $V$ is an LTL($\eta$)-partition of $(cD^*)^*$ which is $(\eta, \beta, 1_M)$-safe. Clearly, $V$ is a partition of $(cD^*)^*$ by definition since $G$ is a partition of $\mathbb{B}^*$.

We first prove that every $V \in V$ belongs to LTL($\eta$). By definition, $V = \mu^{-1}(G)$ for some $G \in G$. Let $\zeta := c \lor \max \in \text{LTL}[\eta]$. We know that every $H \in H$ belongs to LTL($\eta$). Hence, Lemma 7.4 yields a formula $\psi'_H \in \text{LTL}[\eta]$ such that for every $w \in B^*$ and $i \in \text{Pos}(w)$, we have $w, i \models \psi'_H$ if and only if there exists $j \in \text{Pos}(w)$ such that $i < j, w, j \models \zeta, w, k \not\models \zeta$ for every $i < k < j$ and $w(i, j) \in H$. We let $\psi_H = c \wedge \psi'_H$. By definition, $w, i \models \psi'_H$ if and only if $i$ has label $c$ and the greatest prefix of $w(i, |w| + 1)$ which is in $D^*$ belongs to $H$. The key idea is that when $w \in (cD^*)^*$, the formula $\psi_H$ holds for the positions $i \in \text{Pos}(w)$ which are labeled by $c$ and such that the position of $\mu(w) \in \mathbb{B}^*$ corresponding to $i$ is labeled by $\mathbb{D}_H \in \mathbb{B}$. Moreover, since $G \in G$, there exists an LTL[$\delta$] formula $\Gamma_G$ defining $G$ by hypothesis on $G$. We modify $\Gamma_G$ into an LTL[$\eta$] formula $\varphi_V$ defining $V = \mu^{-1}(G)$. First, let $\varphi'_V$ be the formula obtained from $\Gamma_G$ by applying the two following modifications:

(1) We replace each atomic sub-formula “$\mathbb{D}_H$” for $H \in H$ by the LTL[$\eta$] formula $\psi_H$.

(2) We recursively replace all sub-formulas $\varphi_1 U_X \varphi_2$. Since $\Gamma_G$ is an LTL[$\delta$]-formula, we have $F \subseteq N$ such that $X = \delta^{-1}(F)$. We recursively replace $\varphi_1 U_X \varphi_2$ by,

$$ (X \ \zeta \wedge (\zeta \Rightarrow \varphi_1) \ U_{\eta^{-1}(F)} \ (\zeta \wedge \varphi_2)) \lor ((\neg X \ \zeta) \wedge ((\neg X \ \zeta) \ U (X \ \zeta \wedge ((\zeta \Rightarrow \varphi_1) \ U_{\eta^{-1}(F)} \ (\zeta \wedge \varphi_2))))) $$

Finally, we let $\varphi_V := X (c \lor \max) \wedge \varphi'_V$. One can now check from the definition that $\varphi_V$ defines $V = \mu^{-1}(G)$.

It remains to prove that $V$ is $(\eta, \beta, 1_M)$-safe. Let $V \in V$ and $v, v' \in V$. By definition, there exists $G \in G$ such that $V = \mu^{-1}(G)$. Hence, we have $\mu(v), \mu(v') \in G$ and since $G$ is $(\delta, \gamma, 1_M)$-safe, this yields $\gamma(\mu(v)) = \gamma(\mu(v'))$ and $\delta(\mu(v)) = \delta(\mu(v'))$. One can verify that $\delta(\mu(v)) = \eta(v)$, $\delta(\mu(v')) = \eta(v')$, $\gamma(\mu(v)) = \beta(v)$ and $\gamma(\mu(v')) = \beta(v')$. Thus, we get $\beta(v) = \beta(v')$ and $\delta(v) = \delta(v')$, concluding the proof. $\square$

We are ready to build our LTL($\eta$)-partition $K$ of $C^*$. Let $V$ be the $(\eta, \beta, 1_M)$-safe LTL($\eta$)-partition of $(cD^*)^*$ given by Lemma F.7. We let,

$$ K = \{HV \mid H \in H \text{ and } V \in V\}. $$

It is immediate by definition that $K$ is a partition of $C^*$ since $D = C \setminus \{c\}$ and $H$ is a partition of $D^*$. Let us verify that every $K \in K$ belongs to LTL($\eta$). By definition, one can write $K = HV$ for some $H \in H$ and $V \in V$. Let $\zeta := c \lor \max$. Since $H \in \text{LTL}(\eta)$, Lemma 7.4 yields an LTL[$\eta$] formula $\psi_H$ such that for every $w \in B^*$, we have $w \models \psi_H$ if and only if there exists $j \in \text{Pos}(w) \setminus \{0\}$ such that
$w, j \models \zeta$, $w, k \not\models \zeta$ for every $k \in \text{Pos}(w)$ such that $0 < k < j$ and $w(0, j) \in H$. Since $V \in \text{LTL}(\eta)$ (by hypothesis on $V$), Lemma 7.3 yields an LTL[$\eta$] formula $\psi_V$ such that for every $w \in B^*$ and every $i \in \text{Pos}(w)$, we have $w, i \models \psi_V$ if and only if $w(i, |w| + 1) \in V$. One can now check that $K = HV$ is defined by the formula,

$$ \psi_H \wedge ((X \zeta \wedge \psi_V) \vee ((\neg X \zeta) \wedge ((\neg X \zeta) \vee (X \zeta \wedge \psi_V)))) . $$

Hence, we get $K \in \text{LTL}(\eta)$. It remains to verify that $K$ is $(\eta, \beta, s)$-safe (it is in fact $(\eta, \beta, 1_M)$-safe). Let $K \in K$ and $w, w' \in K$, we show that $\eta(w) = \eta(w')$ and $\beta(w) = \beta(w')$ (which implies $\beta(w)s = \beta(w')s$). By definition, $K = HV$ with $H \in H$ and $V \in V$. Therefore, $w = uv$ and $w' = u'v'$ with $u, u' \in H$ and $v, v' \in V$. Since $H$ and $V$ are both $(\eta, \beta, 1_M)$-safe by definition, we have $\eta(u) = \eta(u')$, $\beta(u) = \beta(u')$, $\eta(v) = \eta(v')$ and $\beta(v) = \beta(v')$. It follows that $\eta(w) = \eta(w')$ and $\beta(w) = \beta(w')$ which concludes the proof. $\square$

## G Proofs of Section 8

In this short appendix, we sketch the proof of Proposition 8.8. More context is available in [40].

**PROPOSITION 8.8.** Let $\mathcal{D}$ be a Boolean algebra. There exists an effective reduction from $\mathcal{D}$-covering to the following problem:

**Input:** A nice multiplicative rating map $\rho : 2^{A^*} \to R$ and $F \subseteq R$.

**Question:** Is it true that $\mathcal{J}_{\mathcal{D}}[\rho] \cap F = \emptyset$?

**PROOF SKETCH.** We briefly describe the reduction (we refer the reader to [40] for details). Consider an input pair $(L_0, \{L_1, \dots, L_n\})$ for $\mathcal{D}$-covering. Since the languages $L_i$ are regular, for every $i \le n$, one can compute a morphism $\alpha_i : A^* \to M_i$ into a finite monoid recognizing $L_i$ together with the set $F_i \subseteq M_i$ such that $L_i = \alpha_i^{-1}(F_i)$. Consider the associated nice multiplicative rating maps $\rho_{\alpha_i} : 2^{A^*} \to 2^{M_i}$. Moreover, let $R$ be the idempotent semiring $2^{M_0} \times \dots \times 2^{M_n}$ equipped with the componentwise addition and multiplication. We define a nice multiplicative rating map $\rho : 2^{A^*} \to R$ by letting $\rho(K) = (\rho_{\alpha_0}(K), \dots, \rho_{\alpha_n}(K))$ for every $K \subseteq A^*$. Finally, let $F \subseteq R$ be the set of all tuples $(X_0, \dots, X_n) \in R$ such that $X_i \cap F_i \ne \emptyset$ for every $i \le n$. One can now verify that $(L_0, \{L_1, \dots, L_n\})$ is $\mathcal{D}$-coverable if and only if $\mathcal{J}_{\mathcal{D}}[\rho] \cap F = \emptyset$. Let us point out that this equivalence is only true when $\mathcal{D}$ is a Boolean algebra. When $\mathcal{D}$ is only a lattice, one has to handle the language $L_0$ separately. $\square$