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

HAL
open science

# Closing Star-Free Closure

Thomas Place, Marc Zeitoun

► To cite this version:

Thomas Place, Marc Zeitoun. Closing Star-Free Closure. ACM Transactions on Computational Logic, 2025, 26 (3), pp.1-62. 10.1145/3733831. hal-05426395

HAL Id: hal-05426395

https://hal.science/hal-05426395v1

Submitted on 19 Dec 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons Attribution 4.0 International License
# Closing star-free closure

THOMAS PLACE and MARC ZEITOUN, LaBRI, Université de Bordeaux, France

We introduce an operator on classes of regular languages, the star-free closure. Our motivation is to generalize standard results of automata theory within a unified framework. Given an arbitrary input class $C$, the star-free closure operator outputs the least class closed under Boolean operations and language concatenation, and containing all languages of $C$ as well as all finite languages. We establish several equivalent characterizations of star-free closure: in terms of regular expressions, first-order logic, pure future and future-past temporal logic, and recognition by finite monoids. A key ingredient is that star-free closure coincides with another closure operator, defined in terms of regular operations where Kleene stars are allowed in restricted contexts.

A consequence of this first result is that we can decide membership of a regular language in the star-free closure of a class whose separation problem is decidable. Moreover, we prove that separation itself is decidable for the star-free closure of any finite class, and of any class of group languages having itself decidable separation (plus mild additional properties). We actually show decidability of a stronger property, called covering.

**CCS Concepts: • Theory of computation → Regular languages; Modal and temporal logics; Finite Model Theory.**

**Additional Key Words and Phrases:** Words, regular languages, star-free closure, first-order logic, linear temporal logic, aperiodicity, membership, separation, covering

**ACM Reference Format:**

Thomas Place and Marc Zeitoun. 2025. Closing star-free closure. *ACM Trans. Comput. Logic* 1, 1 (April 2025), 61 pages. https://doi.org/10.1145/nnnnnnn.nnnnnnn

## 1 Introduction

**Context.** The starting point of this paper is a major result from the theory of regular languages. It states that it is equivalent for a language of finite words to be defined by:

(1) a star-free regular expression, i.e., which forbids Kleene star but allows complement,

(2) a regular expression restricting Kleene stars to prefix codes of bounded synchronization delay,

(3) a first-order logic sentence using the linear order and the alphabetic predicates,

(4) a pure future temporal logic formula,

(5) a future-past temporal logic formula,

(6) a morphism into a finite aperiodic monoid.

This statement compiles a series of theorems by Schützenberger [41, 42] for $(1) ⇔ (2) ⇔ (6)$, McNaughton and Papert [24] for $(3) ⇔ (1)$ and Kamp [17] for $(3) ⇔ (4) ⇔ (5)$. It attests to the robustness of a class of languages defined by seemingly unrelated formalisms: various types of regular expressions, of logics and of machine-based devices. Moreover, Property (6) can be decided on a specific canonical morphism, which can be computed from the language. This yields an

Work supported by ANR-24-CE48-1142, Project UnREAL.

Authors' Contact Information: Thomas Place, tplace@labri.fr; Marc Zeitoun, mz@labri.fr; LaBRI, Université de Bordeaux, Talence, France.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org.

© 2025 Copyright held by the owner/author(s). Publication rights licensed to ACM.

ACM 1557-945X/2025/4-ART

https://doi.org/10.1145/nnnnnnn.nnnnnnn
algorithm for checking whether a given regular language has any of the aforementioned properties. In other words, the *membership problem* of a regular language to this class of languages is decidable.

This result had a profound influence on automata theory: its impact went far beyond the class of star-free languages. By highlighting the correspondence between specific regular expressions, fragments of second-order monadic logic, variants of temporal logic and classes of finite monoids, it initiated a line of research whose aim is to capture the expressive power of natural classes of regular languages—see [26, Part B) or [47] for overviews. As in the theorem above, these classes are defined by restricting the syntax of the aforementioned formalisms. Historically, the way to study such a class was inspired by Schützenberger’s contribution to the above result: the aim was to design *membership algorithms*. There is an abundant literature on the subject, due to the number of interesting classes of regular languages. See for example [43, 19, 6, 27] (for variations on the quantifier alternation free fragment of first-order logic), [30, 14, 21] (for variations on a more expressive fragment) or [49, 7, 20] (for variations on two-variable first-order logic).

**Operators.** The number of publications in the field is also explained by the fact that the investigated classes do not have a unique flavor. Indeed, logic and regular expressions come in a multitude of variants. For example, other versions of first-order logic can be envisaged by allowing more predicates, thus increasing the expressive power. This leads to two classic variants: we can add predicates that test the value of a position modulo a certain integer, and more generally predicates that count the number of occurrences of a particular letter modulo an integer. Similarly, star-free expressions can be extended in a natural way: instead of starting with singleton languages, we can start with languages of a certain fixed class. Finally, there are several extensions of temporal logic, usually obtained by adding more expressive temporal modalities (see for example [13]).

The historical approach has been to treat each variation individually. Hence, the proofs have to be recast for each variation, which is often technical and sometimes nontrivial. To avoid such adaptations, it is desirable to develop a generic approach, which would encompass several variations of a given class at once. This is where the notion of operator comes in. An *operator Op* associates with any class *C* a larger class *Op(C)*. For example, the star-free closure operator *SF* takes as input a class *C* and outputs *SF(C)*, the least class containing *C* and all finite languages, and which is closed under union, complement and concatenation. We recover the class of star-free languages as the star-free closure of the class consisting of two languages: the empty and the full languages.

Focusing on operators rather than on individual classes meets our main objective (understanding classes of regular languages). Indeed, most interesting classes are obtained from simpler ones by applying operators from a small set. The main operators are Boolean and polynomial closure [30] (they appear in concatenation hierarchies, see for example [28]), unambiguous polynomial closure [32] and star-free closure, which is the subject of this paper. It is more rewarding to concentrate on operators, as this allows multiple variants of the same class to be handled at once, leading to *generic* results. Not only this avoids reproducing proofs for classes that are variations of each other, but also and more importantly, this simplifies the proofs and emphasizes the characteristics of the operator *Op* and the assumptions needed on the class *C* to decide *Op(C)-membership*.

Ideally, for an operator *Op*, we would like to reduce *Op(C)-membership* to *C-membership*, i.e., to obtain a statement like: "If *C* has decidable membership, then so does *Op(C)*". Unfortunately, although this situation may occur [32], it is uncommon: decidability of membership is rarely preserved by operators (see [1], which provides negative examples in the context of classes of monoids). This observation leads to the following question:

"What properties should *C* satisfy for the *Op(C)-membership* problem to be decidable?"

This question, in turn, motivates us to consider a new problem: *C-separation*. It asks whether two regular input languages can be separated by a language from the class *C*, i.e., whether there exists a
language from $\mathcal{C}$ containing the first input language while being disjoint from the second. There is an easy algorithmic reduction from $\mathcal{C}$-membership to $\mathcal{C}$-separation: a language belongs to $\mathcal{C}$ if and only if it can be $\mathcal{C}$-separated from its complement. Note that separation is more demanding than membership: it requires to exhibit a separating language, if possible, even when none of the input languages belong to the class under study. In contrast, solving membership only requires to prove that the input language does or does not belong to the class. For this reason separation is also more rewarding than membership: although more difficult, it brings more information, which can later be exploited to tackle classes of languages built on top of the one being investigated.

In particular, looking at separation provides a partial answer to the above question ("what properties should $\mathcal{C}$ satisfy for the $Op(\mathcal{C})$-membership problem to be decidable?"). Indeed, for some operators $Op$, being able to decide $\mathcal{C}$-separation is sufficient to decide $Op(\mathcal{C})$-membership. This is the case when $Op$ is the polynomial closure operator [33] (assuming mild properties on $\mathcal{C}$). If in addition, the class $\mathcal{C}$ consists of group languages (see Section 3.5), this is also the case for the Boolean closure of the polynomial closure [38] (which, in fact, has then decidable separation). For this reason, separation has replaced membership as the standard problem to understand a class of regular languages. It turns out that in order to tackle $\mathcal{C}$-separation, it is convenient to study an even more general problem called $\mathcal{C}$-covering. Intuitively, it generalizes separation to an arbitrary number of input languages. The state of the art regarding the class of star-free languages is that it has decidable covering, hence also decidable separation. This follows from [36] and indirectly from [15, 2].

**Contributions.** We investigate the star-free closure operator. With any class of languages $\mathcal{C}$, it associates the least class $SF(\mathcal{C})$ containing $\mathcal{C}$, all finite languages, and which is closed under Boolean operations and language concatenation. Note that these operations preserve regularity and that Kleene star is explicitly forbidden. We generalize the known results in two orthogonal directions:

* First, we generalize the Kamp-McNaughton-Papert-Schützenberger theorem: we generalize the properties appearing in this theorem, and show that they all characterize star-free closure. In other words, we find suitable operators extending the definition of the classes that appear in this result: languages of bounded synchronization delay, first-order definable languages, languages definable in pure future and future-past temporal logic, and languages recognized by finite aperiodic monoids. An important consequence of the algebraic characterization, is that $SF(\mathcal{C})$-membership reduces to $\mathcal{C}$-separation.

* Secondly, we prove that under certain (strong) assumptions on the input class $\mathcal{C}$, which we detail below, the covering problem for the star-free closure $SF(\mathcal{C})$ is decidable.

Let us comment on these two contributions. Concerning the first, one of the operators we have to define already exists: with each class $\mathcal{C}$, one can associate a variant $FO(\mathbb{I}_{\mathcal{C}})$ of first-order logic whose predicates depend on $\mathcal{C}$ [33]. It defines exactly the languages in the star-free closure of $\mathcal{C}$. Its definition is simple: each language $L$ in $\mathcal{C}$ yields a binary predicate that selects pairs of positions such that the infix between them belongs to $L$. On the other hand, all other operators are new.

The main one is the *SD* operator. It generalizes a class defined by Schützenberger [42] (see also [10, 11]). Roughly speaking, *SD*(*C*) is the least class containing all finite languages which is closed under intersection with languages of *C*, disjoint union, unambiguous concatenation, and Kleene star applied to prefix codes of bounded synchronization delay. Unlike *SF*, the *SD* operator prohibits complement. In fact, the definitions of these operators are of a different nature: the restrictions for *SF* are syntactic (they constrain legal regular expressions), whereas being a disjoint union, an unambiguous concatenation or a prefix code with bounded synchronization delay are semantic notions: they depend on the languages themselves, not just on expressions used to describe them.

The *SD* operator is a key ingredient in the generalization of the Kamp-McNaughton-Papert-Schützenberger theorem: the first step, establishing the inclusion $SD(\mathcal{C}) \subseteq SF(\mathcal{C})$, is particularly
helpful. Indeed, proving inclusion in SF(C) is generally difficult, since this requires the construction of expressions that involve alternating complement and concatenation operations, which are hard to understand. On the other hand, proving inclusion in SD(C) is easier, as we may use Kleene stars. In fact, several of the article's proofs are based on this capability.

The proof of the converse inclusion $SF(C) \subseteq SD(C)$ is intertwined with the algebraic characterization. We generalize Property (6), which involves finite aperiodic monoids. For each morphism into a finite monoid $M$, we associate monoids in $M$ called $C$-orbits. Their computation boils down to $C$-separation. The generalized algebraic characterization states that a language is in $SD(C) = SF(C)$ if and only if all $C$-orbits of its syntactic morphism are aperiodic. In particular, if $C$-separation is decidable, then so is $SF(C)$-membership. This generalizes Schützenberger's membership theorem.

At last, we generalize the correspondences with temporal logic. We define an operator that associates a variant of pure future temporal logic with each class. This simply amounts to generalizing the “Until” temporal modality to take into account the input class $C$. Each language $L$ of $C$ produces a new “Until” modality $U_L$. This modality adds a constraint to the semantic of the standard Until: a formula $\phi_{U_L} \psi$ holds at position $i$ in a word when there exists a position $j > i$ where $\psi$ holds, such that $\phi$ holds on all the intermediate positions, and such that the infix between $i$ and $j$ belongs to $L$. Adapting this construction to future-past temporal logic is straightforward. We show that both temporal logic operators obtained in this way correspond to the star-free closure operator, thus generalizing Properties 4 and 5 of the Kamp-McNaughton-Papert-Schützenberger theorem.

We now turn to the second contribution: covering algorithms for specific input classes. First, we show that the star-free closure of a *finite class* has decidable covering (and therefore, decidable separation). We then use this result to establish our main theorem: the star-free closure of a class of *group languages* with decidable *separation* has decidable *covering* (and therefore again, decidable separation). Let us mention some important features of this work.

A first point is that the case of a *finite class* is important by itself. Foremost, it is a crucial step for the main result on the star-free closure of classes of group languages (this is due to the fact that a language in the star-free closure of a class is built using a finite number of languages of the class). Second, it provides a new proof that covering is decidable for the original class of star-free languages (this is shown in [37] or can be derived from [15, 2]). This new proof is simpler and generic. While the original underlying technique goes back to Wilke [51], the proof has been simplified at several levels. The main simplification is obtained thanks to an abstract framework, introduced in [40]. It is based on the central notion of rating map, which is meant to measure the quality of a separator. For the framework to be relevant, we actually need to generalize separation to multiple input languages, which leads to the covering problem. Another key difference is that existing proofs (specific to star-free languages) involve abstracting words by new letters at some point, which requires the working alphabet to be a parameter of the induction. Here, we cannot use this approach as the classes we build with star-free closure are less robust in general. We work with a fixed alphabet, which also makes the proof simpler. In fact, several proofs should look similar to the reader. This is not surprising, since in order to establish membership or covering, we have to build languages from the classes we are interested in.

**Applications.** Finally, let us present important applications of the result about covering for classes made of group languages. First, one can look at the input class containing all group languages. Straubing [45] described an algebraic counterpart of the star-free closure of this class, whose membership was then shown to be decidable by Rhodes and Karnofsky [18]. Altogether, this implies that membership is decidable for the star-free closure of group languages, as noted by Margolis and Pin [23]. Here, we are able to generalize this result to separation and covering, as separation is known to be decidable for the class of all group languages [3, 34].
Another application is the class of languages definable by first-order logic with modular predicates FO(⟨·, MOD⟩). This class is known to have decidable membership [4]. It is the star-free closure of the class consisting of the languages counting the length of words modulo some number. Since this input class is easily shown to have decidable separation (see e.g. [38]), our main theorem applies.

The third application concerns first-order logic endowed with predicates counting the number of occurrences of a letter before a position, modulo some integer. Indeed, the class of languages definable in this logic is exactly the star-free closure of the class of languages recognized by Abelian groups (this follows from a generic correspondence theorem between star-free closure of a class and variants of first-order logic [38, 25], as well as from the description of languages recognized by Abelian groups [12]). Again, our main theorem applies, since the class of Abelian groups is known to have decidable separation: this follows from [8] and [2] (see also [34]).

**Organization.** We set up the notation and recall the background in Section 2. We introduce the star-free closure operator and present some of its properties in Section 3. We also introduce classes of group languages, for which this operator produces relevant classes. We define prefix codes of bounded synchronization delay in Section 4 and the associated operator *SD*, which allows Kleene star to be applied only to these languages. We also show that this new operator can be simulated by the star-free closure. We then develop in Section 5 the material needed to establish, for a class $C$ with mild properties, a common algebraic characterization of $SF(C)$ and $SD(C)$ (thus proving the missing inclusion $SF(C) \subseteq SD(C)$). As explained above, this characterization is decidable as soon as separation is decidable for the underlying class $C$. We establish the correspondences of star-free closure with first-order logic in Section 6 and with temporal logic in Section 7. Finally, we consider the covering problem. In Section 8, we recall the framework of rating maps, which is convenient for handling covering. We then prove that the star-free closure operator outputs a class whose covering is decidable in two cases: in Section 9, when the input class is finite and in Section 10, when it is made of group languages (satisfying mild additional properties).

**Related paper.** This paper completes results from [35] and extend them.

## 2 Preliminaries

In this section, we introduce the terminology used in the paper. We also present the membership, separation and covering problems, as well as key mathematical tools designed to handle them.

### 2.1 Classes of regular languages

For the whole paper, we fix a finite alphabet $A$. We denote by $A^*$ the set of all *finite* words over $A$, including the empty word $\varepsilon$. We let $A^+ = A^* \setminus \{\varepsilon\}$. For $u, v \in A^*$, we write $uv$ the word obtained by concatenating $u$ and $v$. Moreover, for every $w \in A^*$, we write $|w| \in \mathbb{N}$ for its length. We shall also consider *positions*. A word $w = a_1 \cdots a_{|w|} \in A^*$ is viewed as an *ordered set* $\text{Pos}(w) = \{0, 1, \dots, |w|, |w| + 1\}$ of $|w| + 2$ *positions*. A position $i$ such that $1 \le i \le |w|$ carries label $a_i \in A$. We write $\text{Pos}_c(w) = \{1, \dots, |w|\}$ for this set of labeled positions. On the other hand, positions 0 and $|w| + 1$ are *artificial leftmost* and *rightmost* positions, which carry *no label*. Finally, given a word $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^*$ (i.e., the *infix* obtained by keeping the letters carried by the positions that are *strictly* between $i$ and $j$). Note that $w(0, |w| + 1) = w$.

A *language* is a subset of $A^*$. It is standard to extend concatenation to languages: given $K, L \subseteq A^*$, we write $KL = \{uv \mid u \in K \text{ and } v \in L\}$. Finally, we use the Kleene star: if $K \subseteq A^*$, then $K^+$ denotes the union of all languages $K^n$ for $n \ge 1$ and $K^*$ denotes the language $K^+ \cup \{\varepsilon\}$.

**Classes.** A class of languages $C$ is a set of languages. Such a class $C$ is a *lattice* when $\emptyset \in C$, $A^* \in C$ and $C$ is closed under union and intersection: for every $K, L \in C$, we have $K \cup L \in C$ and $K \cap L \in C$.
A Boolean algebra is a lattice which is closed under complement: if $K \in \mathbb{C}$, then $A^* \setminus K \in \mathbb{C}$. Finally, a class $\mathcal{C}$ is quotient-closed if for every $L \in \mathbb{C}$ and $u \in A^*$, the following properties hold:

$u^{-1}L \stackrel{\text{def}}{=} \{w \in A^* | uw \in L\}$ and $Lu^{-1} \stackrel{\text{def}}{=} \{w \in A^* | wu \in L\}$ both belong to $\mathcal{C}$.

A *prevariety* is a quotient-closed Boolean algebra containing only *regular languages*. Regular languages are those which can be equivalently defined by nondeterministic finite automata, finite monoids or monadic second-order logic. We work with the definition by monoids, which we recall.

**Finite monoids and regular languages.** A semigroup is a set $S$ endowed with an associative multiplication $(s, t) \mapsto s \cdot t$ (also denoted by $st$). A monoid is a semigroup $M$ whose multiplication has an identity element $1_M$, i.e., such that $1_M \cdot s = s \cdot 1_M = s$ for every $s \in M$.

An *idempotent* of a semigroup $S$ is an element $e \in S$ such that $ee = e$. We let $E(S) \subseteq S$ be the set of all idempotents in $S$. It is folklore that for every *finite* semigroup $S$, there exists a natural number $\omega(S)$ (denoted by $\omega$ when $S$ is understood) such that for every $s \in S$, the element $s^\omega$ is idempotent.

Clearly, $A^*$ is a monoid whose multiplication is concatenation (the identity element is $\varepsilon$). Thus, we may consider morphisms $\alpha : A^* \to M$ where $M$ is an arbitrary monoid. That is, $\alpha : A^* \to M$ is a map satisfying $\alpha(\varepsilon) = 1_M$ and $\alpha(uv) = \alpha(u)\alpha(v)$ for all $u, v \in A^*$. Given such a morphism and some language $L \subseteq A^*$, we say that $L$ is *recognized* by $\alpha$ when there exists a subset $F$ of $M$ such that $L = \alpha^{-1}(F)$. It is standard and well known that the regular languages are those which can be recognized by a morphism into a *finite* monoid.

**Syntactic morphism.** Every language $L$ is recognized by a canonical morphism, which we recall. One associates to $L$ an equivalence relation $\equiv_L$ over $A^*$: the *syntactic congruence of L*.

Given $u, v \in A^*$, we let: $u \equiv_L v$ if and only if $xuy \in L \Leftrightarrow xvy \in L$ for every $x, y \in A^*$.

It can be verified that "$\equiv_L$" is indeed a congruence on $A^*$: it is reflexive, symmetric and transitive, and for all $u, u', v, v' \in A^*$ such that $u \equiv_L v$ and $u' \equiv_L v'$, we have $uu' \equiv_L vv'$. Thus, the set of equivalence classes $M_L = A^*/\equiv_L$ is a monoid. It is called the *syntactic monoid of L*. Moreover, the map $\alpha_L : A^* \to M_L$ sending every word to its equivalence class is a morphism recognizing $L$, called the *syntactic morphism of L*. Myhill-Nerode's theorem states that $L$ is regular if and only if $M_L$ is finite (i.e., $\equiv_L$ has finite index). In this case, one can compute the syntactic morphism $\alpha_L : A^* \to M_L$ from any representation of $L$ (such as a finite automaton or an arbitrary monoid morphism).

## 2.2 Decision problems

These problems depend on an arbitrary class $\mathcal{C}$. We use them as mathematical tools for analyzing $\mathcal{C}$. Indeed, obtaining an algorithm for one of these three problems requires a solid understanding of $\mathcal{C}$.

The $\mathcal{C}$-membership problem is the simplest one. It takes as input a single regular language $L$ and asks whether $L \in \mathcal{C}$. The second problem, $\mathcal{C}$-separation, is more general. Given three languages $K, L_1, L_2$, we say that $K$ separates $L_1$ from $L_2$ if we have $L_1 \subseteq K$ and $L_2 \cap K = \emptyset$. Given a class of languages $\mathcal{C}$, we say that $L_1$ is $\mathcal{C}$-separable from $L_2$ if some language in $\mathcal{C}$ separates $L_1$ from $L_2$. Observe that when $\mathcal{C}$ is not closed under complement, the definition is not symmetrical: it is possible for $L_1$ to be $\mathcal{C}$-separable from $L_2$ while $L_2$ is not $\mathcal{C}$-separable from $L_1$. The separation problem associated to a given class $\mathcal{C}$, also called $\mathcal{C}$-separation problem, takes two regular languages $L_1$ and $L_2$ as input and asks whether $L_1$ is $\mathcal{C}$-separable from $L_2$.

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

We do not consider separation directly. Instead, we work with a third, even more general problem: $\mathcal{C}$-covering. It was introduced in [40] and takes as input a single regular language $L_1$ and a finite set of regular languages $L_2$. It asks whether there exists a "$\mathcal{C}$-cover of $L_1$ which is separating for $L_2$".
Given a language $L$, a *cover of* $L$ is a *finite set* of languages $\mathbf{K}$ such that $L \subseteq \bigcup_{K \in \mathbf{K}} K$. A *cover* $\mathbf{K}$ is a $\mathcal{C}$-cover if all languages $K \in \mathbf{K}$ belong to $\mathcal{C}$. Moreover, given two finite sets of languages $\mathbf{K}$ and $\mathbf{L}$, we say that $\mathbf{K}$ is *separating* for $\mathbf{L}$ if for every $K \in \mathbf{K}$, there exists $L \in \mathbf{L}$ such that $K \cap L = \emptyset$. Finally, given a language $L_1$ and a finite set of languages $L_2$, we say that the pair $(L_1, L_2)$ is $\mathcal{C}$-coverable if there exists a $\mathcal{C}$-cover of $L_1$ which is separating for $L_2$.

The $\mathcal{C}$-covering problem takes as input a regular language $L_1$ and a finite set of regular languages $L_2$, it asks whether the pair $(L_1, L_2)$ $\mathcal{C}$-coverable. It is straightforward to prove that covering generalizes separation if the class $\mathcal{C}$ is a lattice, as stated in the lemma (see [40, Theorem 3.5] for the proof).

**LEMMA 2.2.** Let $\mathcal{C}$ be a lattice and $L_1, L_2$ be two languages. Then $L_1$ is $\mathcal{C}$-separable from $L_2$ if and only if $(L_1, \{L_2\})$ is $\mathcal{C}$-coverable.

## 2.3 $\mathcal{C}$-morphisms

We turn to a key mathematical tool. Consider a prevariety $\mathcal{C}$. A $\mathcal{C}$-morphism is a surjective morphism $\eta : A^* \to N$ into a finite monoid $N$ such that every language recognized by $\eta$ belongs to $\mathcal{C}$. This notion is connected to the membership problem via the following simple, yet crucial proposition. A proof can be found in [32, Proposition 2.12] and provided in Appendix A.

**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.

In view of Proposition 2.3, getting an algorithm for $\mathcal{C}$-membership boils down to finding a procedure to decide whether an input morphism $\alpha : A^* \to M$ is a $\mathcal{C}$-morphism.

We use $\mathcal{C}$-morphisms as mathematical tools in proof arguments. They are convenient when manipulating arbitrary classes. We present some properties we need in this context. First, we have the following simple corollary of Proposition 2.3 (see [32, Proposition 2.13] and Appendix A).

**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$.

Finally, we consider the special case when $\mathcal{C}$ is a *finite* prevariety (i.e., $\mathcal{C}$ contains finitely many languages). In this case, Proposition 2.4 yields a $\mathcal{C}$-morphism recognizing all languages in $\mathcal{C}$. The following lemma implies that it is unique, up to renaming (see [32, Lemma 2.16] and Appendix A).

**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$.

By Lemma 2.5, if $\mathcal{C}$ is a finite prevariety and $\alpha : A^* \to M$ and $\eta : A^* \to N$ are two $\mathcal{C}$-morphisms which both recognize all languages in $\mathcal{C}$, there are morphisms $\gamma : M \to N$ and $\beta : N \to M$ such that $\eta = \gamma \circ \alpha$ and $\alpha = \beta \circ \eta$. This yields $\beta \circ \gamma \circ \alpha = \alpha$. Since $\alpha$ is surjective, $\beta \circ \gamma : M \to M$ is the identity. Hence, $\alpha$ and $\eta$ are the same object up to renaming. We call it the *canonical $\mathcal{C}$-morphism* and denote it by $\eta_{\mathcal{C}} : A^* \to N_{\mathcal{C}}$. Do note that this object is only defined when $\mathcal{C}$ is a *finite prevariety*.

# 3 Star-free closure

In this section, we introduce the classes investigated in the paper. Each of them is built from a simpler input class using a single operator: the *star-free closure*, which we first define. Then, we present classes that we use as key inputs for this operator: those containing only *group languages*.

## 3.1 Definition

Consider a class $\mathcal{C}$. The *star-free closure* of $\mathcal{C}$, denoted by $SF(\mathcal{C})$, is the least class of languages containing $\mathcal{C}$ and all singletons $\{a\}$ for $a \in A$, and which is closed under union, complement and concatenation (that is, if $K, L \in SF(\mathcal{C})$, then $K \cup L, A^* \setminus K$ and $KL$ belong to $SF(\mathcal{C})$ as well).
**REMARK 3.1.** *Star-free closure is the generalization of a prominent single class: the class SF of star-free languages. It contains exactly the languages that can be defined by a star-free expression, i.e., a regular expression that cannot use the Kleene star but can use complement instead. One can check that SF is exactly the star-free closure of the class {$\emptyset, A^*$}, i.e., $SF = SF(\{\emptyset, A^*\})$. Naturally, SF is also the star-free closure of itself. Therefore, $SF(C) = SF$ for every class C included in SF and containing {$\emptyset, A^*$}. It follows that investigating the star-free closure is worthwhile only when applied to a class which is **not** included in SF. As we explain below, typical such classes are made of group languages.*

In practice, we only apply star-free closure to input classes $C$ that are prevarieties. In this case, $SF(C)$ is a prevariety as well, as stated in the following proposition (see Appendix B for a proof).

**PROPOSITION 3.2.** *If $C$ is a prevariety, then $SF(C)$ is a prevariety closed under concatenation.*

We complete the presentation with a characteristic property of star-free closure (for input classes that are prevarieties). We present it as a property of the $SF(C)$-morphisms, proved in Appendix B.

**PROPOSITION 3.3.** Let $C$ be a prevariety and let $\alpha : A^* \to M$ be an $SF(C)$-morphism. There exists a $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}$.

## 3.2 Group languages

We now present a central kind of class. As we explained in the introduction, all classes investigated in the paper are built from basic ones using the star-free closure operator. Here, we introduce the basic classes used in this construction: the *classes of group languages*.

A group is a monoid $G$ such that every element $g \in G$ has an inverse $g^{-1} \in G$, i.e., $gg^{-1} = g^{-1}g = 1_G$. A language $L$ is a *group language* if it is recognized by a morphism $\alpha : A^* \to G$ into a *finite group* $G$ (i.e., there exists $F \subseteq G$ such that $L = \alpha^{-1}(F)$). We write `GR` for the class of all group languages. One can verify that `GR` is a prevariety.

**REMARK 3.4.** *No language theoretic definition of GR is known. There is however a definition based on automata: the group languages are those recognized by a permutation automaton [50] (i.e., which is simultaneously deterministic, co-deterministic and complete).*

A class of group languages is a class consisting of group languages only, i.e., a subclass of GR. The results of this paper apply to arbitrary *prevarieties of group languages*.

While our results apply in a generic way to all prevarieties of group languages, there are four main classes of this kind that we shall use for providing examples. One of them is `GR` itself. Let us present the other three. First, we write `ST = {$\emptyset, A^*$}`, which is clearly a prevariety of group languages (the notation from the fact that this class is the base level of the *Straubing-Thérien hierarchy* [44, 48]). While trivial, we shall see that this class has important applications. Moreover, we look at the class `MOD` of *modulo languages*. For every $q, r \in \mathbb{N}$ with $r < q$, we write $L_{q,r} = \{w \in A^* \mid |w| \equiv r \mod q\}$. The class `MOD` consists of all *finite unions* of languages $L_{q,r}$. One can check that `MOD` is a prevariety of group languages. Finally, we shall consider the class `AMT` of *alphabet modulo testable languages*. For every $a \in A$ and every $w \in A^*$, we write $|w|_a \in \mathbb{N}$ for the number of occurrences of the letter $a$ inside the word $w$. For all $q, r \in \mathbb{N}$ with $r < q$ and all $a \in A$, let $L_{q,r}^a = \{w \in A^* \mid |w|_a \equiv r \mod q\}$. We define `AMT` as the least class consisting of all languages $L_{q,r}^a$ and closed under union and intersection. It is again straightforward to check that `AMT` is a prevariety of group languages.

We do not investigate classes of group languages themselves in the paper: they are only input classes for our operator. We shall use `ST`, `MOD`, `AMT` and `GR` in order to illustrate our results. In this context, it will be important that these classes have decidable *separation*. The techniques involved for proving this are independent from those of the paper. On one hand, the decidability of `ST`-separation is immediate (two languages are `ST`-separable if and only if one of them is empty). On
the other hand, the decidability of GR-separation is equivalent to a difficult algebraic question [16], which remained open for several years before it was solved by Ash [3]. Recent automata-based proofs that separation is decidable for MOD, AMT and GR are available in [34].

We conclude this section with a standard result, which states a simple property of the $\mathcal{G}$-morphisms when $\mathcal{G}$ is a group prevariety. It follows from Lemma 2.5 and is proved in Appendix B.

**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.

# 4 Bounded synchronization delay

We now present an alternate definition of star-free closure. More precisely, we introduce a second operator $\mathcal{C} \mapsto \text{SD}(\mathcal{C})$ whose definition is independent from that of star-free closure. We then prove that $\text{SD}(\mathcal{C}) = \text{SF}(\mathcal{C})$ if $\mathcal{C}$ is a prevariety. This definition is less prominent than the primary one and the logical characterizations we will present later. Nevertheless, it plays a crucial role in the paper, as it enables us to bypass the complement operation on languages, which is notoriously challenging to handle. Whenever we have to construct languages in $\text{SF}(\mathcal{C})$ in proof arguments, we actually build them as languages of $\text{SD}(\mathcal{C})$. For example, this is how we obtain the algebraic characterization of $\text{SF}(\mathcal{C})$ (in fact, this argument is intertwined with the proof of the inclusion $\text{SF}(\mathcal{C}) \subseteq \text{SD}(\mathcal{C})$ that we present in this section).

This second definition was discovered by Schützenberger [42]. He defined a single class $\text{SD}$ (in our terminology, this is the class $\text{SD}(\text{ST})$) and he proved that it coincides with the class $\text{SF}$ of star-free languages (see the work of Diekert and Kufleitner [9] for a recent proof). This is a surprising result since $\text{SD}$ seems antithetic to $\text{SF}$ at first glance. Its definition is based on the operations available in classical regular expressions: union, concatenation and Kleene star. However, these operations are restricted to languages satisfying specific semantic conditions. The main restriction concerns the Kleene star, which can only be applied to prefix codes of bounded synchronization delay (a notion from code theory, recalled below). Here, we extend the definition of $\text{SD}$ as an operator $\mathcal{C} \mapsto \text{SD}(\mathcal{C})$.

We first present preliminary notions from code theory that we shall need for the definition. Then, we define $\mathcal{C} \mapsto \text{SD}(\mathcal{C})$ properly and state the correspondence with star-free closure.

## 4.1 Prefix codes of bounded synchronization delay

The objects introduced in this section are based on a notion taken from code theory: prefix codes. We briefly present them here and prove a few basic properties that we shall need. For a detailed presentation of code theory, we refer the reader to the book of Berstel, Perrin and Reutenauer [5].

**Prefix codes.** A language $K \subseteq A^*$ is a prefix code when $\epsilon \notin K$ (i.e., $K \subseteq A^+$) and $K \cap KA^+ = \emptyset$ (i.e., no word in $K$ admits a strict prefix which is also a word in $K$).

*Example 4.1.* If $A = \{a, b\}$, then the language $A$ is a prefix code. Any singleton language $\{u\}$ with $u \neq \epsilon$ is also a prefix code. Finally, $a^*b$ is a prefix code as well. On the other hand, $L = \{a, aa\}$ is not a prefix code, since $aa \in L \cap LA^+$.

We now present the key property of such languages: the left-to-right parsing of concatenations of words from the prefix code is unambiguous. It is well-known and proved in Appendix C.

**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$.

The second assertion in Fact 4.2 implies that when $K$ is a prefix code, every word $w \in K^*$ admits a unique decomposition witnessing this membership. This property is exactly the definition of a code, which is therefore a notion more general than that of prefix code.
**Bounded synchronization delay.** We turn to a more restrictive notion. Consider an integer $d \ge 1$. We say that a prefix code $K \subseteq A^+$ has synchronization delay $d$ when the following property holds:

$$ \text{for every } u, v, w \in A^*, \quad uvw \in K^+ \text{ and } v \in K^d \Rightarrow uv \in K^+. \quad (1) $$

Furthermore, we say that a prefix code $K \subseteq A^+$ has bounded synchronization delay when there exists some $d \ge 1$ such that $K$ has synchronization delay $d$.

**REMARK 4.3.** A prefix code with synchronization delay $d$ has synchronization delay $d'$ for all $d' \ge d$.

**REMARK 4.4.** Let $K$ be a prefix code with synchronization delay $d$. If $u, v, w \in A^*$ satisfy $uvw \in K^+$ and $v \in K^d$, we have $w \in K^*$. Indeed, Condition (1) states that $uv \in K^+$. This means that there are $u_1, \dots, u_n, v_1, \dots, v_m$ in $K$ such that $uvw = u_1 \cdots u_n$ and $uv = v_1 \cdots v_m$. From Fact 4.2, we deduce that $m \le n$ and $w = u_{m+1} \cdots u_n$, which belongs to $K^*$. This explains the terminology: any infix $v$ in $K^d$ of a word $uvw \in K^+$ determines a decomposition $uv \cdot w$ of $uvw$ whose factors ($uv$ and $w$) both belong to $K^*$.

*Example 4.5.* Assume that $A = \{a, b\}$.

* Clearly, for any $B \subseteq A$, the language $B$ is a prefix code of synchronization delay 1.

* It is also immediate that any language $L \subseteq a^*b$ is a prefix code of synchronization delay 1. Indeed, if $uvw \in L^*$ and $v \in L$, then $v$ ends with a “b”, whence $uv \in L^*$.

* Let $K = \{ab, aab\}$ and $H = \{ab\}$. It follows from the previous item that $K$ is a prefix code of synchronization delay 1. Fact 4.7 below entails that $(aab)^*ab$ is a prefix code of synchronization delay 2. However, it does not have synchronization delay 1. Indeed, consider the decomposition $aabab = a \cdot ab \cdot ab$. We have $aabab, ab \in ((aab)^*(ab))^1$ but $aab \notin ((aab)^*ab)^+$.

* Finally, $\{aa\}$ (which is a prefix code) does not have bounded synchronization delay. Indeed, given $d \ge 1$, we have $a(aa)^d a \in (aa)^+$ and $(aa)^d \in \{aa\}^d$ but $a(aa)^d \notin (aa)^*$.

We complete the definition with two properties of prefix codes of bounded synchronization delay. They are standard and proved in Appendix C. First, every language included in a such a code retains the property of being a prefix code of bounded synchronization delay.

**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$.

Finally, we show how to build a prefix code of bounded synchronization delay from another one.

**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$.

## 4.2 Definition

We now define the operator $\mathcal{C} \mapsto SD(\mathcal{C})$. The definition involves two additional notions. First, we consider disjoint union. Two languages $K, L \subseteq A^*$ are disjoint if $K \cap L = \emptyset$. In this case, we write $K \uplus L$ for $K \cup L$ in order to emphasize disjointedness. Additionally, we consider unambiguous concatenation. Given two languages $K, L \subseteq A^*$, their concatenation $KL$ is unambiguous when every word $w \in KL$ admits a unique decomposition witnessing this membership: if $u, u' \in K, v, v' \in L$ and $uv = u'v'$, then $u = u'$ and $v = v'$.

Let $\mathcal{C}$ be some class of languages. We write $SD(\mathcal{C})$ for the least class containing $\emptyset$ and $\{a\}$ for every $a \in A$, and which is closed under the following properties:

* **Intersection with $\mathcal{C}$**: if $K \in SD(\mathcal{C})$ and $L \in \mathcal{C}$, then $K \cap L \in SD(\mathcal{C})$.

* **Disjoint union**: if $K, L \in SD(\mathcal{C})$ are disjoint then $K \uplus L \in SD(\mathcal{C})$.

* **Unambiguous concatenation**: if $K, L \in SD(\mathcal{C})$ and $KL$ is unambiguous, then $KL \in SD(\mathcal{C})$.

* **Kleene star for prefix codes of bounded synchronization delay**: if $K \in SD(\mathcal{C})$ is a prefix code of bounded synchronization delay, then $K^* \in SD(\mathcal{C})$.
An important input class is the trivial prevariety $ST = \{\emptyset, A^*\}$. In this case, $SD(ST)$ is the original class $SD$ of Schützenberger [42]. His definition is slightly different, as it does not require unions to be disjoint, nor concatenations to be unambiguous. Yet, the two definitions are equivalent.

**Example 4.8.** Let $A = \{a, b\}$. We show that $(ab)^* \in SD(ST)$ and $(aa + bb)^* \in SD(MOD)$.

* Clearly, $\{a\}, \{b\} \in SD(ST)$ which yields $\{ab\} \in SD(ST)$ by closure under unambiguous concatenation. Since $\{ab\}$ is a has synchronization delay one, we get $(ab)^* \in SD(ST)$.

* Since $\{a\}$ and $\{b\}$ have synchronization delay one, $a^*, b^* \in SD(MOD)$. Moreover, since $(AA)^* \in MOD$, we get $(aa)^*, (bb)^* \in SD(MOD)$ by closure under intersection with MOD. We then use unambiguous concatenation to get $(aa)^+(bb)^+ = aa(aa)^*bb(bb)^* \in SD(MOD)$. This is a prefix code of bounded synchronization delay. Hence, $((aa)^+(bb)^+)^* \in SD(MOD)$. Using unambiguous concatenation again, this yields $(bb)^*((aa)^+(bb)^+)^*(aa)^* \in SD(MOD)$. One can now check that $(aa + bb)^* = (bb)^*((aa)^+(bb)^+)^*(aa)^* \in SD(MOD)$.

**REMARK 4.9.** We do not explicitly require in the definition that $SD(C)$ contains $C$. Yet, this is a simple consequence of the definition. Clearly, $A^* \in SD(C)$ since $A \in SD(C)$ is a prefix code of bounded synchronization delay. Hence, $L = A^* \cap L \in SD(C)$ for every $L \in C$.

On the other hand, it is crucial to allow intersection with languages in $C$. If we only require the inclusion $C \subseteq SD(C)$ in the definition, we would end up with a weaker operator (which, therefore, does not correspond to star-free closure in general). For example, consider the class MOD of modulo languages. Assume that $A = \{a, b\}$. As observed in Example 4.8, $(aa)^* \in SD(MOD)$. On the other hand, one can check that $(aa)^*$ cannot be built from the languages of MOD using only union, concatenation and Kleene star for prefix codes of bounded synchronization delay.

It is not immediate that the classes $SD(C)$ have robust closure properties, even when this is the case for $C$. Actually, it is not even clear whether $SD(C)$ is a lattice, since closure under intersection is not required in the definition, and closure under union is restricted. However, $SD(C)$ does have robust properties: if $C$ is a prevariety, then $SD(C)$ is a prevariety closed under concatenation. This follows from Proposition 3.2, which states that $SF(C)$ is a prevariety closed under concatenation, together with the following theorem, which states the correspondence with star-free closure.

**THEOREM 4.10.** Let $C$ be a prevariety. Then, $SD(C) = SF(C)$.

The difficult direction in Theorem 4.10 is the inclusion $SF(C) \subseteq SD(C)$. We rely on an indirect approach based on the generic algebraic characterization of star-free closure, which we use as an intermediary result to prove this implication. In fact, the proof of the difficult inclusion is intertwined with the one of the characterization itself. Hence, we postpone it to the next section. On the other hand, we prove the easier inclusion $SD(C) \subseteq SF(C)$ now.

**INCLUSION SD(C) ⊆ SF(C) IN THEOREM 4.10.** We fix a prevariety $C$ and prove $SD(C) \subseteq SF(C)$. This amounts to proving that $SF(C)$ satisfies all properties in the definition of $SD(C)$. In all cases but one, this is immediate by definition of $SF(C)$. Indeed, we have $\emptyset \in SF(C)$ and $\{a\} \in SF(C)$ for every $a \in A$. Moreover, $SF(C)$ is closed under union, intersection and concatenation by definition (this includes intersection with languages of $C$ since $C \subseteq SF(C)$). It remains to show that $SF(C)$ is closed under Kleene star applied to a prefix code of bounded synchronization delay.

We let $K \in SF(C)$ be such a prefix code, and we let $d \ge 1$ be its synchronization delay. We have to show that $K^* \in SF(C)$. Consider the following languages:

$$H = \left( A^* K^d \cap \left( A^* \setminus \left(A^* K^{d+1} \cup \bigcup_{0 \le h \le d} K^h\right) \right) \right) A^* \quad \text{and} \quad G = \left( \bigcup_{0 \le h \le d-1} K^h \right) \cup \left( A^* K^d \cap (A^* \setminus H) \right).$$
Clearly, $H \in SF(C)$ since both $K$ and $A^*$ belong to $SF(C)$, which is closed under Boolean operations and concatenation. Therefore $G \in SF(C)$ as well. We show that $K^* = G$, which will entail that $K^* \in SF(C)$, concluding the proof of $SD(C) \subseteq SF(C)$ in Theorem 4.10.

We first show that $K^* \cap H = \emptyset$. Note that this is the only part of the proof where we use the hypothesis that $K$ has synchronization delay $d$.

**FACT 4.11.** We have $K^* \subseteq A^* \setminus H$.

**PROOF.** We have to show that $K^* \cap H = \emptyset$. Since $K^* \subseteq A^*K^{d+1} \cup \bigcup_{0 \le h \le d} K^h$, we have,

$$A^* \setminus (A^*K^{d+1} \cup \bigcup_{0 \le h \le d} K^h) \subseteq A^* \setminus K^*.$$

By definition of $H$, this yields $H \subseteq (A^*K^d \cap (A^* \setminus K^*))A^*$. Therefore, it suffices to show that $K^* \cap (A^*K^d \cap (A^* \setminus K^*))A^* = \emptyset$, which follows immediately from the hypothesis that $K$ has synchronization delay $d$. $\square$

It remains to show that $K^* = G$. We start with the left to right inclusion. Recall that $G = (\bigcup_{0 \le h \le d-1} K^h) \cup (A^*K^d \cap (A^* \setminus H))$. Consider $x \in K^*$. If $x \in K^h$ for $h \le d-1$, it is immediate that $x \in G$. Otherwise, we have $x \in A^*K^d$ and since $x \in K^*$, we know that $x \in A^* \setminus H$ by Fact 4.11. This implies that $x \in A^*K^d \cap (A^* \setminus H) \subseteq G$, finishing the proof for this inclusion.

For the right to left inclusion, consider $x \in G$. We show that $x \in K^*$. If $x \in \bigcup_{0 \le h \le d-1} K^h$, this is immediate. Otherwise, $x \in A^*K^d \cap (A^* \setminus H)$. We proceed by induction on the length of $x$. By hypothesis, $x \in A^*K^d$ and $x \notin H$. By definition of $H$, this implies that,

$$x \in A^*K^{d+1} \cup \bigcup_{0 \le h \le d} K^h.$$

If $x \in \bigcup_{0 \le h \le d} K^h$, it is immediate that $x \in K^*$, which finishes the proof. Otherwise, $x \in A^*K^{d+1}$ which means that $x = x' y$ with $x' \in A^*K^d$ and $y \in K$. Since $\epsilon \notin K$ (as $K$ is a prefix code), we have $y \ne \epsilon$ which implies that $|x'| < |x|$. Moreover, since $x \in A^* \setminus H$ and $x'$ is a prefix of $x$, the definition of $H$ implies that $x' \in A^* \setminus H$ as well. Altogether, we have $x' \in A^*K^d \cap (A^* \setminus H)$ and $|x'| < |x|$. Therefore by induction, $x' \in K^*$. Finally, since $y \in K$, we get $x = x' y \in K^*K \subseteq K^*$, as desired. $\square$

**REMARK 4.12.** In the above proof, we used Fact 4.11 only to establish that $K^* \subseteq G$. This inclusion relies on the assumption that $K$ has bounded synchronization delay (clearly, relying on this hypothesis to show that $K^*$ belongs to $SF(C)$ is mandatory). On the other hand, the inclusion $G \subseteq K^*$ is independent from this hypothesis.

# 5 Algebraic characterization of $SF(C)$

We present a generic algebraic characterization of the classes $SF(C)$ built with star-free closure from a prevariety $C$. It yields an effective reduction from $SF(C)$-membership to $C$-separation (here, we mean reduction in the Turing sense: we get a generic algorithm for $SF(C)$-membership that uses an oracle for $C$-separation). Moreover, we use this characterization to prove the missing inclusion $SF(C) \subseteq SD(C)$ in Theorem 4.10.

More precisely, we characterize the languages in $SF(C)$ by a property of their syntactic morphisms. It generalizes Schützenberger's characterization of star-free languages as those whose syntactic monoid is *aperiodic* [41]. First, with every class $C$ and every morphism $\alpha: A^* \to M$, we associate a relation on $M$: the $C$-pair relation for $\alpha$ (it was defined in [33]). Then, we use this relation to identify special subsets of $M$, which happen to be monoids when $C$ is a prevariety: the $C$-orbits of $\alpha$. Finally, the characterization states that for every prevariety $C$, a language belongs to $SF(C)$ if and only if all $C$-orbits of its syntactic morphism are aperiodic monoids. Let us now define $C$-pairs.
## 5.1 C-Pairs

Consider a class $\mathcal{C}$ and a morphism $\alpha : A^* \to M$ into a finite monoid. We define the $\mathcal{C}$-pair relation for $\alpha$ on $M$ as follows. Let $(s, t) \in M^2$. We say that,

$$ (s, t) \text{ is a } \mathcal{C}\text{-pair (for } \alpha \text{) if and only if } \alpha^{-1}(s) \text{ is not } \mathcal{C}\text{-separable from } \alpha^{-1}(t). \quad (2) $$

**REMARK 5.1.** While we often make this implicit, being a $\mathcal{C}$-pair depends on $\alpha$.

By definition, the set of $\mathcal{C}$-pairs for $\alpha$ is finite: it is a subset of $M^2$. Moreover, having a $\mathcal{C}$-separation algorithm in hand is clearly enough to compute all $\mathcal{C}$-pairs associated to an input morphism $\alpha$. We complete the definition with some properties of $\mathcal{C}$-pairs. A simple and useful one is that the $\mathcal{C}$-pair relation is reflexive when the morphism $\alpha$ is surjective (which is the case in practice). Moreover, it is symmetric if $\mathcal{C}$ is closed under complement (this is the case for all classes considered in the paper). On the other hand, the $\mathcal{C}$-pair relation is not transitive in general, as the following example shows.

**Example 5.2.** Let $A = \{a, b\}$ and $\mathcal{C} = \text{AT}$ be the least Boolean algebra containing $A^*aA^*$ and $A^*bA^*$. Let $M$ be the monoid $\{1, a, b, 0\}$ where 1 acts as an identity element, 0 as an absorbing element, and the rest of the multiplication is given by $aa = ab = ba = bb = 0$. Let $\alpha : A^* \to M$ be the morphism defined by $\alpha(a) = a$ and $\alpha(b) = b$. We have $\alpha^{-1}(a) = \{a\}$. Therefore, one can verify that any language of $\text{AT}$ containing $\alpha^{-1}(a)$ also contains $a^+$, and therefore intersects $\alpha^{-1}(0)$ (which is the set of words of length at least 2). Hence, $(a, 0)$ is an $\text{AT}$-pair. Likewise, $(0, b)$ is an $\text{AT}$-pair. However, $(a, b)$ is not an $\text{AT}$-pair, since the language $a^+ \in \text{AT}$ separates $\alpha^{-1}(a) = \{a\}$ from $\alpha^{-1}(b) = \{b\}$. This example shows that the $\mathcal{C}$-pair relation is not transitive in general.

We state a useful characterization of $\mathcal{C}$-pairs via $\mathcal{C}$-morphisms when $\mathcal{C}$ is a prevariety, which, again, is the only case that we consider here (see [32, Lemma 5.11] or Appendix D for a proof).

**LEMMA 5.3.** Let $\mathcal{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 $\mathcal{C}$-morphism $\eta : A^* \to N$ and every $\mathcal{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 $\mathcal{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 $\mathcal{C}$-pair for $\alpha$.

Finally, if $\mathcal{C}$ is a prevariety, the $\mathcal{C}$-pair relation is compatible with multiplication (see Appendix D).

**LEMMA 5.4.** Let $\mathcal{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 $\mathcal{C}$-pairs, then $(s_1s_2, t_1t_2)$ is a $\mathcal{C}$-pair as well.

## 5.2 $\mathcal{C}$-orbits and $\mathcal{C}$-kernels

Consider a class $\mathcal{C}$ and a morphism $\alpha : A^* \to M$ into a finite monoid. For every idempotent $e \in E(M)$ we define the $\mathcal{C}$-orbit of $e$ (for $\alpha$) as the set consisting of all elements $ese \in M$ such that $(e, s) \in \mathcal{C}$-pair (for $\alpha$). More generally, the $\mathcal{C}$-orbits for $\alpha$ are all the subsets of $M$ which are the $\mathcal{C}$-orbit of some idempotent $e \in E(M)$. When $\mathcal{C}$ is a prevariety, we have the following simple corollary of Lemma 5.4. See Appendix D for a proof.

**LEMMA 5.5.** Let $\mathcal{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 $\mathcal{C}$-orbit of $e$ for $\alpha$ is a subsemigroup of $M$. Moreover, it is a monoid whose neutral element is $e$.

By definition, the $\mathcal{C}$-pairs associated to a morphism $\alpha : A^* \to M$ can be computed provided that $\mathcal{C}$-separation is decidable. Therefore, it is immediate that for each $e \in E(M)$, the $\mathcal{C}$-orbit of $e$ can be computed as well in this case. We state this property in the following lemma.
**LEMMA 5.6.** Let $\mathcal{C}$ be a class of languages with decidable separation. Then, given as input a morphism $\alpha : A^* \to M$ into a finite monoid and an idempotent $e \in E(M)$, one can compute the $\mathcal{C}$-orbit of $e$ for $\alpha$.

We complete the definition of $\mathcal{C}$-orbits by connecting it with another notion tailored to classes that are group prevarieties [32]. Given a class $\mathcal{G}$, we associate with any morphism $\alpha : A^* \to M$ (where $M$ is a finite monoid) a subset of $M$. We call this subset of $M$ the $\mathcal{G}$-kernel of $\alpha$. It consists of all elements $s \in M$ such that $\{\epsilon\}$ is not $\mathcal{G}$-separable from $\alpha^{-1}(s)$.

**REMARK 5.7.** While the definition makes sense for an arbitrary class $\mathcal{G}$, it is meant to be used in the special case when $\mathcal{G}$ is a group prevariety.

**REMARK 5.8.** When $\mathcal{G}$ is the class MOD of modulo languages, it can be shown that the MOD-kernel of a morphism corresponds to a standard notion: the stable monoid, defined in [46]. Given a morphism $\alpha : A^* \to M$ into a finite monoid, one can check that there exists $d \ge 1$ such that $\alpha(A^{2d}) = \alpha(A^d)$. The least such number $d \ge 1$ is called the stability index of $\alpha$. The stable monoid of $\alpha$ is $N = \{1_M\} \cup \alpha(A^d)$. One can verify that $N$ is the MOD-kernel of $\alpha$ (this follows from a simple analysis of MOD-separation).

Clearly, having a $\mathcal{G}$-separation algorithm in hand suffices to compute the $\mathcal{G}$-kernel of an input morphism $\alpha$. This yields the following lemma.

**LEMMA 5.9.** Let $\mathcal{G}$ be a class with decidable separation. Given as input a morphism $\alpha : A^* \to M$ into a finite monoid, one can compute the $\mathcal{G}$-kernel of $\alpha$.

When $\mathcal{G}$ is a group prevariety, $\mathcal{G}$-kernels are fully characterized by $\mathcal{G}$-orbits (see Appendix D).

**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$.

## 5.3 Characterization of $SF(\mathcal{C})$

Let us first recall the definition of aperiodic monoids. We use an equational definition, specific to finite monoids. We say that a finite monoid $M$ is aperiodic when every $s \in M$ satisfies $s^{\omega+1} = s^{\omega}$. We are ready to state the generic characterization of $SF(\mathcal{C})$. In fact, the statement also mentions the correspondence with $SD(\mathcal{C})$. This is important because we still have to prove the inclusion $SF(\mathcal{C}) \subseteq SD(\mathcal{C})$, and the argument is intertwined with the proof of the algebraic characterization.

**THEOREM 5.11.** Let $\mathcal{C}$ be a prevariety and consider a regular language $L \subseteq A^*$. The following properties are equivalent:

(1) $L \in SF(\mathcal{C})$.

(2) $L \in SD(\mathcal{C})$.

(3) All $\mathcal{C}$-orbits for the syntactic morphism of $L$ are aperiodic monoids.

Before we prove Theorem 5.11, let us discuss its consequences. First, it yields a transfer result for deciding of $SF(\mathcal{C})$-membership. It follows from Lemma 5.6 that the $\mathcal{C}$-orbits associated to a morphism into a finite monoid can be computed as soon as $\mathcal{C}$-separation is decidable. Hence, we obtain an algorithm for $SF(\mathcal{C})$-membership in this case. Given an input language $L$, one first computes its syntactic morphism $\alpha : A^* \to M$. Then, one computes all elements $s \in M$ belonging to a $\mathcal{C}$-orbit for $\alpha$ (this is possible, as $\mathcal{C}$-separation is decidable). Finally, it follows from Theorem 5.11 and the definition of aperiodicity that $L \in SF(\mathcal{C})$ if and only if every such element $s \in M$ satisfies $s^{\omega+1} = s^{\omega}$.

**COROLLARY 5.12.** If $\mathcal{C}$ be a prevariety with decidable separation, $SF(\mathcal{C})$-membership is decidable.
**Theorem 5.11** can be simplified in the special case of classes SF($\mathcal{G}$) where $\mathcal{G}$ is a group prevariety. In this case, it is possible to characterize the languages in SF($\mathcal{G}$) using only the $\mathcal{G}$-kernel of their syntactic morphisms. Indeed, we have the following statement as an immediate corollary of Theorem 5.11, Lemma 5.10 and the definition of aperiodic monoids.

**COROLLARY 5.13.** Let $\mathcal{G}$ be a group prevariety and consider a regular language $L$. The following properties are equivalent:

(1) $L \in SF(\mathcal{G})$.

(2) $L \in SD(\mathcal{G})$.

(3) The $\mathcal{G}$-kernel of the syntactic morphism of $L$ is an aperiodic monoid.

**REMARK 5.14.** Schützenberger's original characterization [41] of the class SF of star-free languages is an immediate consequence of Corollary 5.13. Indeed, consider a regular language $L$ and let $\alpha : A^* \to M$ be its syntactic morphism. Since $SF = SF(ST)$, it follows from Corollary 5.13 that $L \in SF$ if and only if the ST-kernel of $\alpha$ is aperiodic. Moreover, since $ST = \{0, A^*\}$ and syntactic morphisms are surjective, it is immediate that the ST-kernel of $\alpha$ is the whole syntactic monoid $M$. Hence, $L \in SF$ if and only if its syntactic monoid $M$ is aperiodic. This is exactly Schützenberger's theorem.

The proof of Theorem 5.11 is long and may seem technical. However, the underlying idea is simple. In the following remark, we discuss its most interesting direction and explain the intuition.

**REMARK 5.15.** The most interesting and difficult implication in Theorem 5.11 is (3) $\Rightarrow$ (2). The proof we present for it is inductive. The induction scheme, inspired by Wilke [51], has been adapted to meet our requirements. It is used thrice in the paper: in the proofs of Lemmas 5.16, F.2 and 9.8.

Each of these statements generalizes part of a related theorem (for example, Lemma 5.16 below generalizes the implication (3) $\Rightarrow$ (2) of Theorem 5.11). In each case, the objective is to prove that a language $L$ belongs to a specific class $\mathcal{D}$ (for instance, in the proof of the implication (3) $\Rightarrow$ (2) of Theorem 5.11, we aim to show that a language belongs to $\mathcal{D} = SD(\mathcal{C})$). However, in each of the three cases, the corresponding lemma establishes a stronger result than mere membership.

Typically, instead of simply proving that $L$ belongs to $\mathcal{D}$, the lemma provides a partition of $L$ into languages within $\mathcal{D}$. This partition is constructed inductively. To carry out the induction, we introduce additional parameters, which must be carefully chosen to suit the specific context of each lemma. This necessity explains why the induction scheme appears three times. Finally, the induction step itself is highlighted in a separate lemma (for instance, Lemma 5.16 carries out the inductive step for the implication (3) $\Rightarrow$ (2) in Theorem 5.11).

**PROOF OF THEOREM 5.11.** We fix a prevariety $\mathcal{C}$ for the proof. Moreover, we let $L \subseteq A^*$ be a regular language and $\alpha : A^* \to M$ be its syntactic morphism. We already proved that (2) $\Rightarrow$ (1) in Theorem 4.10. Hence, it suffices to prove that (1) $\Rightarrow$ (3) and (3) $\Rightarrow$ (2). The latter implication corresponds of the inclusion $SF(\mathcal{C}) \subseteq SD(\mathcal{C})$, which we omitted in the proof of Theorem 4.10.

**Implication (1) $\Rightarrow$ (3).** Assume that $L \in SF(\mathcal{C})$. For every idempotent $e \in E(M)$, we prove that the $\mathcal{C}$-orbit of $e$ for $\alpha$ is aperiodic. By definition, this boils down to proving that for all $s \in M$ such that $(e, s) \in M^2$ is a $\mathcal{C}$-pair for $\alpha$, we have $(ese)^{\omega+1} = (ese)^{\omega}$. By hypothesis on $\mathcal{C}$, it follows from Proposition 3.2 that $SF(\mathcal{C})$ is a prevariety. Hence, since $L \in SF(\mathcal{C})$, Proposition 2.3 implies that its syntactic morphism $\alpha$ is an $SF(\mathcal{C})$-morphism. Consequently, Proposition 3.3 yields a $\mathcal{C}$-morphism $\eta : A^* \to N$ such that for every $u \in A^*$, if $\eta(u)$ is idempotent, then we have $(\alpha(u))^{\omega+1} = (\alpha(u))^{\omega}$.

Since $\eta$ is a $\mathcal{C}$-morphism and $(e, s)$ is a $\mathcal{C}$-pair for $\alpha$, Lemma 5.3 yields $u, v \in A^*$ such that $\eta(u) = \eta(v)$, $\alpha(u) = e$ and $\alpha(v) = s$. Let $k = \omega(N)$. Clearly, $\eta(u^{k-1}vu^k) = \eta(u^k)$ is an idempotent of $N$. Hence, it follows from the definition of $\eta$ that $(\alpha(u^{k-1}vu^k))^{\omega+1} = (\alpha(u^{k-1}vu^k))^{\omega}$. Finally, since $\alpha(u) = e$ and $\alpha(v) = s$, this exactly says that $(ese)^{\omega+1} = (ese)^{\omega}$, as desired.
**Implication (3) ⇒ (2).** We assume that all $\mathcal{C}$-orbits for $\alpha$ are aperiodic monoids and prove that $L \in \text{SD}(\mathcal{C})$. By definition, this amounts to proving that $L$ can be constructed from the basic languages $\emptyset$ and $\{a\}$ for $a \in A$ using only the four operations available in the definition of $\text{SD}(\mathcal{C})$: intersection with $\mathcal{C}$, disjoint union, unambiguous concatenation and Kleene star for prefix codes with bounded synchronization delay. As announced in Remark 5.15, we argue by induction. The induction step is provided by Lemma 5.16. Let us set up some preliminary terminology.

Given a language $K \subseteq A^*$ and an element $s \in M$, we say that $K$ is s-safe when $s\alpha(u) = s\alpha(v)$ for every $u, v \in K$. For instance, if $s = 0_M$ is a zero of $M$, then the property of being s-safe is trivial, as every language is $0_M$-safe. On the other hand, a language is $1_M$-safe when all of its elements have the same image under $\alpha$. This is an interesting property: if we have in hand a finite partition of $A^*$ into $1_M$-safe languages from $\text{SD}(\mathcal{C})$, then $\alpha$ recognizes only languages of $\text{SD}(\mathcal{C})$. Indeed, any inverse image of an arbitrary element $t \in M$ is a union of languages of this partition. This motivates the following definition: given a language $P \subseteq A^*$, an $\text{SD}(\mathcal{C})$-partition of $P$ is a finite partition of $P$ into languages which all belong to $\text{SD}(\mathcal{C})$. The induction step is based on the following lemma.

**LEMMA 5.16.** Let $P \subseteq A^+$ be a prefix code with bounded synchronization delay such that there exists an $\text{SD}(\mathcal{C})$-partition $\mathbf{H}$ of $P$ whose elements are all $1_M$-safe. Then, for every $s \in M$, there exists an $\text{SD}(\mathcal{C})$-partition $\mathbf{K}$ of $P^*$ whose elements are all s-safe.

We first apply Lemma 5.16 to show that $L$ belongs to $\text{SD}(\mathcal{C})$ and conclude the main argument. In fact, the lemma implies that all languages recognized by $\alpha$ (including $L$) belong to $\text{SD}(\mathcal{C})$. By definition, $\text{SD}(\mathcal{C})$ is closed under disjoint union. Hence, it suffices to show that $\alpha^{-1}(t) \in \text{SD}(\mathcal{C})$ for every $t \in M$. We fix such an element $t$ in $M$.

Note that $A \subseteq A^+$ is a prefix code with bounded synchronization delay. Moreover, the set $\mathbf{H} = \{\{a\} | a \in A\}$ is an $\text{SD}(\mathcal{C})$-partition of $A$ such that every $H \in \mathbf{H}$ is $1_M$-safe. Hence, we may apply Lemma 5.16 in the case when $P = A$ and $s = 1_M$. We get an $\text{SD}(\mathcal{C})$-partition $\mathbf{K}$ of $A^*$ such that every $K \in \mathbf{K}$ is $1_M$-safe. Being $1_M$-safe means that $\alpha(K)$ is a singleton for every $K \in \mathbf{K}$. Therefore, $\alpha^{-1}(t)$ is the disjoint union of all $K \in \mathbf{K}$ intersecting $\alpha^{-1}(t)$. Since $\text{SD}(\mathcal{C})$ is closed under disjoint union, we obtain that $\alpha^{-1}(t) \in \text{SD}(\mathcal{C})$, which concludes the main argument.

It remains to prove Lemma 5.16. Let $P \subseteq A^*$ be a prefix code with bounded synchronization delay and consider an $\text{SD}(\mathcal{C})$-partition $\mathbf{H}$ of $P$ such that every $H \in \mathbf{H}$ is $1_M$-safe. Moreover, fix $s \in M$. We need to build an $\text{SD}(\mathcal{C})$-partition $\mathbf{K}$ of $P^*$ such that every $K \in \mathbf{K}$ is s-safe. We proceed by induction on the three following parameters listed by order of importance:

(1) The size of $\alpha(P^+) \subseteq M$.

(2) The size of $\mathbf{H}$.

(3) The size of $s \cdot \alpha(P^*) \subseteq M$.

We distinguish two cases depending on the following property of $s$ and $\mathbf{H}$. We say that $s$ is $\mathbf{H}$-stable when:

$$ \text{for every } H \in \mathbf{H}, \quad s \cdot \alpha(P^*) = s \cdot \alpha(P^*H). \qquad (3) $$

The base case happens when $s$ is $\mathbf{H}$-stable. We handle it directly. Otherwise, we use induction.

**Base case: $s$ is $\mathbf{H}$-stable.** This is the only part of the proof where we need the hypothesis that all $\mathcal{C}$-orbits for $\alpha$ are aperiodic monoids. Lemma 5.3 yields a $\mathcal{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 $\mathcal{C}$-pair for $\alpha$. We define,

$$ \mathbf{K} = \{P^* \cap \eta^{-1}(t) \mid t \in N\}. $$

Clearly, $\mathbf{K}$ is a partition of $P^*$. Moreover, it consists of languages in $\text{SD}(\mathcal{C})$. Indeed, we have $P \in \text{SD}(\mathcal{C})$: it is the disjoint union of all languages in the $\text{SD}(\mathcal{C})$-partition $\mathbf{H}$ of $P$. Therefore, $P^* \in \text{SD}(\mathcal{C})$ since $P$ is a prefix code with bounded synchronization delay. Hence, $P^* \cap \eta^{-1}(t) \in \text{SD}(\mathcal{C})$
for every $t \in N$ since $\eta^{-1}(t) \in \mathbb{C}$ (as $\eta$ is a $\mathbb{C}$-morphism). It remains to show that every language $K \in \mathbf{K}$ is $s$-safe. The argument is based on the following fact, which is where we use the hypothesis that $s$ is $\mathbf{H}$-stable.

**FACT 5.17.** Let $q, f \in \alpha(P^*)$ such that $f$ is idempotent. Then, we have $\mathrm{sqf} = \mathrm{sq}$.

**PROOF.** The proof is based on the following preliminary result. For every $u, v \in P^*$, we show that, there exists $r \in \alpha(P^*)$ such that $sr\alpha(u) = s\alpha(v)$. (4)

We fix $u, v \in P^*$ for the proof of (4). There exists a decomposition $u = u_1 \cdots u_n$ with $u_1, \dots, u_n \in P$. We use induction on the length $n$ of this decomposition. If $n = 0$, then $u = \varepsilon$ and it suffices to choose $r = \alpha(v) \in \alpha(P^*)$. Otherwise, $u = wu'$ with $w \in P$ and $u' \in P^*$ admits a decomposition of length $n-1$. Induction yields $r' \in \alpha(P^*)$ such that $sr'\alpha(u') = s\alpha(v)$. Moreover, since $w \in P$ and $H$ is a partition of $P$, there exists some $H \in \mathbf{H}$ such that $w \in H$. Since $s$ is $H$-stable and $r' \in \alpha(P^*)$, it follows from (3) that there exists $r \in \alpha(P^*)$ and $x \in \alpha(H)$ such that $sr' = srx$. Recall that $H \in \mathbf{H}$ is $1_M$-safe by hypothesis. Hence, since $x, \alpha(w) \in \alpha(H)$, we have $x = \alpha(w)$. Therefore, $sr' = sr\alpha(w)$. Altogether, this yields $sr\alpha(u) = sr\alpha(w)\alpha(u') = sr'\alpha(u') = s\alpha(v)$, which concludes the proof of (4).

It remains to prove the fact. Consider $q, f \in \alpha(P^*)$ such that $f$ is idempotent. By definition, there exist $u, v \in P^*$ such that $q = \alpha(v)$ and $f = \alpha(u)$. Hence (4) yields $r \in \alpha(P^*)$ such that $srf = \mathrm{sq}$. Since $f$ is idempotent, we obtain $\mathrm{sqf} = srff = srf = \mathrm{sq}$, which completes the proof. $\square$

We are ready to show that every language $K \in \mathbf{K}$ is $s$-safe. By definition, $K = P^* \cap \eta^{-1}(t)$ for $t \in N$. Given $u, v \in K$, we have to show that $s\alpha(u) = s\alpha(v)$. Let $n = \omega(M)$ and $e = (\alpha(u))^n \in E(M)$. Since $u, v \in K$, we have $\eta(u) = \eta(v) = t$. Hence, $\eta(u^n) = \eta(vu^{n-1})$. By definition of $\eta$, it follows that $(e, \alpha(vu^{n-1})) = (\alpha(u^n), \alpha(vu^{n-1}))$ is a $\mathbb{C}$-pair. Hence, $e\alpha(vu^{n-1})e$ belongs to the $\mathbb{C}$-orbit of $e$, which is aperiodic by hypothesis on $\alpha$. This yields $(e\alpha(vu^{n-1})e)^n = (e\alpha(vu^{n-1})e)^{n+1}$. Multiplying by $s$ on the left gives $s(e\alpha(vu^{n-1})e)^n = s(e\alpha(vu^{n-1})e)^{n+1}$. Since $n = \omega(M)$, we know that $(e\alpha(vu^{n-1})e)^n$ is an idempotent of $M$. Moreover, since $u, v \in K$, we have $(e\alpha(vu^{n-1})e)^n \in \alpha(P^*)$. Therefore, Fact 5.17 yields $s(e\alpha(vu^{n-1})e)^n = s$. Together with $s(e\alpha(vu^{n-1})e)^n = s(e\alpha(vu^{n-1})e)^{n+1}$, this yields $s = s\alpha(vu^{n-1})e$. We now multiply by $\alpha(u)$ on the right to get $s\alpha(u) = s\alpha(v)e$ (recall that $e = \alpha(u^n)$). Finally, $e$ is an idempotent of $M$ and since $u, v \in K$, we have $e, \alpha(v) \in \alpha(P^*)$. Hence, we may apply Fact 5.17 twice to get $s\alpha(v)e = s\alpha(v)$. Altogether, this yields $s\alpha(u) = s\alpha(v)$, as desired.

**Inductive step: $s$ is not $H$-stable.** By hypothesis, we know that (3) does not hold. Therefore, we get some $H \in \mathbf{H}$ such that the following strict inclusion holds,

$$s \cdot \alpha(P^*H) \subseteq s \cdot \alpha(P^*). \qquad (5)$$

We fix this language $H \in \mathbf{H}$ for the remainder of the proof. The following fact is proved by induction on our second parameter (the size of $H$).

**FACT 5.18.** There exists an $\mathrm{SD}(\mathbb{C})$-partition $U$ of $(P \setminus H)^*$ such that every $U \in U$ is $1_M$-safe.

**PROOF.** Clearly, $P \setminus H \subseteq P$ remains a prefix code with bounded synchronization delay by Fact 4.6. Moreover, it is immediate that $G = H \setminus \{H\}$ is an $\mathrm{SD}(\mathbb{C})$-partition of $P \setminus H$ such that every $G \in G$ is $1_M$-safe. Additionally, it is clear that $\alpha((P \setminus H)^+) \subseteq \alpha(P^+)$ (our first induction parameter has not increased) and $G \subseteq H$ (our second parameter has decreased). Hence, we may apply induction in Lemma 5.16 for the case when $P, H$ and $s$ have been replaced by $P \setminus H$, $G$ and $1_M$ respectively. This yields an $\mathrm{SD}(\mathbb{C})$-partition $U$ of $(P \setminus H)^*$ such that every $U \in U$ is $1_M$-safe. $\square$

We fix the partition $U$ of $(P \setminus H)^*$ given by Fact 5.18 for the remainder of the proof. We distinguish two independent subcases. Since $H$ is an element of the partition $H$ of $P$, we have $H \subseteq P$. It is
therefore immediate that the inclusion $\alpha(P^*H) \subseteq \alpha(P^+)$ holds. We use a different argument depending on whether this inclusion is strict or not.

**Subcase 1: we have the equality $\alpha(P^*H) = \alpha(P^+)$.** We handle this subcase with induction on our third parameter (i.e., the size of $s\alpha(P^*)$). Recall that we have to build an $SD(C)$-partition $K$ of $P^*$ containing only $s$-safe languages.

Observe that the hypothesis that $H$ is $1_M$-safe means that there exists some element $t \in M$ satisfying $\alpha(H) = \{t\}$. Similarly, since every $U \in U$ is $1_M$-safe, there exists some element $r_U \in M$ such that $\alpha(U) = \{r_U\}$. We fix these elements of $M$ for the rest of this subcase. The construction of $K$ is based on the following lemma, which is where we use our hypotheses and induction.

**FACT 5.19.** For every $U \in U$, there exists an $SD(C)$-partition $W_U$ of $P^*$ such that every $W \in W_U$ is $sr_U t$-safe.

**PROOF.** We fix $U \in U$ for the proof. Since $U$ is a partition of $(P \setminus H)^*$, we have $\alpha(U) \subseteq \alpha(P^*)$ which means that $r_U \in \alpha(P^*)$. Thus, we have $sr_U t \in s\alpha(P^*H)$. Therefore, $sr_U t \alpha(P^*) \subseteq s\alpha(P^+HP^*)$ and since $H \subseteq P$, we get $sr_U t \alpha(P^*) \subseteq s\alpha(P^+)$. Combined with our hypothesis in Subcase 1 (i.e., $\alpha(P^*H) = \alpha(P^+)$), this yields $sr_U t \alpha(P^*) \subseteq s\alpha(P^*H)$. Finally, the hypothesis (5) of the inductive step yields the strict inclusion $sr_U t \alpha(P^*) \subseteq s\alpha(P^*)$: the third parameter in our induction has decreased. On the other hand, the first two parameters have not increased, as they only depend on $P$ and $H$, which remain unchanged. Consequently, by induction, we may apply Lemma 5.16 in the case when $s \in M$ has been replaced by $sr_U t \in M$. This yields the desired $SD(C)$-partition $W_U$ of $P^*$. $\square$

We are ready to define the partition $K$ of $P^*$. Using Fact 5.19, we define,

$$K = U \cup \bigcup_{U \in U} \{UHW \mid W \in W_U\}.$$

It remains to show that $K$ is an $SD(C)$-partition of $P^*$ and that every $K \in K$ is $s$-safe. Let us first verify that $K$ is a partition of $P^*$. Since $P$ is a prefix code, every word $w \in P^*$ admits a unique decomposition $w = w_1 \cdots w_n$ with $w_1, \dots, w_n \in P$. If no factor $w_i$ belongs to $H$, then $w \in (P \setminus H)^*$ and $w$ belongs to some unique $U \in U$. Otherwise, let $w_i$ be the leftmost factor such that $w_i \in H$. This implies that $w_1 \cdots w_{i-1} \in (P \setminus H)^*$, which yields a unique $U \in U$ such that $w_1 \cdots w_{i-1} \in U$. Moreover, $w_{i+1} \cdots w_n \in P^*$, which yields a unique $W \in W_U$ such that $w_{i+1} \cdots w_n \in W$. It follows that $w \in UHW$, and that $UHW$ is the unique element of $K$ containing $w$.

Let us next verify that every $K \in K$ belongs to $SD(C)$. If $K \in U$, this is immediate by definition of $U$ in Fact 5.18. Otherwise, $K = UHW$ with $U \in U$ and $W \in W_U$. We know that $U, H, W \in SD(C)$: this an hypothesis for $H$ and stated in Facts 5.18 and 5.19 for $U$ and $W$. Furthermore, one can check that the concatenation $UHW$ is unambiguous since $P$ is a prefix code, $U \subseteq (P \setminus H)^*$ and $W \subseteq P^*$. Altogether, it follows that $K \in SD(C)$.

Finally, we prove that every $K \in K$ is $s$-safe. If $K \in U$, this is immediate since $K$ is actually $1_M$-safe by definition of $U$ in Fact 5.18. Otherwise, $K = UHW$ with $U \in U$ and $W \in W_U$. Consider $w, w' \in K$. We show that $s\alpha(w) = s\alpha(w')$. By definition, $\alpha(H) = \{t\}$ and $\alpha(U) = \{r_U\}$ which implies that $s\alpha(w) = sr_U \alpha(x)$ and $s\alpha(w') = sr_U \alpha(x')$ for $x, x' \in W$. Moreover, $W \in W_U$ is $sr_U t$-safe by definition in Fact 5.19. Therefore, $s\alpha(w) = s\alpha(w')$. This concludes the proof of Subcase 1.

**Subcase 2: we have the strict inclusion $\alpha(P^*H) \subseteq \alpha(P^+)$.** In this case, we use induction on the first parameter (i.e., the size of $\alpha(P^*)$). Recall that our objective is to construct an $SD(C)$-partition $K$ of $P^*$ containing only $s$-safe languages.

Consider a word $w \in P^*$. Since $P$ is a prefix code, $w$ admits a unique decomposition $w = w_1 \cdots w_n$ with $w_1, \dots, w_n \in P$. We can uniquely decompose $w$ in two (possibly empty) parts: a prefix $w_1 \cdots w_i \in ((P \setminus H)^*H)^*$ and a suffix in $w_{i+1} \cdots w_n \in (P \setminus H)^*$. Using induction, we construct
$SD(\mathcal{C})$-partitions of the possible prefixes and suffixes. Then, we combine them to construct a partition of the whole set $P^*$. Actually, we already handled the suffixes: Fact 5.18 provides an $SD(\mathcal{C})$-partition $U$ of $(P \setminus H)^*$. It remains to partition the prefixes. We do so this in the following fact, which is proved using the hypothesis of Subcase 2 and induction.

**FACT 5.20.** *There exists an $SD(\mathcal{C})$-partition $V$ of $((P \setminus H)^*H)^*$ such that every $V \in V$ is $1_M$-safe.*

**PROOF.** Let $Q = (P \setminus H)^*H$. In view of Fact 4.7, $Q$ is a prefix code with bounded synchronization delay. We apply induction in Lemma 5.16 for the case when $P$ has been replaced by $Q$. Doing so requires building an appropriate $SD(\mathcal{C})$-partition of $Q$ and proving that one of our induction parameters has decreased.

Let $F = \{UH \mid U \in U\}$. Since $U$ is a partition of $(P \setminus H)^*$ and $P$ is a prefix code, one can check that $F$ is a partition of $Q = (P \setminus H)^*H$. Moreover, it only contains languages in $SD(\mathcal{C})$. Indeed, if $U \in U$, then the concatenation $UH$ is unambiguous since $U \subseteq (P \setminus H)^*$ and $P$ is a prefix code. Moreover, $U, H \in SD(\mathcal{C})$ by hypothesis. Finally, $UH$ is $1_M$-safe since this is the case for both $U$ and $H$ by definition. It remains to show that our induction parameters have decreased. Since $Q = (P \setminus H)^*H$, it is clear that $Q^+ \subseteq P^*H$. Now, $\alpha(P^*H) \subseteq \alpha(P^+)$ by hypothesis in Subcase 2, whence $\alpha(Q^+) \subseteq \alpha(P^+)$: our first induction parameter has decreased. Thus, we may apply Lemma 5.16 in the case when $P, H$ and $s$ have been replaced by $Q$, $F$ and $1_M$ respectively. This yields the desired $SD(\mathcal{C})$-partition $V$ of $((P \setminus H)^*H)^*$. $\square$

We are ready to construct the $SD(\mathcal{C})$-partition $K$ of $P^*$ and conclude the main argument. Let $K = \{VU \mid V \in V \text{ and } U \in U\}$. It is immediate by definition that $K$ is a partition of $P^*$ since $P$ is a prefix code and $V, U$ are partitions of $((P \setminus H)^*H)^*$ and $(P \setminus H)^*$ respectively (cf. the above discussion). Moreover, every $K \in K$ belongs to $SD(\mathcal{C})$. Indeed, one can verify that $K$ is the unambiguous concatenation $VU$ of $V \in V$ and $U \in U$ which both belong to $SD(\mathcal{C})$. It remains to prove that every $K \in K$ is $s$-safe. Let $w, w' \in K$, we show that $s\alpha(w) = s\alpha(w')$. By definition, we have $K = VU$ with $V \in V$ and $U \in U$. Therefore, $w = vu$ and $w' = v'u'$ with $u, u' \in U$ and $v, v' \in V$. Since $U$ and $V$ are both $1_M$-safe by definition, we have $\alpha(u) = \alpha(u')$ and $\alpha(v) = \alpha(v')$. It follows that $s\alpha(w) = s\alpha(w')$, which concludes the proof of Lemma 5.16. $\square$

# 6 First logical characterization: first-order logic

We now turn to the logical characterizations of star-free closure. In this section, we present the first one. It generalizes a well-known theorem of McNaughton and Papert [24], which characterizes the star-free languages as those which can be defined by a sentence of first-order logic equipped with the linear ordering (i.e., $SF = SF(ST) = FO(<)$). Here, we extend this theorem to all classes $SF(\mathcal{C})$ where $\mathcal{C}$ is a prevariety. More precisely, we associate a set $\mathbb{I}_{\mathcal{C}}$ of first-order predicates to every prevariety $\mathcal{C}$ (its definition is taken from [33]). Then, we show that $SF(\mathcal{C})$ contains exactly the languages that can be defined by a sentence of first-order logic equipped with the predicates in $\mathbb{I}_{\mathcal{C}}$ (i.e., $SF(\mathcal{C}) = FO(\mathbb{I}_{\mathcal{C}})$). First, we briefly recall the definition of first-order logic over words. Then, we present the theorem itself.

## 6.1 Definitions

We view each word $w \in A^*$ as a logical structure. Its domain is the set $Pos(w) = \{0, \dots, |w| + 1\}$ of positions in $w$. A position $i$ such that $1 \le i \le |w|$ carries a label in $A$. On the other hand, $0$ and $|w| + 1$ are dummy unlabeled positions. We use first-order logic FO to express properties of words $w$: a formula can quantify over the positions of $w$ with first-order variables and use a predetermined set of predicates to test properties of these positions. We also allow two constants "min" and "max" interpreted as the artificial unlabeled positions $0$ and $|w| + 1$. Let us briefly recall the definition.
**Signatures.** A signature is a (possibly infinite) set of predicates interpreted over words in $A^*$. For $k \in \mathbb{N}$, a predicate of arity $k$ over $A$ is given by a symbol $P$ and for every word $w \in A^*$, an interpretation of $P$ as a relation of arity $k$ over the set of positions of $w$. That is, with every word $w \in A^*$, the predicate $P$ associates a set of $k$-tuples of positions of $w$ (i.e., a subset of $((\mathrm{Pos}(w))^k)$). If $(i_1, \dots, i_k)$ is a $k$-tuple in this set, we say that $P(i_1, \dots, i_k)$ holds in $w$. All predicates we consider in practice are either unary (they have arity 1) or binary (they have arity 2). Let us present them.

First, we use label predicates. For every letter $a \in A$, we associate a unary predicate (also denoted by “a”). It is interpreted as the unary relation selecting all positions whose label is $a$: given a word $w \in A^*$ and $i \in \mathrm{Pos}(w)$, we have that $a(i)$ holds when the label of $i$ is “a”. In particular, if $a(i)$ holds, then $i$ cannot be one of the two artificial positions 0 and $|w| + 1$. Abusing notation, we write “A” for the set of all label predicates. Moreover, we use a binary predicate “<”, interpreted as the linear ordering between positions. Given a word $w$ and $i, j \in \mathrm{Pos}(w)$, we have that $<(i, j)$ holds if $i < j$. For the sake of improved readability, we use the infix notation, writing $i < j$ instead of $<(i, j)$.

Finally, with each class $C$, we associate two generic sets of predicates. The first one, written $\mathbb{I}_C$, contains a binary “infix” predicate $I_L(x, y)$ for every $L \in C$. Given $w \in A^*$ and two positions $i, j \in \mathrm{Pos}(w)$, we have $w \models I_L(i, j)$ when $i < j$ and $w(i, j) \in L$ (recall that $w(i, j)$ denotes the infix of $w$ obtained by keeping only the positions which are strictly between $i$ and $j$). The second set, written $\mathbb{P}_C$, contains a unary “prefix” predicate $P_L(x)$ for every $L \in C$. Given $w \in A^*$ and a position $i \in \mathrm{Pos}(w)$, we have $w \models P_L(i)$ when $0 < i$ and $w(0, i) \in L$.

**REMARK 6.1.** All classes $C$ that we consider in practice are prevarieties. In particular, this implies that $A^* \in C$. Hence, set $\mathbb{I}_C$ always contains the linear order predicate, since “$x < y$” is clearly equivalent to “$I_{A^*}(x, y)$”. In particular, when $C$ is the trivial prevariety $\mathrm{ST} = \{\emptyset, A^*\}$, the signature $\mathbb{I}_{\mathrm{ST}}$ contains only $I_{A^*}$ and $I_0$. Since $I_0(i, j)$ never holds, using $\mathbb{I}_{\mathrm{ST}}$ boils down to considering $\{<\}$.

**First-order formulas.** With a signature $\mathbb{S}$ (i.e., $\mathbb{S}$ is a possibly infinite set of predicates), we associate a set FO[$\mathbb{S}$] of first-order formulas. They are built-up from simple expressions called atomic formulas. The atomic formulas can test properties of the positions that were quantified by first-order variables using either equality or the predicates in $\mathbb{S}$. More precisely, they are of the form:

$$x_1 = x_2 \quad \text{or} \quad P(x_1, \dots, x_k),$$

where $P \in \mathbb{S}$ is a predicate of arity $k$ for some $k \in \mathbb{N}$ and, for every $i \le k$, $x_i$ is either a first-order variable or one of the two constants min and max (symbols can be repeated: it may happen that $x_i$ and $x_j$ are the same symbol for $i \ne j$). We define FO[$\mathbb{S}$] as the least set of expressions containing the atomic formulas and closed under the following rules:

* **Disjunction:** if $\varphi$ and $\psi$ are FO[$\mathbb{S}$] formulas, then so is $(\varphi \lor \psi)$.

* **Negation:** if $\varphi$ is an FO[$\mathbb{S}$] formula, then so is $(\neg \varphi)$.

* **Existential quantification:** for any first-order variable $x$, if $\varphi$ is an FO[$\mathbb{S}$] formula, then so is $(\exists x \varphi)$.

For the sake of improved readability, we omit the parentheses when there is no ambiguity. Moreover, we define the other standard logical connectives as abbreviations. We write $\varphi \land \psi$ for $\neg((\neg \varphi) \lor (\neg \psi))$ and $\varphi \Rightarrow \psi$ for $(\neg \varphi) \lor \psi$. We also write $\forall x \varphi$ for $\neg(\exists x \neg \varphi)$.

Finally, we use the standard notion of “free variable”. Let $\varphi$ be an FO[$\mathbb{S}$] formula. An occurrence of some variable $x$ in $\varphi$ is said to be bound when it occurs inside an atomic formula that is under the scope of a quantification $\exists x$. For example, in the following formula $a(x) \land \exists y (x < y \land b(y)) \land \exists x c(x)$, the occurrence of the variable $x$ inside the atomic formula $c(x)$ is bound. We say that a variable $x$ is free in a formula $\varphi$ if there exists an occurrence of $x$ in $\varphi$ that is not bound. For example, in the formula above, there also exist two occurrences of $x$ that are not bound (inside the atomic formula $a(x)$ and inside the atomic formula $x < y$). Hence, $x$ is a free variable of this formula. A sentence is a formula that has no free variable.
**Semantics.** We define when a word $w \in A^*$ satisfies a sentence $\varphi$ (a fact that we denote by $w \models \varphi$). The definition is by structural induction on the sentence $\varphi$. This means that we actually need to give the semantics of all formulas, not just sentences. Indeed, in general, a sentence can have subformulas with free variables. To tackle this issue, we need the notion of variable assignment. Let $w \in A^*$ be a word and let $\mathcal{X}$ be a finite set of variables. We define an assignment of $\mathcal{X}$ in $w$ as a map $\mu : \mathcal{X} \to \text{Pos}(w)$. Additionally, we canonically extend every such assignment as a map $\mu : \mathcal{X} \cup \{\text{min}, \text{max}\} \to \text{Pos}(w)$ by defining $\mu(\text{min}) = 0$ and $\mu(\text{max}) = |w| + 1$.

Let $\varphi$ be an FO[$\$$] formula and let $\mathcal{X}$ be a set of variables containing all free variables of $\varphi$. For every word $w \in A^*$ and every assignment $\mu : \mathcal{X} \to \text{Pos}(w)$, we write $w, \mu \models \varphi$ when one the following properties hold:

* $\varphi := \text{"}x_1 = x_2\text{"}$ and $\mu(x_1) = \mu(x_2)$ holds.

* $\varphi := \text{"}P(x_1, \dots, x_k)\text{"}$ for some predicate $P \in \$$ and $P(\mu(x_1), \dots, \mu(x_k))$ holds.

* $\varphi := \text{"}\psi \lor \chi\text{"}$ and either $w, \mu \models \psi$ or $w, \mu \models \chi$.

* $\varphi := \text{"}\neg\psi\text{"}$ and $w, \mu \models \psi$ (w does not satisfy $\psi$ under $\mu$).

* $\varphi := \text{"}\exists y \psi\text{"}$ and there exists an assignment $\gamma : \mathcal{X} \cup \{y\} \to \text{Pos}(w)$ such that $\mu(x) = \gamma(x)$ for every $x \in \mathcal{X} \setminus \{y\}$ and $w, \gamma \models \psi$.

The definition depends on an assignment $\mu : \mathcal{X} \to \text{Pos}(w)$ where $\mathcal{X}$ contains all free variables of $\varphi$. In particular, it may happen that $\mathcal{X}$ contains variables that are not free in $\varphi$. Yet, this is allowed only for the sake of simplifying the presentation: one can verify that whether $w, \mu \models \varphi$ only depends on the restriction of $\mu$ to the variables that are free in $\varphi$. In particular, when no variable is free (i.e., $\varphi$ is a sentence), whether $w, \mu \models \varphi$ holds is independent from the assignment $\mu$. Hence, we simply write $w \models \varphi$ in this case. Altogether, it follows that each sentence $\varphi$ of FO[$\$$] defines a language: we let $L(\varphi) = \{w \in A^* | w \models \varphi\}$.

**Classes associated to first-order logic.** To every set of predicates $\$$, we associate a class of languages FO($\$$). It consists of all languages that can be defined by a sentence in FO[$A, \$$] (that is, we use the signature $A \cup \$$, containing the label predicates and those in $\$$). For the sake of avoiding clutter, we often abuse terminology and speak of an FO($\$$)-sentence to mean an FO[$A, \$$]-sentence.

**REMARK 6.2.** *The notation FO($\$$) (representing a class of languages), resembles the notation FO[$\$$] (representing a set of formulas). This similarity is harmless; from now on, we exclusively use the former.*

**Example 6.3.** Let $A = \{a, b\}$. Let us present some languages in FO(<). In first-order sentences, we use the abbreviation "$x + 1 = y$" for the formula "$\neg(x < y) \land \exists z (x < z \land z < y)$". In other words, "+1" is interpreted as the successor relation over positions. We have $A^*aA^*bA^*a \in \text{FO}(<)$ since it is defined by the following sentence: $\exists x \exists y (x < y) \land a(x) \land b(y)) \land (\exists x a(x) \land (x + 1 = \text{max}))$. Moreover, $(ab)^* \in \text{FO}(<)$ as well, since it is defined by the following FO(<) sentence:

$$ \forall x \forall y (x + 1 = y) \Rightarrow \left( \begin{array}{lcl} (x = \min \land y = \max) & \lor & (x = \min \land a(y)) \\ \lor & (a(x) \land b(y)) & \lor & (b(x) \land a(y)) \\ \lor & (b(x) \land y = \max) & & \end{array} \right). $$

We are interested in classes FO($\mathbb{I}_c$) where $\mathbb{I}$ is a prevariety. Indeed, we prove below that FO($\mathbb{I}_c$) = SF($\mathbb{C}$) in such cases. However, when $\mathbb{C}$ is a group prevariety, the presentation of FO($\mathbb{I}_c$) can be simplified in view of the following lemma, proved in Appendix E.

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

**Example 6.5.** Lemma 6.4 applies to important sets of predicates. First, if $\mathcal{G}$ is the trivial prevariety $\text{ST} = \{\emptyset, A^*\}$, all predicates in $\mathbb{P}_{\text{ST}}$ are trivial. Hence, FO(<, $\mathbb{P}_{\text{ST}}$) = FO(<).

Next, let us consider the class MOD of modulo languages, consisting in Boolean combinations of languages $\{w \in A^* | |w| \equiv k \mod m\}$ with $k, m \in \mathbb{N}$ such that $k < m$. In this case, we obtain
first-order logic with *modular predicates*. For all $k, m \in \mathbb{N}$ such that $k < m$, the set "MOD" of *modular predicates* contains a unary predicate $M_{k,m}$ selecting the positions $i$ such that $i \equiv k \mod m$. One may use Lemma 6.4 to verify that $\text{FO}(<, \mathbb{P}_{\text{MOD}}) = \text{FO}(<, \text{MOD})$.

Finally, we consider the class AMT of *alphabet modulo testable languages*. If $w \in A^*$ and $a \in A$, we let $\#_a(w) \in \mathbb{N}$ be the number of occurrences of letter $a$ in $w$. The class AMT consists of all Boolean combinations of languages $\{w \in A^* | |w|_a \equiv k \mod m\}$ where $a \in A$ and $k, m \in \mathbb{N}$ such that $k < m$ (these are the languages recognized by commutative groups). In this case, we obtain first-order logic with *alphabetic modular predicates*. For all $a \in A$ and all $k, m \in \mathbb{N}$ the set "AMOD" of *alphabetic modular predicates* contains a unary predicate $M_{k,m}^a$ selecting the positions $i$ such that $|w(0, i)|_a \equiv k \mod m$. One may use Lemma 6.4 to verify that $\text{FO}(<, \mathbb{P}_{\text{AMT}}) = \text{FO}(<, \text{AMOD})$.

## 6.2 Main theorem

We can now present the main result of the section. It connects star-free closure to first-order logic for all input classes that are prevarieties.

**THEOREM 6.6.** Let $\mathcal{C}$ be a prevariety. Then, $\text{SF}(\mathcal{C}) = \text{FO}(\mathbb{I}_{\mathcal{C}})$.

**REMARK 6.7.** The hypothesis that the class $\mathcal{C}$ is a prevariety is crucial for Theorem 6.6. For instance, Lippert and Thomas [22] gave the example of a class $\mathcal{C}$ consisting of a single language, for which the inclusion $\text{SF}(\mathcal{C}) \supseteq \text{FO}(\mathbb{I}_{\mathcal{C}})$ fails.

Additionally, in view of Lemma 6.4, Theorem 6.6 can be simplified when the input class is a group prevariety $\mathfrak{G}$. More precisely, we have the following theorem.

**COROLLARY 6.8.** Let $\mathfrak{G}$ be a group prevariety. Then, $\text{SF}(\mathfrak{G}) = \text{FO}(<, \mathbb{P}_{\mathfrak{G}})$.

**REMARK 6.9.** Corollary 6.8 has interesting applications when combined with Corollary 5.13 (i.e., the algebraic characterization of the class SF($\mathfrak{G}$)): we obtain that a regular language belongs to FO(<, $\mathbb{P}_{\mathfrak{G}}$) if and only if the $\mathfrak{G}$-kernel of its syntactic morphism is aperiodic. In particular when $\mathfrak{G} = \text{MOD}$, recall from Remark 5.8 that MOD-kernels correspond to a standard notion: stable monoids. Hence, we obtain that a regular language belongs to FO(<, MOD) if and only if the stable monoid of its syntactic morphism is aperiodic. This is a well-known theorem of Barrington, Compton, Straubing and Thérien [4], whose original proof relies on entirely different techniques.

The proof of Theorem 6.6 if provided in Appendix E. Let us point out that both directions of the proofs are handled directly: we "translate" FO($\mathbb{I}_{\mathcal{C}}$) sentences into expressions witnessing membership in SF($\mathcal{C}$) and vice-versa.

## 7 Second logical characterization: linear temporal logic

We present a second logical characterization of star-free closure. It also generalizes a well-known result concerning the star-free languages: they are exactly those that can be defined in linear temporal logic (LTL). This is a consequence of Kamp's theorem [17] which implies the equality $\text{FO}(<) = \text{LTL}$. It then follows from the theorem of McNaughton and Papert that $\text{SF} = \text{FO}(<) = \text{LTL}$. Here, we introduce a generalized definition of linear temporal logic, which is parameterized by a class $\mathcal{C}$. Actually, we define two classes LTL($\mathcal{C}$) and LTLP($\mathcal{C}$). They generalize the two classical variants of linear temporal logic: without and with past, respectively. Then, we prove that $\text{SF}(\mathcal{C}) = \text{LTL}(\mathcal{C}) = \text{LTLP}(\mathcal{C})$ for every prevariety $\mathcal{C}$. The proof argument relies heavily on the characterizations of star-free closure that we already presented. The proof that $\text{LTLP}(\mathcal{C}) \subseteq \text{SF}(\mathcal{C})$ is based on the equality $\text{SF}(\mathcal{C}) = \text{FO}(\mathbb{I}_{\mathcal{C}})$ (Theorem 6.6). Moreover, the proof that $\text{SF}(\mathcal{C}) \subseteq \text{LTL}(\mathcal{C})$ uses the algebraic characterization of star-free closure (Theorem 5.11).
## 7.1 Preliminaries

We first define the generalized notion of “linear temporal logic over finite words”. Then, we present some results about it, which are useful to prove the correspondence with star-free closure.

**Syntax.** For every class $\mathcal{C}$, we define two sets of temporal formulas denoted by LTL[$\mathcal{C}$] and LTLP[$\mathcal{C}$], which generalize the classical notions of “linear temporal logic” and “linear temporal logic with past”. We first define the LTLP[$\mathcal{C}$] formulas, which are more general.

A particular formula is built from the atomic formulas using Boolean connectives and temporal modalities. The atomic formulas are: min, max, $\top$ and $a$ for every letter $a \in A$. Moreover, we allow all Boolean connectives: if $\psi_1$ and $\psi_2$ are LTLP[$\mathcal{C}$] formulas, then so are $(\psi_1 \lor \psi_2)$, $(\psi_1 \land \psi_2)$ and $(\neg \psi_1)$. Finally, there are two binary temporal modalities “until” and “since”. They are parameterized by a language in $\mathcal{C}$. If $\psi_1$ and $\psi_2$ are LTLP[$\mathcal{C}$] formulas and $L \in \mathcal{C}$, then the following expressions are LTLP[$\mathcal{C}$] formulas as well:

$$ (\psi_1 \mathrm{U}_L \psi_2) \quad \text{and} \quad (\psi_1 \mathrm{S}_L \psi_2). $$

Moreover, we write “U” for “$U_{A^*}$” and “S” for “$S_{A^*}$” (their semantics will be the same as the standard modalities “until” and “since” in classical linear temporal logic). We also use the following abbreviations: given an LTLP[$\mathcal{C}$] formula $\psi$ and a language $L \in \mathcal{C}$, we write $F_L \psi$ for $\top U_L \psi$ and $X \psi$ for $(\neg \top) U \psi$.

Finally, an LTL[$\mathcal{C}$] formula is an LTLP[$\mathcal{C}$] formula that only contains “until” modalities (i.e., “since” is disallowed).

**Semantics.** In order to evaluate an LTLP[$\mathcal{C}$] formula $\varphi$, one needs a word $w \in A^*$ and a position $i \in \mathrm{Pos}(w)$. We use structural induction to define when the pair $(w, i)$ satisfies the formula $\varphi$. We denote this property by $w, i \models \varphi$:

* **Atomic formulas:** We always have $w, i \models \top$. For $a \in A$, we have $w, i \models a$ when $a$ is the letter at position $i$ in $w$. Moreover, we have $w, i \models \min$ when $i = 0$ (i.e., $i$ is the leftmost unlabeled position) and $w, i \models \max$ when $i = |w| + 1$ (i.e., $i$ is the rightmost unlabeled position).

* **Disjunction:** $w, i \models \psi_1 \lor \psi_2$ when $w, i \models \psi_1$ or $w, i \models \psi_2$.

* **Conjunction:** $w, i \models \psi_1 \land \psi_2$ when $w, i \models \psi_1$ and $w, i \models \psi_2$.

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

* **Until:** $w, i \models \psi_1 \mathrm{U}_L \psi_2$ when there exists $j \in \mathrm{Pos}(w)$ such that $i < j$, $w(i, j) \in L$, and,
  (1) For every $k \in \mathrm{Pos}(w)$ such that $i < k < j$, we have $w, k \models \psi_1$, and,
  (2) $w, j \models \psi_2$.

* **Since:** $w, i \models \psi_1 \mathrm{S}_L \psi_2$ when there exists $j \in \mathrm{Pos}(w)$ such that $j < i$, $w(j, i) \in L$ and,
  (1) For every $k \in \mathrm{Pos}(w)$ such that $j < k < i$, we have $w, k \models \psi_1$, and,
  (2) $w, j \models \psi_2$.

It remains to define what it means for a single word $w$ (without any distinguished position) to satisfy an LTL[$\mathcal{C}$] formula $\varphi$: we evaluate formulas at the leftmost unlabeled position of each word. That is, we say that a word $w \in A^*$ satisfies $\varphi$ and write $w \models \varphi$ if and only if $w, 0 \models \varphi$. The language defined by the formula $\varphi$ is $L(\varphi) = \{w \in A^* | w \models \varphi\}$.

Finally, we let LTL($\mathcal{C}$) (resp. LTLP($\mathcal{C}$)) be the class consisting of all languages defined by a formula in LTL[$\mathcal{C}$] (resp. LTLP[$\mathcal{C}$]). The classes LTL(ST) and LTLP(ST) (where ST = {$\emptyset, A^*$}) is the trivial prevariety correspond to the classical variants of linear temporal logic from the literature. Typically, the classes LTL($\mathcal{G}$) and LTLP($\mathcal{G}$) associated to some standard group prevariety $\mathcal{G}$ (such as MOD or AMT), are also natural. We present an example using the class MOD of modulo languages.

**Remark 7.1.** Similarly to what we mentioned in Remark 6.2, the notation LTL($\mathcal{C}$) (representing a class of languages) bears a resemblance to LTL[$\mathcal{C}$] (representing a set of formulas). However, this
similarity is inconsequential, as the context will clearly indicate the intended meaning. Specifically, when discussing LTL[$\mathcal{C}$], we always refer to a formula from that set.

**Example 7.2.** Let $A = \{a, b\}$. The language $(ab)^*$ belongs to LTL(ST) since it is defined by the LTL[ST] formula $X (a \lor \max) \land ((a \Rightarrow X b) \land (b \Rightarrow X (a \lor \max)) \lor \max)$. Moreover, $(aa + bb)^* \in \text{LTL(MOD)}$. It is defined by the following LTL[MOD] formula:

$$ (F_{(AA)} \cdot \max) \land ((F_{(AA)} \cdot A \max) \Rightarrow ((a \land X a) \lor (b \land X b))) \lor \max). $$

**Properties.** We present a few properties of the classes LTL($\mathcal{C}$), which we shall use later for proving that $SF(\mathcal{C}) \subseteq \text{LTL}(\mathcal{C})$ (when $\mathcal{C}$ is a prevariety). A key point is that the proof involves auxiliary arbitrary alphabets, independent from the alphabet $A$ that we fix at the beginning. When $B$ is such an alphabet, we need to specify what are the languages over $B$ corresponding to the class LTL($\mathcal{C}$) (this is not clear since $\mathcal{C}$ will be defined over our fixed alphabet $A$). We shall do so using morphisms $\eta : B^* \to N$ that we obtain from the class $\mathcal{C}$.

Let $B$ be an alphabet and $\eta : B^* \to N$ be a morphism into a finite monoid. An LTL[$\mathcal{D}$] formula is an LTL[$\mathcal{D}$] formula $\varphi$ where $\mathcal{D}$ is the (finite) class consisting of all languages recognized by $\eta$ (in particular, this means that atomic formulas in $\varphi$ are min, max, $\top$ and letters from $B$). Additionally, we let LTL($\eta$) be the class consisting of all languages (over $B$) that can be defined by an LTL[$\eta$] formula. We now state two lemmas proved in Appendix F, which are useful to build LTL[$\eta$] formulas.

**LEMMA 7.3.** Let $B$ be an alphabet, $\eta : B^* \to N$ be a morphism into a finite monoid and $L \in \text{LTL}(\eta)$. There exists a formula $\varphi \in \text{LTL}(\eta)$ such that for every $w \in B^*$ and $i \in \text{Pos}(w)$ we have $w, i \models \varphi$ if and only if $w(i, |w| + 1) \in L$.

**LEMMA 7.4.** Let $B$ be an alphabet, $\eta : B^* \to N$ be a morphism into a finite monoid, $L \in \text{LTL}(\eta)$ and $\zeta \in \text{LTL}(\eta)$. There exists a formula $\varphi \in \text{LTL}(\eta)$ such that for all $w \in B^*$ and $i \in \text{Pos}(w)$, we have $w, i \models \varphi$ if and only if there exists $j \in \text{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$.

## 7.2 Main Theorem

It is well-known that we have $SF = FO(<) = \text{LTL}(\text{ST}) = \text{LTLP}(\text{ST})$. The equality $FO(<) = \text{LTL}(\text{ST}) = \text{LTLP}(\text{ST})$ follows from Kamp's theorem [17] (these equalities are only an instance of Kamp's theorem, which is more general, as it connects first-order logic to linear temporal logic for more general structures than finite words). Then, the equality $SF = FO(<)$ follows from the work of McNaughton and Papert [24]. Here, we generalize this result to arbitrary input classes that are prevarieties. More precisely, we prove the following theorem.

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

Note that, in view of Corollary 5.12, Theorem 7.5 implies that for every prevariety $\mathcal{C}$ with decidable separation, the class LTL($\mathcal{C}$) = LTLP($\mathcal{C}$) has decidable membership. We prove Theorem 7.5 in Appendix F.

## 8 Rating maps

We now focus on the two decision problems of interest: separation and covering, as defined in Section 2.2. We prove two results in the paper. In Section 9, we show that $SF(\mathcal{C})$-covering is decidable for every finite prevariety $\mathcal{C}$. Then, in Section 10, we prove that $SF(\mathcal{G})$-covering is decidable for every group prevariety $\mathcal{G}$ that has decidable separation. In both cases, the algorithms are based on
a generic framework which was introduced in [40] for the specific purpose of handling separation and covering. It relies on simple algebraic objects called *rating maps*. We recall this framework in this preliminary section.

We define rating maps and present two particular kinds: the nice and the multiplicative ones. We use this notion to associate a computational problem with each lattice $\mathcal{C}$: "given as input a nice multiplicative rating map $\rho$ and a regular language $L$, compute an optimal $\mathcal{C}$-cover of $L$ for $\rho$". Then, we connect this problem to $\mathcal{C}$-covering, thanks to the notion of *optimal imprint* introduced in [40]. Finally, we present a refinement of this notion, called "nested optimal imprint", specifically designed for handling the classes of the form $Op(\mathcal{C})$ built from an input class $\mathcal{C}$ using an operator. In the paper, we are interested in the case when $Op$ is star-free closure.

## 8.1 Definition

We first introduce *rating algebras*. A *rating algebra* is a monoid $(R, +)$ which is *commutative* $(q + r = r + q$ for every $q, r \in R$) and *idempotent* $(r + r = r$ for all $r \in R)$. The binary operation $+$ is called *addition* and we denote the neutral element of $R$ by $0_R$ (we use an additive notation here, since we are dealing with a commutative monoid). Given a rating algebra $R$, we also define a canonical ordering $\leq$ over $R$ as follows:

$$ \text{for all } r, s \in R, \quad r \leq s \text{ when } r + s = s. $$

One can verify that $\leq$ is a partial order and that it makes $R$ an ordered monoid (i.e., $\leq$ is compatible with addition). It can be verified that every morphism between two rating algebras is increasing for the canonical orderings. We often use this property implicitly.

**Example 8.1.** For every set $S$, the algebra $(2^S, \cup)$ is a rating algebra whose neutral element is $\emptyset$. The canonical ordering $\leq$ on $2^S$ is inclusion. Indeed, given $P, Q \in 2^S$, it is clear that $P \subseteq Q$ if and only if $P \cup Q = Q$. In particular, if $A$ is an alphabet, then $(2^{A^*}, \cup)$ is a rating algebra. In practice, these are the only *infinite* rating algebras that we shall consider.

We often apply a "downset operator" to subsets of our rating algebras $R$. That is, for every $S \subseteq R$, we write $\downarrow_R S$ for the set $\downarrow_R S = \{r \mid \exists s \in S \text{ such that } r \leq s\}$. We also consider Cartesian products $X \times R$ of an arbitrary set $X$ with a rating algebra $R$. Given $S \subseteq X \times R$, we write $\downarrow_R S = \{(x, r) \in X \times R \mid \exists r' \in R \text{ such that } r \leq r' \text{ and } (x, r') \in S\}$.

**Definition of a rating map.** As seen above, $(2^{A^*}, \cup)$ is a rating algebra. A *rating map* (over $A$) is a monoid morphism $\rho : (2^{A^*}, \cup) \to (R, +)$ where $(R, +)$ is an arbitrary *finite* rating algebra. In other words, we have $\rho(\emptyset) = 0_R$ and $\rho(K_1 \cup K_2) = \rho(K_1) + \rho(K_2)$ for all $K_1, K_2 \subseteq A^*$. Note that since rating maps are morphisms of rating algebras, they are necessarily increasing: if $K_1 \subseteq K_2$, then $\rho(K_1) \leq \rho(K_2)$. For the sake of improved readability, when applying a rating map $\rho$ to a singleton language $K = \{w\}$ (i.e., $w \in A^*$ is a word), we write $\rho(w)$ for $\rho(\{w\})$. We often consider rating maps satisfying additional properties.

**Nice rating maps.** We say that a rating map $\rho : 2^{A^*} \to R$ is nice to indicate that for every language $K \subseteq A^*$, there exists a *finite* set $F \subseteq K$ such that $\rho(K) = \rho(F)$.

**REMARK 8.2.** Not all rating maps are nice. Consider the rating algebra $R = \{0, 1\}$ whose addition is defined by $i + j = \max(i, j)$ for $i, j \in R$. We define $\rho : 2^{A^*} \to R$ by $\rho(K) = 0$ if $K \subseteq A^*$ is finite and $\rho(K) = 1$ if $K \subseteq A^*$ is infinite. One can check that $\rho$ is not nice: if $K$ is infinite, then $\rho(K) = 1$ while $\rho(F) = 0$ for every finite subset $F \subseteq K$.

The definition of nice rating maps motivates the following object. For every rating map $\rho : 2^{A^*} \to R$ (nice or not), we associate a map $\rho_* : A^* \to R$ defined as the restriction of $\rho$ to $A^*$: for
every $w \in A^*$, $\rho_*(w) = \rho(\{w\})$. One can verify that when $\rho$ is nice, it is characterized by $\rho_*$. More precisely, for every $K \subseteq A^*$, we have $\rho(K) = \sum_{w \in K} \rho_*(w)$ (the sum is well-defined as it boils down to a finite one since $\rho$ is nice and $R$ is idempotent and commutative).

**Multiplicative rating maps.** The rating algebras of multiplicative rating maps have more structure: they are *idempotent semirings*. A semiring is a tuple $(R, +, \cdot)$ where $R$ is a set and “+” and “\cdot” are two binary operations, such that the following axioms are satisfied:

* $(R, +)$ is a commutative monoid (its neutral element is denoted by $0_R$).

* $(R, \cdot)$ is a monoid (its neutral element is denoted by $1_R$).

* The neutral element of $(R, +)$ is a zero for multiplication: $0_R r = r 0_R = 0_R$ for all $r \in R$.

* The multiplication distributes over addition: $r(s + t) = rs + rt$ and $(r + s)t = rt + st$ for every $r, s, t \in R$.

Finally, a semiring $(R, +, \cdot)$ is *idempotent* when $r + r = r$ for every $r \in R$ (on the other hand, there is no additional constraint on the multiplication). By definition, it follows that in this case, the additive monoid $(R, +)$ is a rating algebra.

*Example 8.3.* For every alphabet $A$, the triple $(2^{A^*}, \cup, \cdot)$ is an idempotent semiring (here, we use language concatenation “\cdot” as the multiplication; its neutral element is the singleton $\{\varepsilon\}$).

A rating map $\rho : 2^{A^*} \to R$ is *multiplicative* when the rating algebra $(R, +)$ is equipped with a second binary operation “\cdot” such that $(R, +, \cdot)$ is an *idempotent semiring* and $\rho$ is also a monoid morphism from $(2^{A^*}, \cdot)$ to $(R, \cdot)$. Thus, the axioms are as follows:

(1) $\rho(\emptyset) = 0_R$ and for all $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 all $K_1, K_2 \subseteq A^*$, we have $\rho(K_1 K_2) = \rho(K_1) \cdot \rho(K_2)$.

Altogether, this exactly says that $\rho$ is a semiring morphism from $(2^{A^*}, \cup, \cdot)$ to $(R, +, \cdot)$.

A key point is that a rating map $\rho : 2^{A^*} \to (R, +, \cdot)$ that is both *nice* and *multiplicative* can be finitely represented. Indeed, since $\rho$ is nice, it is characterized by the map $\rho_* : A^* \to R$. Moreover, since $\rho$ is multiplicative, $\rho_*$ is a monoid morphism from $A^*$ to $(R, \cdot)$. Altogether, it follows that $\rho$ is finitely representable: it suffices to store the image $\rho(a) \in R$ of each letter $a \in A$ as well as the addition and multiplication tables of $(R, +, \cdot)$. This means that we can speak of algorithms *taking a nice multiplicative rating map as input*.

**Canonical nice multiplicative rating map associated to a morphism.** We complete the presentation with a simple construction. It associates a canonical nice multiplicative rating map to a morphism into a finite monoid. We shall use it to make the link with covering. Consider a morphism $\alpha : A^* \to M$ into a finite monoid. We associate a nice multiplicative rating map $\rho_\alpha : 2^{A^*} \to 2^M$ to $\alpha$. Consider the triple $(2^M, \cup, \cdot)$ whose multiplication is defined as follows for all $T, T' \in 2^M$:

$$TT' = \{tt' \in M \mid t \in T \text{ and } t' \in T'\}.$$

One can check that $(2^M, \cup, \cdot)$ is an idempotent semiring. For every $K \subseteq A^*$, we define,

$$\rho_\alpha(K) = \alpha(K) = \{t \in M \mid \alpha^{-1}(t) \cap K \neq \emptyset\}.$$

One can check that $\rho_\alpha : 2^{A^*} \to 2^M$ is a *nice multiplicative rating map*.

## 8.2 Optimal covers and optimal imprints.

Now that we have defined what rating maps are, we turn to imprints. Consider a rating map $\rho : 2^{A^*} \to R$. Given any finite set of languages $K$, we define the $\rho$-imprint of $K$. Roughly speaking, when $K$ is a cover of some language $L$, this object measures the “quality” of $K$, which is a subset
of R. Intuitively, the smaller the imprint, the better the cover. The $\rho$-imprint of $K$ is the subset of $R$ defined by:

$$ \mathcal{I}[\rho](K) = \downarrow_R \{\rho(K) \mid K \in K\}. $$

We now define optimality. Consider an arbitrary rating map $\rho: 2^{A^*} \to R$ and a lattice $\mathcal{D}$. Given a language $L$, an optimal $\mathcal{D}$-cover of $L$ for $\rho$ is a $\mathcal{D}$-cover $K$ of $L$ having the least possible imprint among all $\mathcal{D}$-covers, i.e., which satisfies the following property:

$$ \mathcal{I}[\rho](K) \subseteq \mathcal{I}[\rho](K') \text{ for every } \mathcal{D}\text{-cover } K' \text{ of } L. $$

In general, there can be infinitely many optimal $\mathcal{D}$-covers for a given rating map $\rho$. The key point is that there always exists at least one, provided that $\mathcal{D}$ is a lattice. We state this simple property in the following lemma (proved in [40, Lemma 4.15]).

**LEMMA 8.4.** Let $\mathcal{D}$ be a lattice. For every language $L$ and every rating map $\rho$, there exists an optimal $\mathcal{D}$-cover of $L$ for $\rho$.

Clearly, given a lattice $\mathcal{D}$, a language $L$ and a rating map $\rho$, all optimal $\mathcal{D}$-covers of $L$ for $\rho$ have the same $\rho$-imprint. Hence, this unique $\rho$-imprint is a canonical object for $\mathcal{D}$, $L$ and $\rho$. We call it the optimal $\rho$-imprint on $L$ for $\mathcal{D}$ and we denote it by $\mathcal{I}_{\mathcal{D}}[L, \rho]$:

$$ \mathcal{I}_{\mathcal{D}}[L, \rho] = \mathcal{I}[\rho](K) \text{ for any optimal } \mathcal{D}\text{-cover } K \text{ of } L \text{ for } \rho. $$

An important special case is when $L = A^*$. In this case, we write $\mathcal{I}_{\mathcal{D}}[\rho]$ for $\mathcal{I}_{\mathcal{D}}[A^*, \rho]$. Let us present a few properties of optimal imprints. First, we have the following useful fact (proved in [40, Facts 4.16 and 4.17]):

**FACT 8.5.** Let $\mathcal{C}$ and $\mathcal{D}$ be lattices such that $\mathcal{C} \subseteq \mathcal{D}$, $\rho: 2^{A^*} \to R$ be a rating map and $H, L \subseteq A^*$ be two languages such that $H \subseteq L$. Then, $\mathcal{I}_{\mathcal{D}}[H, \rho] \subseteq \mathcal{I}_{\mathcal{C}}[L, \rho]$.

Additionally, we have the following lemma (proved in [39, Fact 4.7]):

**LEMMA 8.6.** Let $\mathcal{D}$ be a lattice and let $\rho: 2^{A^*} \to R$ be a rating map. Then, $\mathcal{I}_{\mathcal{D}}[\emptyset, \rho] = \emptyset$. Moreover, given two languages $H, L$, we have $\mathcal{I}_{\mathcal{D}}[H \cup L, \rho] = \mathcal{I}_{\mathcal{D}}[H, \rho] \cup \mathcal{I}_{\mathcal{D}}[L, \rho]$

We complete Lemma 8.6 with a similar statement for language concatenation instead of union (proved in [40, Lemma 5.8]). Note that it requires more hypotheses: $\mathcal{D}$ must be a prevariety and the rating map $\rho$ must be multiplicative.

**LEMMA 8.7.** Let $\mathcal{D}$ be a prevariety and let $\rho: 2^{A^*} \to R$ be a multiplicative rating map. Given two languages $H, L \subseteq A^*$, we have $\mathcal{I}_{\mathcal{D}}[H, \rho] \cdot \mathcal{I}_{\mathcal{D}}[L, \rho] \subseteq \mathcal{I}_{\mathcal{D}}[HL, \rho]$.

## 8.3 Connection with covering.

We now connect these definitions to the covering problem. The key idea is that solving $\mathcal{D}$-covering for a class $\mathcal{D}$ boils down to finding an algorithm that computes the optimal imprint for $\mathcal{D}$ from a nice multiplicative rating map given as input. In [40], two statements are presented. The first is simpler but it only applies Boolean algebras, while the second, more involved, applies to all lattices. Since all classes investigated in the paper are Boolean algebras, we only present the first one (see Appendix G for a proof sketch).

**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{I}_{\mathcal{D}}[\rho] \cap F = \emptyset$?
In view of Proposition 8.8, for a Boolean algebra $\mathcal{D}$, getting a $\mathcal{D}$-covering algorithm boils down to finding a procedure computing the set $\mathcal{J}_{\mathcal{D}}[\rho] \subseteq R$ from a nice multiplicative rating map $\rho : 2^{A^*} \to R$. In practice, these procedures are often presented as elegant *characterization theorems*. The key idea is that such a theorem should provide a description of the set $\mathcal{J}_{\mathcal{D}}[\rho] \subseteq R$, which yields an algorithm for computing it as an immediate corollary. Typically, such a result is called a “characterization of optimal imprints for $\mathcal{D}$”. For example a characterization of optimal imprints for SF is presented in [40] (recall that SF is the class of star-free languages). This procedure reformulates a result of [36] in the framework of rating maps.

*Example 8.9.* It is shown in [36, 40] that for every nice multiplicative rating map $\rho : 2^{A^*} \to R$, the optimal $\rho$-imprint for SF, $\mathcal{J}_{\mathcal{S}F}[\rho] \subseteq R$, is the least subset $S \subseteq R$ which satisfies the following conditions:

(1) **Trivial elements.** For every $w \in A^*$, we have $\rho(w) \in S$.

(2) **Closure under downset.** $\downarrow_{RS} = S$.

(3) **Closure under multiplication.** For every $q, r \in S$, we have $qr \in S$.

(4) **SF-closure.** For every $r \in S$, we have $r^\omega + r^{\omega+1} \in S$.

This characterization yields a *least fixpoint procedure* that computes $\mathcal{J}_{\mathcal{S}F}[\rho]$ from $\rho$: it starts from the set of all trivial elements and saturates it with the operations given by conditions (2)–(4) above. Together with Proposition 8.8, this yields the decidability of SF-covering.

In the paper, our aim is to generalize the characterization presented in Example 8.9 to arbitrary classes of the form $SF(C)$ where $C$ is a prevariety. We are able to handle two cases: the case when $C$ is a *finite prevariety* and the case when $C$ is a *group prevariety*. We present two characterizations of optimal imprints, one for each case. They are generic in the sense that each of them applies to families of classes rather than to a single class. This raises a question. Intuitively, a generic characterization of optimal imprints for $SF(C)$ should be parametrized by the class $C$. How is this achieved? It turns out that this requires to work with *more general objects capturing additional information*. Roughly speaking, given a nice multiplicative rating map $\rho : 2^{A^*} \to R$, our characterizations describe a single object that captures both $\mathcal{J}_{\mathcal{S}F}(\rho) \subseteq R$ and $\mathcal{J}_{\mathcal{C}}[\rho] \subseteq R$, as well as extra information, which connects them. The key idea is that while we are only interested in the set $\mathcal{J}_{\mathcal{S}F}(\rho)$, this more general object is required to formulate a characterization. This is not surprising since characterizations of optimal imprints are often *fixpoint descriptions*, as seen in Example 8.9. An important point is that these more general objects are also optimal imprints. However, they involve auxiliary rating maps built from $C$ and $\rho$. The last part of the section is devoted to defining these objects.

## 8.4 Nested optimal imprints

We introduce a construction from [31, 39], which takes as input a lattice $\mathcal{D}$ and a rating map $\rho : 2^{A^*} \to R$ and builds a new rating map $\xi_{\mathcal{D}}[\rho]$ whose rating algebra is $(2^R, \cup)$. We let,

$$ \begin{array}{rcl} \xi_{\mathcal{D}}[\rho] & : & 2^{A^*} \to (2^R, \cup) \\ & & K \mapsto \mathcal{J}_{\mathcal{D}}[K, \rho]. \end{array} $$

Let us reformulate Lemma 8.6, which exactly states that $\xi_{\mathcal{D}}[\rho] : 2^{A^*} \to (2^R, \cup)$ is itself a rating map.

**COROLLARY 8.10.** Let $\mathcal{D}$ be a lattice and $\rho : 2^{A^*} \to R$ a rating map. Then, $\xi_{\mathcal{D}}[\rho] : 2^{A^*} \to 2^R$ is a rating map as well.

Let us point out that $\xi_{\mathcal{D}}[\rho]$ is neither nice nor multiplicative in general, even if this is the case for the original rating map $\rho$. In practice, this is not an issue for the “multiplicative” property. Actually, $\xi_{\mathcal{D}}[\rho]$ is multiplicative when $\rho$ is multiplicative and the lattice $\mathcal{D}$ is a prevariety closed under concatenation (such as when $\mathcal{D} = SF(C)$). On the other hand, $\xi_{\mathcal{D}}[\rho]$ is rarely nice (see [39,
Example 6.3] for a counterexample). This is why it is important that most results of the framework hold for arbitrary rating maps.

Let us now provide some high-level intuition on why this construction is important when dealing with star-free closure. Consider some input prevariety $\mathcal{C}$. Since $SF(\mathcal{C})$ is a Boolean algebra, we know by Proposition 8.8 that in order to solve $SF(\mathcal{C})$-covering, it suffices to characterize the set $\mathcal{J}_{SF(e)}[\rho] \subseteq R$ for every nice multiplicative rating map $\rho : 2^{A^*} \to R$. Roughly speaking, the two characterizations of optimal imprints for $SF(\mathcal{C})$ that we present (for finite prevarieties $\mathcal{C}$ in Section 9 and for prevarieties of group languages in Section 10) consider the set $\mathcal{J}_e[\xi_{SF(e)}[\rho]] \subseteq 2^R$, which is more general. Indeed, one can check that $\mathcal{J}_{SF(e)}[\rho]$ is the union of all sets in $\mathcal{J}_e[\xi_{SF(e)}[\rho]]$. The point is that the extra information contained in this set is required in order to formulate these characterizations. Let us point out that this discussion is only meant to provide a sketchy general intuition. In practice, we shall refine these ideas by adopting an approach tailored to the two particular kinds of input prevarieties that we shall consider.

# 9 Covering for finite input classes

In this section, we prove that separation and covering are both decidable for the class $SF(\mathcal{C})$ when $\mathcal{C}$ is a finite prevariety. The algorithm is based on the framework introduced in Section 8: we present a generic effective characterization of optimal imprints for $SF(\mathcal{C})$. Given as input an arbitrary finite prevariety $\mathcal{C}$ and a nice multiplicative rating map $\rho : 2^{A^*} \to R$, it provides an effective description of the set $\mathcal{J}_{SF(e)}[\rho] \subseteq R$. By Proposition 8.8, having this set in hand suffices to decide $SF(\mathcal{C})$-covering. As announced at the end of Section 8, the characterization actually describes more information than just the set $\mathcal{J}_{SF(e)}[\rho] \subseteq R$. The first part of the section is devoted to defining the full object that we characterize. In the second part, we present the characterization itself and its proof.

## 9.1 Pointed optimal imprints

Consider an arbitrary finite prevariety $\mathcal{C}$. Recall that since $\mathcal{C}$ is finite, Lemma 2.5 implies that there exists a unique (up to renaming) $\mathcal{C}$-morphism recognizing exactly all languages in $\mathcal{C}$. We denote it by $\eta_e : A^* \to N_e$ and call it the canonical $\mathcal{C}$-morphism. The set $K = \{\eta_e^{-1}(t) | t \in N_e\}$ is the finest partition of $A^*$ into languages of $\mathcal{C}$. Consequently, $K$ is an optimal $\mathcal{C}$-cover of $A^*$ for all rating maps. In particular, if $\rho : 2^{A^*} \to R$ is a nice multiplicative rating map, then $K$ is an optimal $\mathcal{C}$-cover of $A^*$ for the auxiliary rating map $\xi_{SF(e)}[\rho] : 2^{A^*} \to 2^R$. By definition, it follows that,

$$ \mathcal{J}_e[\xi_{SF(e)}[\rho]] = \mathcal{J}[\xi_{SF(e)}[\rho]](K) = \downarrow_{2^R} \{\xi_{SF(e)}[\rho](K) | K \in \mathbf{K}\} = \downarrow_{2^R} \{\mathcal{J}_{SF(e)}[\eta_e^{-1}(t), \rho] | t \in N_e\}. $$

As explained in Section 8, the set $\mathcal{J}_e[\xi_{SF(e)}[\rho]]$ is exactly the information that our characterization of optimal imprints for $SF(\mathcal{C})$ will describe. More precisely, we characterize the family of sets $\mathcal{J}_{SF(e)}[\eta_e^{-1}(t), \rho] \subseteq R$ for $t \in N_e$. According to Lemma 8.6, the union of these sets is $\mathcal{J}_{SF(e)}[A^*, \rho] = \mathcal{J}_{SF(e)}[\rho]$, whose knowledge is enough to decide $SF(\mathcal{C})$-covering. Let us point out that this is also how the characterization depends on the finite prevariety $\mathcal{C}$: it is parametrized by the canonical $\mathcal{C}$-morphism $\eta_e : A^* \to N_e$. We now introduce additional notations that will be convenient in order to manipulate the family of sets $\mathcal{J}_{SF(e)}[\eta_e^{-1}(t), \rho]$ in our statements and our proofs.

**Definition.** Let $\mathcal{D}$ be a lattice, $\eta : A^* \to N$ be a morphism into a finite monoid and $\rho : 2^{A^*} \to R$ be a rating map. The $\eta$-pointed optimal $\rho$-imprint for $\mathcal{D}$ is defined as the following set $\mathcal{P}_{\mathcal{D}}[\eta, \rho] \subseteq N \times R$:

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

Clearly, $\mathcal{P}_{\mathcal{D}}[\eta, \rho]$ encodes all sets $\mathcal{J}_{\mathcal{D}}[\eta^{-1}(t), \rho]$ for $t \in N$. We shall use the notation in the case when $\mathcal{D} = SF(\mathcal{C})$ for some prevariety $\mathcal{C}$ and $\eta$ is the canonical $\mathcal{C}$-morphism $\eta_e$.
We complete the definition with a simple result which implies that $\mathcal{P}_D[\eta, \rho] \subseteq N \times R$ is more general than the set $\mathcal{J}_D[\rho] \subseteq R$. Indeed, since $\mathcal{J}_D[\rho] = \mathcal{J}_D[A^*, \rho]$, we have the following immediate corollary of Lemma 8.6.

**COROLLARY 9.1.** Let $\mathcal{D}$ be a lattice, $\eta : A^* \to N$ be a morphism into a finite monoid and $\rho : 2^{A^*} \to R$ be a multiplicative rating map. Then,

$$ \mathcal{J}_{\mathcal{D}}[\rho] = \bigcup_{t \in N} \mathcal{J}_{\mathcal{D}}[\eta^{-1}(t), \rho] = \{r \in R \mid \text{there exists } t \in N \text{ such that } (t, r) \in \mathcal{P}_{\mathcal{D}}[\eta, \rho]\}. $$

**Pointed covers.** Pointed optimal imprints are closer to being a notation rather than a new notion. Yet, it is possible to define them *directly* in terms of “covers”. This will be convenient for manipulating them. However, we have to slightly generalize the notion of cover in order to do so.

Consider a morphism $\eta : A^* \to N$ into a finite monoid and a language $L \subseteq A^*$. An $\eta$-pointed cover of $L$ is a finite set $\mathbf{K}$ of pairs $(s, K) \in N \times 2^{A^*}$ such that for every $w \in L$, there exists $(s, K) \in \mathbf{K}$ such that $\eta(w) = s$ and $w \in K$. In other words, the set $\{K \mid (s, K) \in \mathbf{K}\}$ must be a cover of $L \cap \eta^{-1}(s)$ for every $s \in N$. Additionally, given some class $\mathcal{D}$, we say that $\mathbf{K}$ is an $\eta$-pointed $\mathcal{D}$-cover when it also satisfies $K \in \mathcal{D}$ for each pair $(s, K) \in \mathbf{K}$.

We generalize imprints to pointed covers. Let $\eta : A^* \to N$ be a morphism into a finite monoid and $\rho : 2^{A^*} \to R$ a be rating map. If $\mathbf{K}$ is an $\eta$-pointed cover of some language $L \subseteq A^*$, we write,

$$ \mathcal{P}[\eta, \rho](\mathbf{K}) = \downarrow_{\mathcal{R}}\{(s, \rho(K)) \mid (s, K) \in \mathbf{K}\} \subseteq N \times R. $$

Here, we use the extended definition of the downset operation (see the definition on page 25). The following lemma provides an alternate definition of pointed optimal imprints. Roughly, it implies that when $\mathcal{D}$ is a lattice, there always exists an “optimal” $\eta$-pointed $\mathcal{D}$-cover $\mathbf{K}$ of $A^*$ (i.e., such that $\mathcal{P}[\eta, \rho](\mathbf{K})$ is minimal for inclusion) and that it satisfies $\mathcal{P}[\eta, \rho](\mathbf{K}) = \mathcal{P}_D[\eta, \rho]$.

**LEMMA 9.2.** Let $\mathcal{D}$ be a lattice, $\eta : A^* \to N$ be a morphism into a finite monoid and $\rho : 2^{A^*} \to R$ be a rating map. The two following properties hold:

* For every $\eta$-pointed $\mathcal{D}$-cover $\mathbf{K}$ of $A^*$, we have $\mathcal{P}_D[\eta, \rho] \subseteq \mathcal{P}[\eta, \rho](\mathbf{K})$.

* There exists an $\eta$-pointed $\mathcal{D}$-cover $\mathbf{K}$ of $A^*$ such that $\mathcal{P}_D[\eta, \rho] = \mathcal{P}[\eta, \rho](\mathbf{K})$.

**PROOF.** For the first assertion, let $\mathbf{K}$ be an $\eta$-pointed $\mathcal{D}$-cover of $A^*$ and let $(s, r) \in \mathcal{P}_D[\eta, \rho]$. Let $\mathbf{K}_s = \{K \mid (s, K) \in \mathbf{K}\}$, which is a $\mathcal{D}$-cover of $\eta^{-1}(s)$ by definition of pointed covers. Since $(s, r) \in \mathcal{P}_D[\eta, \rho]$, we have $r \in \mathcal{J}_D[\eta^{-1}(s), \rho]$, which yields $K \in \mathbf{K}_s$ such that $r \le \rho(K)$. By definition of $\mathbf{K}_s$, we have $(s, K) \in \mathbf{K}$. Hence, we get $(s, r) \in \mathcal{P}[\eta, \rho](\mathbf{K})$, as desired.

We turn to the second assertion. For every $s \in N$, let $\mathbf{K}_s$ be an optimal $\mathcal{D}$-cover of $\eta^{-1}(s)$ for $\rho$: $\mathcal{J}[\rho](\mathbf{K}_s) = \mathcal{J}_D[\eta^{-1}(s), \rho]$. We let $\mathbf{K} = \{(s, K) \mid s \in N \text{ and } K \in \mathbf{K}_s\}$. By definition, $\mathbf{K}$ is an $\eta$-pointed cover of $L$. Let us prove that $\mathcal{P}_D[\eta, \rho] = \mathcal{P}[\eta, \rho](\mathbf{K})$. The left to right inclusion is immediate from the first assertion. For the converse one, let $(s, r) \in \mathcal{P}[\eta, \rho](\mathbf{K})$. By definition of $\mathbf{K}$, we get $K \in \mathbf{K}_s$ such that $r \le \rho(K)$, i.e., $r \in \mathcal{J}[\rho](\mathbf{K}_s) = \mathcal{J}_D[\eta^{-1}(s), \rho]$. Hence, $(s, r) \in \mathcal{P}_E[\eta, \rho]$ by definition. $\square$

## 9.2 Characterization

Let us first present the characterization. Given an arbitrary morphism $\eta : A^* \to N$ into a finite monoid and a multiplicative rating map $\rho : 2^{A^*} \to R$, we define the SF-saturated subsets of $N \times R$ for $\eta$ and $\rho$ (this notion makes sense for arbitrary multiplicative rating maps, but it is only useful for those that are *nice*). Let $S \subseteq N \times R$. We say that $S$ is SF-saturated for $\eta$ and $\rho$ when it satisfies the following properties:

(1) **Trivial elements.** For every $w \in A^*$, we have $(\eta(w), \rho(w)) \in S$.

(2) **Closure under downset.** $\downarrow_{\mathcal{R}}S = S$.
(3) **Closure under multiplication.** For every $(s, q), (t, r) \in S$, we have $(st, qr) \in S$.

(4) **SF-closure.** For every $(e, r) \in S$, if $e \in N$ is an idempotent, then $(e, r^{\omega} + r^{\omega+1}) \in S$.

We are ready to present the characterization. Given a finite prevariety $\mathcal{C}$, if $\rho$ is nice, we show that the least SF-saturated subset of $N_{\mathcal{C}} \times R$ for $\eta_{\mathcal{C}}$ and $\rho$ is exactly $\mathcal{P}_{SF}(e)[\eta_{\mathcal{C}}, \rho]$.

**THEOREM 9.3.** Let $\mathcal{C}$ be a finite prevariety and $\rho: 2^{A^*} \to R$ be a nice multiplicative rating map. Then, $\mathcal{P}_{SF}(e)[\eta_{\mathcal{C}}, \rho]$ is the least SF-saturated subset of $N_{\mathcal{C}} \times R$ for $\eta_{\mathcal{C}}$ and $\rho$.

Given a nice multiplicative rating map $\rho: 2^{A^*} \to R$ as input, it is clear the one can compute the least SF-saturated subset of $N_{\mathcal{C}} \times R$ for $\eta_{\mathcal{C}}$ and $\rho$. This is achieved with a least fixpoint procedure. Hence, Theorem 9.3 provides an algorithm for computing $\mathcal{P}_{SF}(e)[\eta_{\mathcal{C}}, \rho]$. It then follows from Corollary 9.1 that one can compute $\mathcal{J}_{SF}(e)[\rho]$ from $\mathcal{P}_{SF}(e)[\eta_{\mathcal{C}}, \rho]$:

$$ \mathcal{J}_{SF}(e)[\rho] = \{r \in R \mid \text{there exists } t \in N \text{ such that } (t, r) \in \mathcal{P}_{SF}(e)[\eta_{\mathcal{C}}, \rho]\}. $$

Together with Proposition 8.8, we obtain that SF($\mathcal{C}$)-covering is decidable. Naturally, this result extends to separation by Lemma 2.2. Altogether, we get the following corollary.

**COROLLARY 9.4.** If $\mathcal{C}$ is a finite prevariety, SF($\mathcal{C}$)-covering and SF($\mathcal{C}$)-separation are decidable.

In practice, there are not many interesting applications of Corollary 9.4. Indeed, the only important class that is the star-free closure of a finite prevariety is the original class of star-free languages. Indeed, we have SF = SF(ST) where ST = {$\emptyset, A^*$}. It was already known that SF has decidable covering: we presented an effective characterization of optimal imprints for SF taken from [40] in Example 8.9. This specialized characterization is actually an immediate corollary of Theorem 9.3 since the canonical ST-morphism is the unique one $\eta_{ST}: A^* \to \{1\}$ into a trivial monoid $\{1\}$.

Nonetheless, Theorem 9.3 is an important result. Indeed, we shall use it as a subresult in the proof of our second characterization, which describes optimal imprints for SF($\mathcal{G}$) when $\mathcal{G}$ is a group prevariety (more precisely, we shall apply Propositions 9.5 and 9.6 below).

We turn to the proof of Theorem 9.3. It involves two independent statements, which correspond respectively to soundness and completeness of the least fixpoint procedure computing $\mathcal{P}_{SF}(e)[\eta_{\mathcal{C}}, \rho]$ from a nice multiplicative rating map $\rho$. Let us start with soundness, which is simpler to establish and does not require the hypothesis that $\rho$ is nice.

**PROPOSITION 9.5 (SOUNDNESS).** Consider a finite prevariety $\mathcal{C}$ and a multiplicative rating map $\rho: 2^{A^*} \to R$. Then, the set $\mathcal{P}_{SF}(e)[\eta_{\mathcal{C}}, \rho] \subseteq N_{\mathcal{C}} \times R$ is SF-saturated for $\eta_{\mathcal{C}}$ and $\rho$.

**PROOF.** Recall that SF($\mathcal{C}$) is a prevariety by Proposition 3.2. There are four properties to verify. We start with the first three, which are standard. For the trivial elements, consider $w \in A^*$ and let $K$ be an optimal SF($\mathcal{C}$)-cover of $\eta_c^{-1}(\eta_c(w))$. Since $w \in \eta_c^{-1}(\eta_c(w))$, there exists $K \in K$ such that $w \in K$. Therefore, $\rho(w) \le \rho(K)$, which yields $\rho(w) \in \mathcal{J}[\rho](K) = \mathcal{J}_{SF}(e)[\eta_c^{-1}(\eta_c(w)), \rho]$. By definition, this implies that $(\eta_c(w), \rho(w)) \in \mathcal{P}_{SF}(e)[\eta_c, \rho]$. Closure under downset is immediate by definition of imprints. Finally, for closure under multiplication, consider $(s_1, r_1)$, $(s_2, r_2) \in \mathcal{P}_{SF}(e)[\eta_c, \rho]$. We have $r_i \in \mathcal{J}_{SF}(e)[\eta_c^{-1}(s_i), \rho]$ for $i = 1, 2$. Since SF($\mathcal{C}$) is a prevariety, Lemma 8.7 yields $r_1r_2 \in \mathcal{J}_{SF}(e)[\eta_c^{-1}(s_1)\eta_c^{-1}(s_2), \rho]$. Clearly, $\eta_c^{-1}(s_1)\eta_c^{-1}(s_2) \subseteq \eta_c^{-1}(s_1s_2)$. Thus, Fact 8.5 yields $r_1r_2 \in \mathcal{J}_{SF}(e)[\eta_c^{-1}(s_1s_2), \rho]$. By definition, this exactly says that $(s_1s_2, r_1r_2) \in \mathcal{P}_{SF}(e)[\eta_c, \rho]$.

It remains to handle SF-closure. Let $(e, r) \in \mathcal{P}_{SF}(e)[\eta_c, \rho]$ be such that $e \in N_{\mathcal{C}}$ is idempotent. We show that $(e, r^{\omega} + r^{\omega+1}) \in \mathcal{P}_{SF}(e)[\eta_c, \rho]$. Let $K$ be an optimal SF($\mathcal{C}$)-cover of $\eta_c^{-1}(e)$. By definition, it now suffices to prove that $r^{\omega} + r^{\omega+1} \in \mathcal{J}[\rho](K)$. Since SF($\mathcal{C}$) is a prevariety, Proposition 2.4 yields an SF($\mathcal{C}$)-morphism $\alpha: A^* \to M$ recognizing every $K \in K$. Let $H$ be the set of all languages $\alpha^{-1}(x)$ for $x \in M$ such that $\alpha^{-1}(x) \cap \eta_c^{-1}(e) \ne \emptyset$. By definition, $H$ is an SF($\mathcal{C}$)-cover of $\eta_c^{-1}(e)$. Hence, since
$(e, r) \in \mathcal{P}_{SF(C)}[\eta_c, \rho]$, we have $r \in \mathcal{J}[\rho](\mathbf{H})$ which yields $H \in \mathbf{H}$ such that $r \le \rho(H)$. By definition of $\mathbf{H}$, we get $x \in M$ such that $H = \alpha^{-1}(x)$ and some word $u \in H \cap \eta_c^{-1}(e)$. Let $p = \omega(M) \times \omega(R)$ and $L = \alpha^{-1}(x^p)$. We claim that:

$$H^p \cup H^{p+1} \subseteq L. \qquad (6)$$

Let us first explain why this implies that $r^\omega + r^{\omega+1} \in \mathcal{J}[\rho](\mathbf{K})$. Since $u^p \in \eta_c^{-1}(e)$ (recall that $e \in N_c$ is idempotent) and $\mathbf{K}$ is a cover of $\eta_c^{-1}(e)$, we get $K \in \mathbf{K}$ such that $u^p \in K$. Moreover, since $u^p \in L = \alpha^{-1}(x^p)$ and $\mathbf{K}$ is recognized by $\alpha$ (by definition), it follows that $L \subseteq K$. Hence, since $r \le \rho(H)$ and $p = \omega(M) \times \omega(R)$, it follows from (6) that $r^\omega + r^{\omega+1} \le \rho(K)$ which yields $r^\omega + r^{\omega+1} \in \mathcal{J}[\rho](\mathbf{K})$, as desired.

It remains to prove (6). Let $w \in H^p \cup H^{p+1}$. We need to prove that $\alpha(w) = x^p$. This is immediate when $w \in H^p$ since $H = \alpha^{-1}(x)$. Assume now that $w \in H^{p+1}$. In that case, we have $\alpha(w) = x^{p+1}$. Hence, it suffices to prove that $x^{p+1} = x^p$. By hypothesis $\eta_c(u) = e$ is an idempotent of $N_c$. Since $\eta_c$ is the canonical $\mathcal{C}$-morphism, it follows from Lemma 2.5 that the image of $u$ under any $\mathcal{C}$-morphism is an idempotent. Hence, since $\alpha$ is an $SF(\mathcal{C})$-morphism, Proposition 3.3 implies that $(\alpha(u))^{\omega+1} = (\alpha(u))^{\omega}$. Since $x = \alpha(u)$ and $p = \omega(M) \times \omega(R)$, it follows that $x^{p+1} = x^p$, as desired. $\square$

We now turn to completeness. As usual, this is the most difficult part of the proof. Note that again, we shall rely on Theorem 4.10: we build our languages in $SF(\mathcal{C})$ using the operations available in the definition of $SD(\mathcal{C})$.

**PROPOSITION 9.6 (COMPLETENESS).** Let $\mathcal{C}$ be a prevariety, $\eta : A^* \to N$ be a $\mathcal{C}$-morphism, $\rho : 2^{A^*} \to R$ be a nice multiplicative rating map and $S \subseteq N \times R$ be an $SF$-saturated set for $\eta$ and $\rho$. There exists an $\eta$-pointed $SF(\mathcal{C})$-cover $\mathbf{K}$ of $A^*$ such that $\mathcal{P}[\eta, \rho](\mathbf{K}) \subseteq S$.

**PROOF.** We build the desired $\eta$-pointed $SF(\mathcal{C})$-cover $\mathbf{K}$ using induction. The argument is adapted from and generalizes the one we used for proving the difficult implication in Theorem 4.10: every language whose syntactic morphism has aperiodic $\mathcal{C}$-orbits is in $SD(\mathcal{C}) = SF(\mathcal{C})$. Let us start with some terminology that we need to present the induction.

A first point is that we build particular $\eta$-pointed covers. Let $P \subseteq A^*$ be an arbitrary language. An $\eta$-pointed $SF(\mathcal{C})$-partition of $P$ is a finite set $\mathbf{H} \subseteq N \times 2^{A^*}$ such that for every $(t, H) \in \mathbf{H}$, we have $H \in SF(\mathcal{C})$ and for every $t \in N$, the set $\{H | (t, H) \in \mathbf{H}\}$ is a partition of $P \cap \eta^{-1}(t)$ (this implies that $H \subseteq \eta^{-1}(t)$ for every $(t, H) \in \mathbf{H}$). Note that in particular, $\mathbf{H}$ is an $\eta$-pointed $SF(\mathcal{C})$-cover of $P$.

If $\mathbf{H}$ is an $\eta$-pointed $SF(\mathcal{C})$-partition, an $\mathbf{H}$-product is a pair $(t_1, \dots, t_n, H_1, \dots, H_n)$ for some $n \in \mathbb{N}$ where $(t_i, H_i) \in \mathbf{H}$ for every $i \le n$. In particular, the pair $(1_N, \{\epsilon\})$ is an $\mathbf{H}$-product: this is the case $n = 0$ in the definition. When $n \ge 1$, we speak of strict $\mathbf{H}$-products. Finally, an $\mathbf{H}$-union (resp. strict $\mathbf{H}$-union) is a pair $(t, G_1 \cup \dots \cup G_m)$ for some $t \in N$ and $m \in \mathbb{N}$ such that $(t, G_j)$ is an $\mathbf{H}$-product (resp. strict $\mathbf{H}$-product) for every $j \le m$. Note that $(t, \emptyset)$ is a strict $\mathbf{H}$-union for every $t \in \mathbb{N}$: this corresponds to the case $m = 0$ in the definition.

Additionally, we write $Q = N \times R$. Observe that $Q$ is a monoid for the componentwise multiplication. Moreover, $S \subseteq Q$ by definition. Finally, for every $\eta$-pointed $SF(\mathcal{C})$-partition of $\mathbf{H}$, we associate two subsets of $Q$. The definitions are as follows:

* We let $Q_H^+ \subseteq Q$ be the set of all elements $(t, \rho(H)) \in Q$ where $(t, H)$ is a strict $\mathbf{H}$-union.

* We let $Q_H^* \subseteq Q$ be the set of all elements $(t, \rho(H)) \in Q$ where $(t, H)$ is an $\mathbf{H}$-union.

Clearly, $Q_H^+ \subseteq Q_H^*$. Moreover, we have the following simple fact which we shall use implicitly throughout the proof.

**FACT 9.7.** Let $P \subseteq A^*$ and $\mathbf{H}$ be an $\eta$-pointed $SF(\mathcal{C})$-partition of $P$. For all $(t_1, q_1), (t_2, q_2) \in Q_H^*$, we have $(t_1 t_2, q_1 q_2) \in Q_H^*$.
PROOF. By definition, there are two H-unions ($t_1, H_1$), ($t_2, H_2$) ∈ H such that $q_i = \rho(H_i)$ for $i = 1, 2$. One can check from the definition that ($t_1t_2, H_1H_2$) remains an H-union since language distributes over union. Since $q_1q_2 = \rho(H_1H_2)$, it follows that ($t_1t_2, q_1q_2$) ∈ $Q_H^*$.
□

We are ready to prove Proposition 9.6. It is based on the following statement which we shall proving using induction.

LEMMA 9.8. Let $P \subseteq A^+$ be a prefix code with bounded synchronization delay and $H$ be an $\eta$-pointed $SF(\mathcal{C})$-partition of $P$ such that $(t, \rho(H)) \in S$ for every $(t, H) \in H$. Then, for every $(s, r) \in S$, there exists an $\eta$-pointed $SF(\mathcal{C})$-partition $K$ of $P^*$ such that,

$$ \text{for every } (t, K) \in K, \text{ we have } (t, \rho(K)) \in Q_H^* \text{ and } (st, r\rho(K)) \in S. \qquad (7) $$

Before we prove Lemma 9.8, let us first complete the main argument. We have to build an $\eta$-pointed $SF(\mathcal{C})$-cover $K$ of $A^*$ such that $\mathcal{P}[\eta, \rho](K) \subseteq S$. Observe that $A \subseteq A^+$ is a prefix code with bounded synchronization delay. Moreover, $H = \{(\eta(a), \{a\}) \mid a \in A\}$ is an $\eta$-pointed $SF(\mathcal{C})$-partition of $A$ and we have $(\eta(a), \rho(a)) \in S$ for every $a \in A$ since $S$ is $SF$-saturated (these are trivial elements). Finally, $(1_N, 1_R) \in S$ (again, this is a trivial element). Therefore, we may apply Lemma 9.8 in the case when $P = A$ and $(s, r) = (1_N, 1_R) \in S$. This yields an $\eta$-pointed $SF(\mathcal{C})$-partition $K$ of $A^*$ satisfying (7). In particular, $(t, \rho(K)) \in S$ for every $(t, K) \in K$. Therefore, since $S$ is $SF$-saturated, closure under downset yields $\mathcal{P}[\eta, \rho](K) \subseteq S$, which completes the proof.

We now prove Lemma 9.8. Let $P \subseteq A^+$ be a prefix code with bounded synchronization delay and $H$ be an $\eta$-pointed $SF(\mathcal{C})$-partition of $P$ such that $(t, \rho(H)) \in S$ for all $(t, H) \in H$. Finally, let $(s, r) \in S$. We need to build an $\eta$-pointed $SF(\mathcal{C})$-partition $K$ of $P^*$ satisfying (7). We proceed by induction on the three following parameters, listed by order of importance:

(1) The size of the set $Q_H^+ \subseteq Q$,

(2) The size of $H$,

(3) The size of the set $(s, r) \cdot Q_H^* \subseteq Q$.

We distinguish two main cases depending on the following property. We say that $(s, r)$ is H-stable when the following holds,

$$ \text{for every } (t, H) \in H, \quad (s, r) \cdot Q_H^* = (s, r) \cdot Q_H^* \cdot (t, \rho(H)). \qquad (8) $$

We first consider the case when $(s, r)$ is H-stable. This is the base case: we construct $K$ directly. Then, we handle the case when $(s, r)$ is not H-stable using induction on our three parameters.

Base case: $(s, r)$ is H-stable. In this case, we let $K = \{(t, P^* \cap \eta^{-1}(t)) \mid t \in N\}$. Let us first verify that this is an $\eta$-pointed $SF(\mathcal{C})$-partition $K$ of $P^*$. It is immediate that $\{P^* \cap \eta^{-1}(t)\}$ is a partition of $P^* \cap \eta^{-1}(t)$ for every $t \in N$. Moreover, we have $P^* \cap \eta^{-1}(t) \in SF(\mathcal{C})$ for every $t \in N$. Indeed, we have $P \in SF(\mathcal{C})$: it is the disjoint union of all languages involved in the $\eta$-pointed $SF(\mathcal{C})$-partition $H$ of $P$. Since $SF(\mathcal{C}) = SD(\mathcal{C})$ by Theorem 4.10, we obtain $P^* \cap \eta^{-1}(t) \in SF(\mathcal{C})$ since $P$ is a prefix code with bounded synchronization delay and $\eta^{-1}(t) \in \mathcal{C}$ (recall that $\eta$ is a $\mathcal{C}$-morphism by hypothesis). It remains to prove that $K$ satisfies (7): for every $(t, K) \in K$, we show that $(t, \rho(K)) \in Q_H^*$ and $(st, r\rho(K)) \in S$. We start with the former property (this is where we use the hypothesis that $\rho$ is nice).

FACT 9.9. For every $(t, K) \in K$, we have $(t, \rho(K)) \in Q_H^*$.

PROOF. By definition of $K$, we have $K = P^* \cap \eta^{-1}(t)$. Since $H$ is an $\eta$-pointed partition of $P$, one can check that $P^* \cap \eta^{-1}(t)$ is the (infinite) union of all H-products $(t', H)$ such that $t' = t$. Since $\rho$ is nice, it follows that there exists finitely many H-products $(t, H_1), \dots, (t, H_\ell)$ such that $\rho(K) = \rho(H_1) + \dots + \rho(H_\ell) = \rho(H_1 \cup \dots \cup H_\ell)$. Clearly, $(t, H_1 \cup \dots \cup H_\ell)$ is an H-union and it follows that $(t, \rho(K)) \in Q_H^*$, as desired.
□
It remains to show that $(st, r\rho(K)) \in S$ for every $K \in K$. We prove that for every $(t, q) \in Q_H^*$, we have $(st, rq) \in S$. In view of Fact 9.9, this yields the desired result. First, we use the hypothesis that $(s, r)$ is H-stable to prove the following fact.

**FACT 9.10.** Let $(e, H)$ be an H-product such that $(e, \rho(H)) \in Q$ is a pair of idempotents. For every $(t, q) \in Q_H^*$, we have $(ste, rq\rho(H)) = (st, rq)$.

**PROOF.** We first use the hypothesis that $(s, r)$ is H-stable to prove the following preliminary result which holds regardless of whether $(e, \rho(H))$ is a pair of idempotents or not:

$$ \text{there exists } (x, y) \in Q_H^* \text{ such that } (sxe, ry\rho(H)) = (st, rq). \qquad (9) $$

Since $(e, H)$ is an H-product, we can find elements $(t'_1, H_1), \dots, (t'_n, H_n)$ of H such that $(e, H) = (t'_1 \cdots t'_n, H_1 \cdots H_n)$. We proceed by induction on $n$. If $n=0$, then $e=1_N$ and $H = \{\varepsilon\}$. It suffices to choose $(x, y) = (t, q) \in Q_H^*$. We now assume that $n \ge 1$. By induction, we get $(x', y') \in Q_H^*$ such that $(sx't'_2 \cdots t'_n, ry'\rho(H_2 \cdots H_n)) = (st, rq)$. Since $(s, r)$ is H-stable, Property (8) yields $(x, y) \in Q_H^*$ such that $(sx', ry') = (sxt'_1, ry\rho(H_1))$. Altogether, it follows that $(sxe, ry\rho(H)) = (st, rq)$. This concludes the proof of (9).

We use (9) to conclude Fact 9.10. Indeed, since $(sxe, ry\rho(H)) = (st, rq)$ for $(x, y) \in Q_H^*$, if $(e, \rho(H))$ is a pair of multiplicative idempotents, then we obtain $(ste, rq\rho(H)) = (st, rq)$. $\square$

We are ready to prove that $(st, rq) \in S$ for every $(t, q) \in Q_H^*$. We first treat the special case when $t$ is an idempotent of $N$. Then, we reuse this special case to treat the general one. Assume that $t$ is an idempotent $e \in E(N)$. Hence, $(e, q) \in Q_H^*$ and we need to prove that $(se, rq) \in S$. By definition, there are finitely many H-products $(e, H_1), \dots, (e, H_\ell)$ such that $q = \rho(H_1) + \cdots + \rho(H_\ell)$. Consider an index $i \le \ell$. Since $(e, H_i)$ is an H-product and we know that $(t', \rho(H')) \in S$ for every $(t', H') \in H$, it follows from closure under multiplication for $S$ (recall that $S$ is SF-saturated) that $(e, \rho(H_i)) \in S$. Since $e$ is idempotent, it then follows from SF-closure that $(e, (\rho(H_i))^\omega + (\rho(H_i))^{\omega+1}) \in S$. Since this holds for all $i \le \ell$, $e$ is idempotent and $(s, r) \in S$, closure under multiplication yields,

$$ \left( \text{se}, \ r \prod_{1 \le i \le \ell} \left( (\rho(H_i))^\omega + (\rho(H_i))^{\omega+1} \right) \right) \in S. $$

Let $k = \omega(R)$. For every $i \le \ell$, we have $(e, (\rho(H_i))^\omega) = (e, \rho(H_i^k))$ and it is clear that $(e, H_i^k)$ is an H-product since this is the case for $(e, H_i)$. Therefore, since $(e, (\rho(H_i))^\omega)$ is a pair of idempotents, Fact 9.10 implies that $(st'e, rq'(\rho(H_i))^\omega) = (st', rq')$ for every $(t', q') \in Q_H^*$. This yields:

$$ \left( \text{se}, \ r \prod_{1 \le i \le \ell} \left( (\rho(H_i))^\omega + (\rho(H_i))^{\omega+1} \right) \right) = \left( \text{se}, \ r \prod_{1 \le i \le \ell} (1_R + \rho(H_i)) \right), $$

Therefore, $(se, r \prod_{1 \le i \le \ell} (1_R + \rho(H_i))) \in S$. Note that $q = \rho(H_1) + \cdots + \rho(H_\ell) \le \prod_{1 \le i \le \ell} (1_R + \rho(H_i))$. By closure under downset for $S$, we get $(se, rq) \in S$, which concludes the case when $t$ is idempotent.

We now consider an arbitrary element $(t, q) \in Q_H^*$ (i.e., $t \in N$ need not be idempotent) and show that $(st, rq) \in S$. By definition of $Q_H^*$ there are finitely many H-products $(t, H_1), \dots, (t, H_n)$ such that $q = \rho(H_1) + \cdots + \rho(H_n)$. Since every $(t', H') \in H$ satisfies $(t', \rho(H')) \in S$ by hypothesis and $S$ is closed under multiplication, we get $(t, \rho(H_i)) \in S$ for every $i \le n$. Moreover, there exists a number $k \ge 1$ such that $(t^k, (\rho(H_i))^k) \in Q_H^*$ is a pair of idempotents for each $i \le n$. In particular, $t^k$ is an idempotent of $N$. Clearly, we have $(t^k, q(\rho(H_1))^{k-1}) \in Q_H^*$. Since $t^k \in N$ is an idempotent, we obtain from the above special case that $(st^k, rq(\rho(H_1))^{k-1}) \in S$. Since we also have $(t, \rho(H_1)) \in S$, it then follows from closure under multiplication that $(st^{k+1}, rq(\rho(H_1))^k) \in S$. Finally, since $(t^k, (\rho(H_1))^k)$ is a pair of idempotents, we obtain from Fact 9.10 that $(st, rq) = (st^{k+1}, rq(\rho(H_1))^k) \in S$. This concludes the proof for the base case.
**Inductive step:** $(s, r)$ is not $H$-stable. Our hypothesis yields a pair $(t, H) \in H$ such that the following strict inclusion holds:

$$ (s, r) \cdot Q_H^* \cdot (t, \rho(H)) \subseteq (s, r) \cdot Q_H^* \qquad (10) $$

We fix this pair $(t, H) \in H$ for the remainder of the proof. First, we use induction on our second parameter in Lemma 9.8 to prove the following fact.

**FACT 9.11.** There exists an $\eta$-pointed SF($\mathbb{C}$)-partition U of $(P \setminus H)^*$ such that $(x, \rho(U)) \in Q_H^* \cap S$ for every $(x, U) \in U$.

**PROOF.** Since $P$ is a prefix code of bounded synchronization delay, Fact 4.6 implies that so is $P \setminus H$. We want to apply induction in Lemma 9.8 when $P$ is replaced by $P \setminus H$. Let $G = H \setminus \{(t, H)\}$. By hypothesis on $H$, one can check that $G$ is an $\eta$-pointed SF($\mathbb{C}$)-partition of $P \setminus H$ and that $(t', \rho(G)) \in S$ for every $(t', G) \in G$. Finally, it is immediate that $Q_G^+ \subseteq Q_H^+$ (our first induction has not increased) and $G \subseteq H$ (our second induction parameter has decreased). Hence, we may apply Lemma 9.8 when $P, H$ and $(s, r) \in S$ have been replaced by $P \setminus H, G$ and $(1_N, 1_R) \in S$. This yields an $\eta$-pointed SF($\mathbb{C}$)-partition U of $(P \setminus H)^*$ such that $(x, \rho(U)) \in Q_H^* \cap S$ for every $(x, U) \in U$. $\square$

We fix the $\eta$-pointed SF($\mathbb{C}$)-partition U of $(P \setminus H)^*$ given by Fact 9.11 for the rest of the proof. We distinguish two subcases. Since $(t, H) \in H$, one can verify from the definitions of $Q_H^+$ and $Q_H^*$ that $Q_H^* \cdot (t, \rho(H)) \subseteq Q_H^*$. We consider two subcases depending on whether this inclusion is strict.

**Subcase 1:** we have the equality $Q_H^* \cdot (t, \rho(H)) = Q_H^*$. We use the following fact, which is proved using our hypotheses and induction on our third parameter (i.e., the size of $(s, r) \cdot Q_H^*$).

**FACT 9.12.** For every $(x, U) \in U$, there exists an $\eta$-pointed SF($\mathbb{C}$)-partition $W_{x,U}$ of $P^*$ such that $(y, \rho(W)) \in Q_H^*$ and $(sxt, r\rho(UHW)) \in S$ for every $(y, W) \in W_{x,U}$.

**PROOF.** We fix $(x, U) \in U$ for the proof. By definition of $U$ in Fact 9.11, $(x, \rho(U)) \in Q_H^*$ and $(x, \rho(U)) \in S$. Hence, since $(s, r)$, $(t, \rho(H)) \in S$ by hypothesis and $S$ is closed under multiplication, we get $(sxt, r\rho(UH)) \in S$. Moreover, it is clear that we have the inclusions $(sxt, r\rho(UH)) \cdot Q_H^* \subseteq (s, r) \cdot Q_H^* \cdot (t, \rho(H)) \cdot Q_H^* \subseteq (s, r) \cdot Q_H^+$. Combined with our hypothesis in Subcase 1 (i.e., $Q_H^* \cdot (t, \rho(H)) = Q_H^+$), this yields $(sxt, r\rho(UH)) \cdot Q_H^* \subseteq (s, r) \cdot Q_H^* \cdot (t, \rho(H))$. We may then use (10) (i.e., the inclusion $(s, r) \cdot Q_H^* \cdot (t, \rho(H)) \subseteq (s, r) \cdot Q_H^*$) to get the strict inclusion $(sxt, r\rho(UH)) \cdot Q_H^* \subseteq (s, r) \cdot Q_H^*$. Consequently, induction on our third parameter (i.e., the size of $(s, r) \cdot Q_H^*$) in Lemma 9.8 (we consider the case when $(s, r) \in S$ has been replaced by $(sxt, r\rho(UH)) \in S$) yields the desired $\eta$-pointed SF($\mathbb{C}$)-partition $W_{x,U}$ of $P^*$. Note that here, our first two parameters have not increased as they only depend on $H$, which remains unchanged. $\square$

We use Fact 9.12 to finish the proof in Subcase 1. We build the following SF($\mathbb{C}$)-partition $K$ of $P^*$:

$$ K = U \cup \bigcup_{(x,U) \in U} \{(sxt, UHW) \mid (y, W) \in W_{x,U}\}. $$

Let us show that $K$ is an $\eta$-pointed SF($\mathbb{C}$)-partition of $P^*$ satisfying (7). First, observe that for every $(t', K) \in K$, we have $K \in SF(\mathbb{C})$. This is immediate by hypothesis on $U$ when $(t', K) \in U$. Otherwise, $K = UHW$ for $(x, U) \in U$ and $(y, W) \in W_{x,U}$ and $U, H, W \in SF(\mathbb{C})$. Hence, $K \in SF(\mathbb{C})$ since SF($\mathbb{C}$) is closed under concatenation.

That $K$ is an $\eta$-pointed SF($\mathbb{C}$)-partition of $P^*$ is also simple to check since $P$ is a prefix code, $H \subseteq P$ and $U, W_{x,U}$ are $\eta$-pointed partitions of $(P \setminus H)^*$ and $P^*$ respectively. Each word $w \in P^*$ admits a unique decomposition $w = w_1 \cdots w_n$ with $w_1, \dots, w_n \in P$. We partition $P^*$ by looking at the leftmost factor belonging to $H$ (if it exists).
It remains to prove that (7) holds. Consider $(t', K) \in K$, we show that $(t', \rho(K)) \in Q_H^*$ and $(st', r\rho(K)) \in S$. If $(t', K) \in U$, this is immediate by definition of $U$ in Fact 9.11. Otherwise, $(t', K) = (wty, UHW)$ with $(x, U) \in U$ and $(y, W) \in W_{x,U}$. By definition of $U$ and $W_{x,U}$, we have $(x, \rho(U))$, $(y, \rho(W)) \in Q_H^*$. Thus, $(xty, \rho(UHW)) \in Q_H^*$. Moreover, $(sxty, r\rho(UHW)) \in S$ by definition of $W_{x,U}$ in Fact 9.12. This concludes the first subcase.

**Subcase 2: we have the strict inclusion** $Q_H^* \cdot (t, \rho(H)) \subseteq Q_H^+$. Recall that our objective is to construct an $\eta$-pointed $SF(C)$-partition $K$ of $P^*$ satisfying (7). We first give an overview of the construction. Consider a word $w \in P^*$. Since $P$ is a prefix code, $w$ admits a unique decomposition as a concatenation of factors in $P$. We can look at the rightmost factor in $H \subseteq P$ to uniquely decompose $w$ in two parts (each of them possibly empty): a prefix in $((P \setminus H)^*H)^*$ and a suffix in $((P \setminus H)^*)^*$. We use induction to construct $\eta$-pointed $SF(C)$-partitions of the sets of possible prefixes and suffixes. Then, we combine them to construct an $\eta$-pointed $SF(C)$-partition of the whole set $P^*$. Actually, we already constructed a suitable $\eta$-pointed $SF(C)$-partition of the possible suffixes in $((P \setminus H)^*)^*$: $U$ (see Fact 9.11). Hence, it remains to partition the prefixes. We do so in the following lemma, which is proved using the hypothesis of Subcase 2 and induction on our first parameter.

**FACT 9.13.** *There is an $\eta$-pointed $SF(C)$-partition $V$ of $((P \setminus H)^*H)^*$ such that $(z, \rho(V)) \in Q_H^*$ and $(z, \rho(V)) \in S$ for every $V \in V$.*

**PROOF.** Let $L = (P \setminus H)^*H$. Since $P$ is a prefix code with bounded synchronization delay, so is $L$ by Fact 4.7. We want to apply induction in Lemma 9.8 where $P$ is replaced by $L$. This requires building an $\eta$-pointed $SF(C)$-partition of $L$ and proving that one induction parameter has decreased.

Let $F = \{(xt, UH) | (x, U) \in U\}$. Since $U$ is an $\eta$-pointed $SF(C)$-partition of $(P \setminus H)^*$ and $P$ is a prefix code, one can check that $F$ is an $\eta$-pointed $SF(C)$-partition of $L = (P \setminus H)^*H$. Finally, given $(y, F) \in F$, we have $(y, F) = (xt, UH)$ for $(x, U) \in U$, which means that $(y, \rho(F)) = (xt, \rho(UH)) \in S$ since $S$ is closed under multiplication. It remains to show that our induction parameters have decreased. Since $F = \{(xt, UH) | (x, U) \in U\}$ and $(x, \rho(U)) \in Q_H^*$ for every $(x, U) \in U$ (by definition of $U$ in Fact 9.11), one can verify that $Q_F^+ \subseteq Q_H^* \cdot (t, \rho(H))$. Hence, since $Q_H^* \cdot (t, \rho(H)) \subseteq Q_H^+$ by hypothesis in Subcase 2, we have $Q_F^+ \subseteq Q_H^*$. Our first induction parameter has decreased. Altogether, it follows that we may apply Lemma 9.8 in the case when $P, H$ and $(s, r) \in S$ have been replaced by $L, F$ and $(1_N, 1_R) \in S$. This yields an $\eta$-pointed $SF(C)$-partition $V$ of $L^* = ((P \setminus H)^*H)^*$ such that for every $(z, V) \in V$, $(z, \rho(V)) \in Q_F^*$ and $(z, \rho(V)) \in S$. Finally, it is clear by definition that $Q_F^* \subseteq Q_H^*$. Hence, the lemma follows. $\square$

We are ready to construct the $\eta$-pointed $SF(C)$-partition $K$ of $P^*$ and conclude the main argument. We let $K = \{(zx, VU) | (z, V) \in V$ and $(x, U) \in U\}$. It is immediate by definition and Fact 4.7 that $K$ is an $\eta$-pointed partition of $P^*$ since $P$ is a prefix code and $V, U$ are $\eta$-pointed partitions of $((P \setminus H)^*H)^*$ and $(P \setminus H)^*$ respectively (see the above discussion). Additionally, it is immediate by definition that $K$ is actually an $\eta$-pointed $SF(C)$-partition of $P^*$ (it only contains concatenations of languages in $SF(C)$). It remains to prove that $K$ satisfies (7). Let $(t', K) \in K$. By definition, there are $(z, V) \in V$ and $(x, U) \in U$ such that $(t', K) = (zx, VU)$. By definition of $U$ and $V$, we have $(x, \rho(U))(z, \rho(V)) \in Q_H^*$ and $(x, \rho(U))(z, \rho(V)) \in S$. Moreover, $(s, r) \in S$ by hypothesis. Therefore, since both $Q_H^*$ and $S$ are closed under multiplication, it follows that $(t', \rho(K)) \in Q_H^*$ and $(st', r\rho(K)) \in S$. This completes the proof of Lemma 9.8. $\square$

We combine Proposition 9.5 and Proposition 9.6 to prove Theorem 9.3 (the argument is standard).

**PROOF OF THEOREM 9.3.** Let $C$ be a finite prevariety and $\rho: 2^{A^*} \to R$ be a nice multiplicative rating map. We have to prove that $\mathcal{P}_{SF(C)}[\eta_C, \rho]$ is the least $SF$-saturated subset of $N_C \times R$ for $\eta_C$ and $\rho$. We proved in Proposition 9.5 that $\mathcal{P}_{SF(C)}[\eta_C, \rho]$ is $SF$-saturated. We need to show that it
is the least such set. Let $S \subseteq N_c \times R$ which is SF-saturated for $\eta_c$ and $\rho$. Proposition 9.6 yields an $\eta_c$-pointed SF($\mathcal{C}$)-cover of $K$ of $A^*$ such that $\mathcal{P}[\eta_c, \rho](K) \subseteq S$. Since Lemma 9.2 implies that $\mathcal{P}_{SF}(e)[\eta_c, \rho] \subseteq \mathcal{P}[\eta_c, \rho](K)$, we obtain $\mathcal{P}_{SF}(e)[\eta_c, \rho] \subseteq S$, which completes the proof. $\square$

# 10 Covering for group input classes

We now consider separation and covering for the classes SF($\mathcal{G}$) when $\mathcal{G}$ is a group prevariety. We prove that both problems are decidable when $\mathcal{G}$-separation is decidable. In this case as well, the algorithm is based on the framework introduced in Section 8: we present a generic effective characterization of optimal imprints for SF($\mathcal{G}$). Given an arbitrary group prevariety $\mathcal{G}$ and a nice multiplicative rating map $\rho: 2^{A^*} \to R$, it describes the set $\mathcal{J}_{SF}(\mathcal{G})[\rho] \subseteq R$. Moreover, this description is effective when $\mathcal{G}$-separation is decidable. As announced at the end of Section 8, the characterization actually describes a more general object than the set $\mathcal{J}_{SF}(\mathcal{G})[\rho]$. The first part of the section is devoted to defining this object. In the second part, we present and prove the characterization itself.

## 10.1 Optimal $\mathcal{G}$-identities

As explained above, characterizing the optimal imprints for SF($\mathcal{G}$) (when $\mathcal{G}$ is a group prevariety) requires working with more general objects than the ones that we actually want to compute: the sets $\mathcal{J}_{SF}(\mathcal{G})[\rho] \subseteq R$ associated to a nice multiplicative rating map $\rho: 2^{A^*} \to R$. In this case as well, we look at sets which are strongly related to the “nested optimal imprints” $\mathcal{J}_{\mathcal{G}}[\xi_{SF}(\mathcal{G})[\rho]] \subseteq 2^R$ associated to the auxiliary rating maps $\xi_{SF}(\mathcal{G})[\rho]: 2^{A^*} \to 2^R$. Yet, since we are dealing with input classes that are group prevarieties, it will not be necessary to consider the whole set: a single special element of $\mathcal{J}_{\mathcal{G}}[\xi_{SF}(\mathcal{G})[\rho]] \subseteq 2^R$ suffices. Let us first define it. The definition makes sense for all rating maps: given an arbitrary rating map $\tau: 2^{A^*} \to Q$, we identify a special element of $\mathcal{J}_{\mathcal{G}}[\tau] \subseteq Q$.

The definition is based on a simple idea: a group prevariety $\mathcal{G}$ does not contain any finite language. In particular, $\{\varepsilon\} \notin \mathcal{G}$. Hence, given a rating map $\tau: 2^{A^*} \to Q$, the optimal $\tau$-imprint for $\mathcal{G}$ on the singleton $\{\varepsilon\}$, i.e., $\mathcal{J}_{\mathcal{G}}[\{\varepsilon\}, \tau]$, is an important object. This leads to the following definition.

**Optimal $\mathcal{G}$-identities.** Let $\mathcal{G}$ be a lattice and let $\tau: 2^{A^*} \to Q$ be a rating map. A $\mathcal{G}$-identity is a language in $\mathcal{G}$ containing $\varepsilon$. An optimal $\mathcal{G}$-identity for $\tau$ is a $\mathcal{G}$-identity $L$ such that for every $\mathcal{G}$-identity $L'$, we have $\tau(L) \le \tau(L')$. In practice, we use this notion when $\mathcal{G}$ is a group prevariety, but this is not required for the definition. As expected, optimal $\mathcal{G}$-identities for $\tau$ always exist.

**LEMMA 10.1.** For any lattice $\mathcal{G}$ and rating map $\tau: 2^{A^*} \to Q$, there exists an optimal $\mathcal{G}$-identity for $\tau$.

**PROOF.** Let $U = \{\tau(L) \mid L \in \mathcal{G} \text{ and } \varepsilon \in L\} = \{\tau(L) \mid L \text{ is a } \mathcal{G}\text{-identity}\}$. Clearly, $U$ is nonempty: $\tau(A^*) \in U$ since $A^* \in \mathcal{G}$, as $\mathcal{G}$ is a lattice. For every $q \in U$, fix an arbitrary $\mathcal{G}$-identity $L_q$ such that $q = \tau(L_q)$ and let $L = \bigcap_{q \in U} L_q$. Since $\mathcal{G}$ is a lattice, we have $L \in \mathcal{G}$. Moreover, $\varepsilon \in L$ by definition. Since $L \subseteq L_q$ for all $q \in U$, it follows that $\tau(L) \le q$ for every $q \in U$. By definition of $U$, this implies that $\tau(L) \le \tau(L')$ for every $\mathcal{G}$-identity $L'$. Hence, $L$ is an optimal $\mathcal{G}$-identity for $\tau$. $\square$

We complete the definition with a second notion, which is the counterpart of optimal imprints in this context. By definition, all optimal $\mathcal{G}$-identities for $\tau$ have the same image under $\tau$. Hence, this image (in $Q$) is a canonical object for $\mathcal{G}$ and $\tau$. We write it $\mathcal{I}_{\mathcal{G}}[\tau] \in Q$. In other words, $\mathcal{I}_{\mathcal{G}}[\tau] = \tau(K)$ for every optimal $\mathcal{G}$-identity $K$ for $\tau$. We now connect this object with optimal imprints.

**LEMMA 10.2.** If $\mathcal{G}$ is a lattice and $\tau: 2^{A^*} \to Q$ is a rating map, then $\mathcal{J}_{\mathcal{G}}[\{\varepsilon\}, \tau] = \downarrow_Q\{\mathcal{I}_{\mathcal{G}}[\tau]\}$.

**PROOF.** For the left to right inclusion, let $L$ be an optimal $\mathcal{G}$-identity for $\tau$. By definition, we have $L \in \mathcal{G}$, $\varepsilon \in L$ and $\mathcal{I}_{\mathcal{G}}[\tau] = \tau(L)$. Clearly, $K = \{L\}$ is a $\mathcal{G}$-cover of $\{\varepsilon\}$. It follows that $\mathcal{J}_{\mathcal{G}}[\{\varepsilon\}, \tau] \subseteq \mathcal{J}[\tau](K) = \downarrow_Q\{\mathcal{I}_{\mathcal{G}}[\tau]\}$. Conversely, let $H$ be an optimal $\mathcal{G}$-cover of $\{\varepsilon\}$ for $\tau$. There exists $H \in H$ such that $\varepsilon \in H$. Hence, $\{H\}$ is also an optimal $\mathcal{G}$-cover of $\{\varepsilon\}$ for $\tau$ and it follows that
$\downarrow_Q\{\tau(H)\} = \mathcal{J}[\tau](\{H\}) = \mathcal{J}_G[\{\epsilon\}, \tau]$. Finally, since $H \in \mathcal{G}$ and $\epsilon \in H$, we have $\mathring{\mathcal{I}}_G[\tau] \le \tau(H)$, which yields $\downarrow_Q\{\mathring{\mathcal{I}}_G[\tau]\} \subseteq \downarrow_Q\{\tau(H)\}$. Altogether, we obtain $\downarrow_Q\{\mathring{\mathcal{I}}_G[\tau]\} \subseteq \mathcal{J}_G[\{\epsilon\}, \tau]$, as desired. $\square$

We complete the definition with a key property. When $\tau$ is a nice rating map, the element $\mathring{\mathcal{I}}_G[\tau] \in Q$ can be specified in terms of $\mathcal{G}$-separation.

**LEMMA 10.3.** Let $\mathcal{G}$ be a lattice and $\tau: 2^{A^*} \to Q$ be a nice rating map. Let $S \subseteq Q$ be the set of all elements $s \in Q$ such that $\{\epsilon\}$ is not $\mathcal{G}$-separable from $\tau_*^{-1}(s)$. Then, $\mathring{\mathcal{I}}_G[\tau] = \sum_{s \in S} s$.

**PROOF.** First, let us prove that $\sum_{s \in S} s \le \mathring{\mathcal{I}}_G[\tau]$. This boils down to proving that $s \le \mathring{\mathcal{I}}_G[\tau]$ for every $s \in S$. By definition of $S$, we know that $\{\epsilon\}$ is not $\mathcal{G}$-separable from $\tau_*^{-1}(s)$. Let $L$ be an optimal $\mathcal{G}$-identity for $\tau$. By definition, we have $L \in \mathcal{G}$, $\epsilon \in L$ and $\mathring{\mathcal{I}}_G[\tau] = \tau(L)$. Since $\{\epsilon\}$ is not $\mathcal{G}$-separable from $\tau_*^{-1}(s)$, $L \in \mathcal{G}$ cannot separate $\{\epsilon\}$ and $\tau_*^{-1}(s)$, and therefore $L \cap \tau_*^{-1}(s) \ne \emptyset$. It follows that $s \le \tau(L)$, i.e., that $s \le \mathring{\mathcal{I}}_G[\tau]$.

Conversely, we prove that $\mathring{\mathcal{I}}_G[\tau] \le \sum_{s \in S} s$. For every $q \in Q \setminus S$, we know that $\{\epsilon\}$ is $\mathcal{G}$-separable from $\tau_*^{-1}(q)$. Hence, we get $H_q \in \mathcal{G}$ such that $\epsilon \in H_q$ and $H_q \cap \tau_*^{-1}(q) = \emptyset$. Let $H = \bigcap_{q \in Q \setminus S} H_q$. Since $\mathcal{G}$ is a lattice, we have $H \in \mathcal{G}$. Moreover, $\epsilon \in H$ by definition. Therefore, $\mathring{\mathcal{I}}_G[\tau] \le \tau(H)$. Since $\tau$ is nice, there are finitely many words $w_1, \dots, w_k \in H$ such that $\tau(H) = \tau(w_1) + \dots + \tau(w_k)$. Finally, it follows from the definition of $H$ that $\tau(w_i) \notin Q \setminus S$ for every $i \le k$. In other words, we have $\tau(w_i) \in S$ for every $i \le k$ and we obtain that $\mathring{\mathcal{I}}_G[\tau] \le \tau(w_1) + \dots + \tau(w_k) \le \sum_{s \in S} s$, as desired. $\square$

In particular when $\mathcal{G}$ has decidable separation, Lemma 10.3 yields an algorithm taking a nice multiplicative rating map $\tau: 2^{A^*} \to Q$ as input and computing the element $\mathring{\mathcal{I}}_G[\tau] \in Q$.

**COROLLARY 10.4.** Let $\mathcal{G}$ be a lattice prevariety with decidable separation. Given a nice multiplicative rating map $\tau: 2^{A^*} \to Q$ as input, the element $\mathring{\mathcal{I}}_G[\tau] \in Q$ is computable.

**Application to SF(\mathcal{G})-covering.** We now explain how these notions are used in the context of SF(\mathcal{G})-covering for a group prevariety \mathcal{G}. Consider a prevariety \mathcal{D} containing \mathcal{G} and which is closed under concatenation. Intuitively, \mathcal{D} is meant to be a class that has been built from \mathcal{G} using an operator. In practice, we shall use the case when $\mathcal{D} = \text{SF}(\mathcal{G})$. The high levels ideas outlined in Section 8 suggest that given a nice multiplicative rating map $\rho: 2^{A^*} \to R$, characterizing the optimal $\rho$-imprint for \mathcal{D}, i.e., $\mathcal{J}_{\mathcal{D}}[\rho] \subseteq R$, involves working with the set $\mathcal{J}_{\mathcal{G}}[\xi_{\mathcal{D}}[\rho]] \subseteq 2^R$ defined from the auxiliary rating map $\xi_{\mathcal{D}}[\rho]: 2^{A^*} \to 2^R$. Yet, because $\mathcal{G}$ is a group prevariety and $\mathcal{D}$ is closed under concatenation, partial information on $\mathcal{J}_{\mathcal{G}}[\xi_{\mathcal{D}}[\rho]]$ suffices. As we prove below, it is enough to consider the single element $\mathring{\mathcal{I}}_G[\xi_{\mathcal{D}}[\rho]] \in 2^R$ (which belongs to $\mathcal{J}_{\mathcal{G}}[\xi_{\mathcal{D}}[\rho]]$ by Lemma 10.2).

First, observe that regardless of our hypotheses on $\mathcal{G}$ and $\mathcal{D}$, this set is directly connected to the object that we truly want to characterize: the set $\mathcal{J}_{\mathcal{D}}[\rho] \subseteq R$. Indeed, by definition, we have $\mathring{\mathcal{I}}_G[\xi_{\mathcal{D}}[\rho]] = \xi_{\mathcal{D}}[\rho](L) = \mathcal{J}_{\mathcal{D}}[L, \rho]$ where $L \in \mathcal{G}$ is an optimal $\mathcal{G}$-identity for $\xi_{\mathcal{D}}[\rho]$. Hence Fact 8.5 implies that,

$$ \mathring{\mathcal{I}}_G[\xi_{\mathcal{D}}[\rho]] = \mathcal{J}_{\mathcal{D}}[L, \rho] \subseteq \mathcal{J}_{\mathcal{D}}[A^*, \rho] = \mathcal{J}_{\mathcal{D}}[\rho]. $$

It turns out that when $\mathcal{G}$ is a group prevariety and $\mathcal{D}$ is closed under concatenation, $\mathcal{J}_{\mathcal{D}}[\rho]$ is characterized by its subset $\mathring{\mathcal{I}}_G[\xi_{\mathcal{D}}[\rho]]$. That is, one can compute the former from the latter.

**PROPOSITION 10.5.** Let $\mathcal{G}$ be a group prevariety and $\mathcal{D}$ be a prevariety closed under concatenation such that $\mathcal{G} \subseteq \mathcal{D}$. Let $\rho: 2^{A^*} \to R$ be a multiplicative rating map. Then, $\mathcal{J}_{\mathcal{D}}[\rho]$ is the least subset $S \subseteq R$ containing $\mathring{\mathcal{I}}_G[\xi_{\mathcal{D}}[\rho]]$ and satisfying the following conditions:

(1) **Trivial elements.** For every $w \in A^*$, we have $\rho(w) \in S$.

(2) **Closure under downset.** We have $\downarrow_R S = S$.

(3) **Closure under multiplication.** For every $q, r \in S$, we have $qr \in S$.
Clearly, Proposition 10.5 yields a least fixpoint procedure for computing the set $\mathcal{J}_{\mathcal{D}}[\rho]$ from the set $\mathring{\mathfrak{I}}_{\mathcal{G}}[\xi_{\mathcal{D}}[\rho]]$. This is exactly how we handle optimal imprints for $\mathcal{SF}(\mathcal{G})$ below. Rather than directly characterizing the sets $\mathcal{J}_{\mathcal{SF}(\mathcal{G})}[\rho] \subseteq \mathcal{R}$ for all nice multiplicative rating maps $\rho: 2^{\mathcal{A}^*} \to \mathcal{R}$, we instead characterize the sets $\mathring{\mathfrak{I}}_{\mathcal{G}}[\xi_{\mathcal{SF}(\mathcal{G})}[\rho]] \subseteq \mathcal{R}$, which *carry more information* by Proposition 10.5. Before we present the characterization, let us prove Proposition 10.5.

PROOF OF PROPOSITION 10.5. Let $S \subseteq \mathcal{R}$ be the least subset of $\mathcal{R}$ containing $\mathring{\mathfrak{I}}_{\mathcal{G}}[\xi_{\mathcal{D}}[\rho]]$ and satisfying the three conditions in Proposition 10.5. We first prove that $S \subseteq \mathcal{J}_{\mathcal{D}}[\rho]$. This is immediate. Indeed, as seen above, we have $\mathring{\mathfrak{I}}_{\mathcal{G}}[\xi_{\mathcal{D}}[\rho]] \subseteq \mathcal{J}_{\mathcal{D}}[\rho]$. Also, $\mathcal{J}_{\mathcal{D}}[\rho]$ contains all trivial elements: clearly, $\rho(w) \in \mathcal{J}_{\mathcal{D}}[A^*, \rho] = \mathcal{J}_{\mathcal{D}}[\rho]$ for every $w \in A^*$. Moreover, $\mathcal{J}_{\mathcal{D}}[\rho]$ is closed under downset since it is an imprint. Finally, since $\mathcal{D}$ is a prevariety, Lemma 8.7 implies that $\mathcal{J}_{\mathcal{D}}[\rho]$ is closed under multiplication. Altogether, we get $S \subseteq \mathcal{J}_{\mathcal{D}}[\rho]$ as desired.

We turn to the inclusion $\mathcal{J}_{\mathcal{D}}[\rho] \subseteq S$. We build a $\mathcal{D}$-cover $\mathbf{K}$ of $A^*$ such that $\mathcal{J}[\rho](\mathbf{K}) \subseteq S$. Since $\mathcal{J}_{\mathcal{D}}[\rho] \subseteq \mathcal{J}[\rho](\mathbf{K})$ by definition, this yields the desired result. Let $L \subseteq A^*$ be an optimal $\mathcal{G}$-identity for $\xi_{\mathcal{D}}[\rho]$. By definition, $L \in \mathcal{G}$, $\varepsilon \in L$ and $\mathring{\mathfrak{I}}_{\mathcal{G}}[\xi_{\mathcal{D}}[\rho]] = \xi_{\mathcal{D}}[\rho](L) = \mathcal{J}_{\mathcal{D}}[L, \rho]$. We now use the following lemma to build a special cover of $A^*$.

LEMMA 10.6. There exists a cover $\mathbf{U}$ of $A^*$ such that each $U \in \mathbf{U}$ satisfies $U = La_1L \cdots a_\ell L$ where $\ell \in \mathbb{N}$ and $a_1, \dots, a_\ell \in A$ (if $\ell = 0$, then $U = L$).

PROOF. With every word $w = a_1 \cdots a_\ell \in A^*$, we associate the language $U_w = La_1L \cdots a_\ell L$ (in particular, $U_\varepsilon = L$). Since $L \in \mathcal{G}$, Proposition 2.4 yields a $\mathcal{G}$-morphism $\eta: A^* \to \mathcal{G}$ recognizing $L$. By hypothesis on $\mathcal{G}$, Lemma 3.5 implies that $G$ is a group. We let $k = |G|$ and $U = \{U_w \mid w \in A^*$ and $|w| \le k\}$. All languages in $\mathbf{U}$ have the desired form. Hence, it suffices to check that $\mathbf{U}$ is a cover of $A^*$. We fix $v \in A^*$ and exhibit $U \in \mathbf{U}$ such that $v \in U$. It can be verified using a pumping argument that there exist $\ell \le k$, $a_1, \dots, a_\ell \in A$ and $v_0, \dots, v_\ell \in A^*$ such that $v = v_0a_1v_1 \cdots a_\ell v_\ell$ and $\eta(v_0a_1v_1 \cdots a_\ell v_\ell) = \eta(v_0a_1v_1 \cdots a_\ell)$ for every $i \le \ell$. Since $G$ is a group, this yields $\eta(v_i) = 1_G$ for all $i \le \ell$. Hence, since $\eta$ recognizes $L$ and $\varepsilon \in L$, we get $v_i \in L$ for every $i \le \ell$. Thus $v \in U_w$ for $w = a_1 \cdots a_\ell$. Finally, we have $U_w \in \mathbf{U}$ since $|w| = \ell \le k$. This completes the proof. $\square$

Let $\mathcal{H}$ be an optimal $\mathcal{D}$-cover of $L$ for $\rho$. By definition, we have $\mathcal{J}[\rho](\mathbf{H}) = \mathcal{J}_{\mathcal{D}}[L, \rho] = \mathring{\mathfrak{I}}_{\mathcal{G}}[\xi_{\mathcal{D}}[\rho]]$. Consider the cover $\mathbf{U}$ of $A^*$ given by Lemma 10.6. Let $U \in \mathbf{U}$. By definition $U = La_1L \cdots a_nL$ for $a_1, \dots, a_n \in A$. Let $\mathbf{K}_U = \{H_0a_1H_1 \cdots a_nH_n \mid H_0, \dots, H_n \in \mathbf{H}\}$. Since $\mathbf{H}$ is a $\mathcal{D}$-cover of $L$ and $\mathcal{D}$ is closed under concatenation, $\mathbf{K}_U$ is a $\mathcal{D}$-cover of $U$. Finally, let $\mathbf{K} = \bigcup_{U \in \mathbf{U}} \mathbf{K}_U$. Since $U$ is a cover of $A^*$ and $\mathbf{K}_U$ is a $\mathcal{D}$-cover of $U$ for every $U \in \mathbf{U}$, it is immediate that $\mathbf{K}$ is a $\mathcal{D}$-cover of $A^*$.

It remains to prove that $\mathcal{J}[\rho](\mathbf{K}) \subseteq S$. Since $S$ is closed under downset, it suffices to prove that $\rho(\mathbf{K}) \in S$ for every $\mathbf{K} \in \mathbf{K}$. By definition, there exist $a_1, \dots, a_n \in A$ and $H_0, \dots, H_n \in \mathbf{H}$ such that $\mathbf{K} = H_0a_1H_1 \cdots a_nH_n$. Hence, it suffices to prove that $\rho(H_0a_1H_1 \cdots a_nH_n) \in S$. By definition of $\mathbf{H}$, we have $\mathcal{J}[\rho](\mathbf{H}) = \mathring{\mathfrak{I}}_{\mathcal{G}}[\xi_{\mathcal{D}}[\rho]]$. Therefore, $\rho(H_i) \in \mathring{\mathfrak{I}}_{\mathcal{G}}[\xi_{\mathcal{D}}[\rho]]$ for every $i \le n$. Since $S$ contains $\mathring{\mathfrak{I}}_{\mathcal{G}}[\xi_{\mathcal{D}}[\rho]]$, this yields $\rho(H_i) \in S$ for every $i \le n$. Moreover, since $S$ contains the trivial elements, we have $\rho(a_i) \in S$ for every $i \le n$. Finally, since $S$ is closed under multiplication, we obtain $\rho(H_0a_1H_1 \cdots a_nH_n) \in S$, which completes the proof. $\square$

## 10.2 Characterization

Let us first present the characterization. Consider an arbitrary group prevariety $\mathcal{G}$ and an arbitrary multiplicative rating map $\rho: 2^{\mathcal{A}^*} \to \mathcal{R}$. We define special subsets of $\mathcal{R}$, which we call *SF-complete* for $\mathcal{G}$ and $\rho$. The definition is based on an auxiliary nice multiplicative rating map $\mu_{\rho,S}: 2^{\mathcal{A}^*} \to 2^R$, which we associate to every subset $S \subseteq \mathcal{R}$. Its rating algebra is $(2^R, \cup, \cdot)$ (the multiplication on $2^R$ is obtained by lifting the multiplication on $\mathcal{R}$ to subsets). Since we are defining a *nice* multiplicative
rating map, it suffices to specify the image of each letter $a \in A$. We let,

$$ \mu_{\rho,S}(a) = \{s\rho(a)s' \mid s, s' \in S\} \in 2^R. $$

Observe that by definition, we have $\mathring{\mathbb{G}}[\mu_{\rho,S}] \subseteq R$ for each set $S \subseteq R$. Now, consider an arbitrary subset $S \subseteq R$. We say that $S$ is SF-complete for $\mathbb{G}$ and $\rho$ when it satisfies the following properties:

(1) **Closure under downset.** $\downarrow_R S = S$.

(2) **Closure under multiplication.** For every $q, r \in S$, we have $qr \in S$.

(3) **$\mathbb{G}$-operation.** We have $\mathring{\mathbb{G}}[\mu_{\rho,S}] \subseteq S$.

(4) **SF-closure.** For every $r \in S$, we have $r^\omega + r^{\omega+1} \in S$.

**REMARK 10.7.** The definition does not explicitly require that an SF-complete subset $S \subseteq R$ for $\mathbb{G}$ and $\rho$ contains some trivial elements. Yet, this is a consequence of $\mathbb{G}$-operation. Indeed, we have $\mu_{\rho,S}(\epsilon) = \{1_R\}$ (this is the multiplicative neutral element of $2^R$). Thus, $1_R \in \mathring{\mathbb{G}}[\mu_{\rho,S}] \subseteq S$ by definition.

With this definition in hand, we can state the main theorem of this section. When $\rho$ is nice, $\mathring{\mathbb{G}}[\xi_{SF}(\mathbb{G})[\rho]]$ is the least SF-complete subset of $R$.

**THEOREM 10.8.** Let $\mathbb{G}$ be a group prevariety and $\rho: 2^{A^*} \to R$ a nice multiplicative rating map. Then, $\mathring{\mathbb{G}}[\xi_{SF}(\mathbb{G})[\rho]]$ is the least SF-complete subset of $R$ for $\mathbb{G}$ and $\rho$.

When $\mathbb{G}$-separation is decidable, Theorem 10.8 yields a least fixpoint procedure for computing $\mathring{\mathbb{G}}[\xi_{SF}(\mathbb{G})[\rho]]$ from a nice multiplicative rating map $\rho: 2^{A^*} \to R$. The computation starts from the empty set and saturates it with the operations in the definition of SF-complete subsets. It is clear that we can implement downset, multiplication and SF-closure. Moreover, we can compute $\mathring{\mathbb{G}}[\mu_{\rho,S}]$ from a set $S \subseteq R$ by Corollary 10.4 since $\mathbb{G}$-separation is decidable. Eventually, the computation reaches a fixpoint and it is straightforward to check that this set is the least SF-complete subset of $R$, i.e., $\mathring{\mathbb{G}}[\xi_{SF}(\mathbb{G})[\rho]]$ by Theorem 10.8. One can then use a second least fixpoint procedure provided by Proposition 10.5 to compute the set $\mathcal{I}_{SF}(\mathbb{G})[\rho] \subseteq R$ from $\mathring{\mathbb{G}}[\xi_{SF}(\mathbb{G})[\rho]]$.

Consequently, it follows from Proposition 8.8 that $SF(\mathbb{G})$-covering is decidable if $\mathbb{G}$-separation is decidable. As before, the result can be lifted to separation for $SF(\mathbb{G})$ using Lemma 2.2. Altogether, we obtain the following corollary.

**COROLLARY 10.9.** Let $\mathbb{G}$ be a group prevariety with decidable separation. Then, separation and covering are decidable for $SF(\mathbb{G})$.

Corollary 10.9 has three important applications: the group prevarieties MOD (the modulo languages), AMT (the alphabet modulo testable languages) and GR (all group languages). Indeed, since it is known that the three of them have decidable separation (see e.g., [34]), we obtain the decidability of covering for the classes SF(MOD), SF(AMT) and SF(GR).

We now concentrate on the proof of Theorem 10.8. In this case as well, we present two independent statements corresponding respectively to soundness and completeness. Let us start with the former. The argument is based on Proposition 9.5, which addresses soundness for the characterization of optimal imprints for $SF(C)$ when $C$ is a finite prevariety.

**PROPOSITION 10.10 (SOUNDNESS).** Let $\mathbb{G}$ be a group prevariety of group languages and $\rho: 2^{A^*} \to R$ be a multiplicative rating map. Then, $\mathring{\mathbb{G}}[\xi_{SF}(\mathbb{G})[\rho]] \subseteq R$ is SF-complete for $\mathbb{G}$ and $\rho$.

**PROOF.** For the sake of avoiding clutter, let $S = \mathring{\mathbb{G}}[\xi_{SF}(\mathbb{G})[\rho]]$. We start with a preliminary result.

**LEMMA 10.11.** There exists a finite group prevariety $\mathcal{H}$ such that $\mathcal{H} \subseteq \mathbb{G}$ and $S = \{r \in R \mid (1_G, r) \in \mathcal{P}_{SF}(\mathcal{H})[\eta_{\mathcal{H}}, \rho]\}$ where $\eta_{\mathcal{H}}: A^* \to \mathbb{G}$ is the canonical $\mathcal{H}$-morphism.
Before we prove Lemma 10.11, let us use it to complete the main argument. Note that Proposition 9.5 implies that $\mathcal{P}_{SF(\mathcal{H})}[\eta_{\mathcal{H}}, \rho] \subseteq G \times R$ is SF-saturated for $\eta_{\mathcal{H}}$ and $\rho$. We shall use this property multiple times. We show that $S$ is SF-complete for $\mathcal{G}$ and $\rho$. That $S$ is closed under downset, multiplication and SF-closure is immediate from Lemma 10.11 (more precisely, it follows from the equality $S = \{r \in R \mid (1_G, r) \in \mathcal{P}_{SF(\mathcal{H})}[\eta_{\mathcal{H}}, \rho]\}$ and the fact that $\mathcal{P}_{SF(\mathcal{H})}[\eta_{\mathcal{H}}, \rho]$ satisfies the three corresponding properties in the definition of SF-saturated sets). Hence, we concentrate on $\mathcal{G}$-operation. Given $s \in \mathcal{I}_G[\mu_{\rho,S}]$, we prove that $s \in S$. By hypothesis in Lemma 10.11, we have $\eta_{\mathcal{H}}^{-1}(1_G) \in \mathcal{H} \subseteq \mathcal{G}$. Moreover, it is clear that $\varepsilon \in \eta_{\mathcal{H}}^{-1}(1_G)$. Therefore, we obtain $\mathcal{I}_G[\mu_{\rho,S}] \subseteq \mu_{\rho,S}(\eta_{\mathcal{H}}^{-1}(1_G))$. This yields $w \in \eta_{\mathcal{H}}^{-1}(1_G)$ such that $s \in \mu_{\rho,S}(w)$. There are now two cases. First, if $w = \varepsilon$, then $\mu_{\rho,S}(\varepsilon) = \{1_R\}$ which yields $s = 1_R$. Clearly, we have $(1_G, 1_R) \in \mathcal{P}_{SF(\mathcal{H})}[\eta_{\mathcal{H}}, \rho]$ (this is a trivial element), hence we obtain $s = 1_R \in S$ by Lemma 10.11. Assume now that $w \in A^+$ and let $a_1, \dots, a_n \in A$ be the letters such that $w = a_1 \cdots a_n$. By definition of $\mu_{\rho,S}$, the fact that $s \in \mu_{\rho,S}(w)$ yields $s_1, \dots, s_n, t_1, \dots, t_n \in S$ such that $s = s_1\rho(a_1)t_1 \cdots s_n\rho(a_n)t_n$. Clearly, we have $(\eta_{\mathcal{H}}(a_i), \rho(a_i)) \in \mathcal{P}_{SF(\mathcal{H})}[\eta_{\mathcal{H}}, \rho]$ for every $i \le n$ (this is a trivial element). Also, Lemma 10.11 yields $(1_G, s_i), (1_G, t_i) \in \mathcal{P}_{SF(\mathcal{H})}[\eta_{\mathcal{H}}, \rho]$ for every $i \le n$. Altogether, since $\mathcal{P}_{SF(\mathcal{H})}[\eta_{\mathcal{H}}, \rho]$ is closed under multiplication, we get $(\eta_{\mathcal{H}}(w), s) = (\eta_{\mathcal{H}}(a_1 \cdots a_n), s) \in \mathcal{P}_{SF(\mathcal{H})}[\eta_{\mathcal{H}}, \rho]$. Finally, since $w \in \eta_{\mathcal{H}}^{-1}(1_G)$, we get $(1_G, s) \in \mathcal{P}_{SF(\mathcal{H})}[\eta_{\mathcal{H}}, \rho]$ and Lemma 10.11 yields $s \in S$, as desired.

It remains to prove Lemma 10.11. We first define $\mathcal{H}$. Let $L \in \mathcal{G}$ be an optimal $\mathcal{G}$-identity for $\xi_{SF(\mathcal{G})}[\rho]$. By definition, $\varepsilon \in L$ and $S = \mathcal{I}_G[\xi_{SF(\mathcal{G})}[\rho]] = \xi_{SF(\mathcal{G})}[\rho](L)$. Let $\mathbf{K}$ be an optimal SF($\mathcal{G}$)-cover of $L$ for $\rho$, so that $\mathcal{J}[\rho](\mathbf{K}) = \mathcal{J}_{SF(\mathcal{G})}[L, \rho] = \xi_{SF(\mathcal{G})}[\rho](L) = S$. By definition of SF($\mathcal{G}$), there exists a *finite* set of languages $\mathbf{H} \subseteq \mathcal{G}$ such that every language $K \in \mathbf{K} \subseteq \text{SF}(\mathcal{G})$ is built from the languages in $\mathbf{H}$ and the singletons $\{a\}$ for $a \in A$ using only concatenation and Boolean combinations. It follows from Proposition 3.2 that SF($\mathcal{G}$) is a prevariety. Therefore, Proposition 2.4 yields a $\mathcal{G}$-morphism $\eta : A^* \to G$ all languages in $\{L\} \cup \mathbf{H}$. Moreover, since $\mathcal{G}$ is a group prevariety, Lemma 3.5 implies that $G$ is a group. We write $\mathcal{H}$ for the class of all languages recognized by $\eta$. That is, $\mathcal{H} = \{\eta^{-1}(F) \mid F \subseteq G\}$. One can verify that $\mathcal{H}$ is a finite group prevariety such that $\mathcal{H} \subseteq \mathcal{G}$. Moreover, $\eta$ is an $\mathcal{H}$-morphism that recognizes every language in $\mathcal{H}$. Hence, $\eta$ is the canonical $\mathcal{H}$-morphism by Lemma 2.5.

It remains to prove that $S = \{r \in R \mid (1_G, r) \in \mathcal{P}_{SF(\mathcal{H})}[\eta, \rho]\}$. We start with the left to right inclusion. Let $r \in S$. By definition, $S = \mathcal{I}_G[\xi_{SF(\mathcal{G})}[\rho]]$. Hence, since $\eta^{-1}(1_G) \in \mathcal{G}$ and $\varepsilon \in \eta^{-1}(1_G)$, we have $r \in \xi_{SF(\mathcal{G})}[\rho](\eta^{-1}(1_G)) = \mathcal{J}_{SF(\mathcal{G})}[\eta^{-1}(1_G), \rho]$. Finally, since $\mathcal{H} \subseteq \mathcal{G}$, this implies by Fact 8.5 that $r \in \mathcal{J}_{SF(\mathcal{H})}[\eta^{-1}(1_G), \rho]$, which exactly says that $(1_G, r) \in \mathcal{P}_{SF(\mathcal{H})}[\eta, \rho]$, as desired. We turn to the converse inclusion. Let $r \in R$ such that $(1_G, r) \in \mathcal{P}_{SF(\mathcal{H})}[\eta, \rho]$. We show that $r \in S$. By definition $r \in \mathcal{J}_{SF(\mathcal{H})}[\eta^{-1}(1_G), \rho]$. Moreover, since $\eta$ recognizes $L$ and we have $\varepsilon \in L$, we have $\eta^{-1}(1_G) \subseteq L$. Therefore, Fact 8.5 yields $r \in \mathcal{J}_{SF(\mathcal{H})}[L, \rho]$. Moreover, it is immediate by definition of $\mathcal{H}$ that every $K \in \mathbf{K}$ belongs to SF($\mathcal{H}$). Hence, $\mathbf{K}$ is an SF($\mathcal{H}$)-cover of $L$ and we get $r \in \mathcal{J}[\rho](\mathbf{K}) = S$. This completes the proof. $\square$

We turn to completeness. The argument is based on Proposition 9.6, the direction addressing completeness for the characterization of optimal imprints for SF($\mathcal{C}$) when $\mathcal{C}$ is a *finite* prevariety.

**PROPOSITION 10.12 (COMPLETENESS).** Let $\mathcal{G}$ be a prevariety of group languages and $\rho : 2^{A^*} \to R$ be a nice multiplicative rating map. Let $S \subseteq R$ be SF-complete for $\mathcal{G}$ and $\rho$. Then, there exists a language $L \in \mathcal{G}$ such that $\varepsilon \in L$, as well as an SF($\mathcal{G}$)-cover $\mathbf{K}$ of $L$ such that $\mathcal{J}[\rho](\mathbf{K}) \subseteq S$.

**PROOF.** We start with a preliminary lemma. It is based on the hypothesis that $S$ is SF-complete for $\mathcal{G}$ and $\rho$. We need it in order to apply Proposition 9.6.

**LEMMA 10.13.** There exist a $\mathcal{G}$-morphism $\eta : A^* \to G$ and a set $S' \subseteq G \times R$ which is SF-saturated for $\eta$ and $\rho$, and such that $S = \{r \mid (1_G, r) \in S'\}$.