# A First Taste of MeSCaL, a Tool for Solving Membership Problems for Regular Languages

Thomas Place, Marc Zeitoun

► To cite this version:

Thomas Place, Marc Zeitoun. A First Taste of MeSCaL, a Tool for Solving Membership Problems for Regular Languages. Implementation and Application of Automata, CIAA'25, Sep 2025, Palerme, Italy. pp.281-298, 10.1007/978-3-032-02602-6_20. hal-05426320

HAL Id: hal-05426320

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

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_1.png" /></figure>
A first taste of MeSCaL, a tool for solving
membership problems for regular languages

Thomas Place$^{[0009-0000-2840-9586]*}$ and Marc Zeitoun$^{[0000-0003-4101-8437]*}$

Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800
F-33400, Talence, France

**Abstract.** This article is the first in a two-part series presenting a software called "MeSCaL". This program is designed to test properties of regular languages. MeSCaL allows the user to define regular languages—either via regular expressions or finite automata—and to perform queries on them. These queries determine whether the input language belongs to a specific subclass of regular languages. While MeSCaL supports at present over one hundred such classes, this paper focuses on just twenty. These membership tests present an inherent difficulty: they often require analyzing an algebraic structure derived from the input language, known as its *syntactic monoid*. Unfortunately, the size of this monoid can grow exponentially relative to the size of the minimal automaton of the language. Therefore, to handle nontrivial cases efficiently, the challenge is to highly optimize the tests performed on this monoid. In particular, naively applying algorithms from the literature is doomed to failure: careful optimizations are essential. The aim of this article is to provide an overview of some of the key optimizations implemented in MeSCaL.

**Keywords:** Regular languages · Finite monoids · Implementation · Membership problem · Separation problem · Star-free closure · First-order logic · Unary temporal logic

<footnote>* Work supported by ANR 24-CE48-1142, Project UnREAL.</footnote>
# 1 Introduction

Regular word languages play a fundamental role in theoretical computer science. They form a robust class, characterized by multiple natural definitions: they are those recognized by finite automata, described by regular expressions, defined via morphisms into finite monoids, or specified using monadic second-order logic. Among these formalisms, regular expressions and logical descriptions are syntactic in nature, which raises a key decision problem: determining how simply a given regular language can be expressed within such a syntax. For example, in logic, a first-order formula is typically regarded as simpler than a monadic second-order formula. Within first-order logic itself, formulas with fewer quantifier alternations are considered simpler than those with many. By imposing syntactic restrictions—such as limiting the number of quantifier alternations—one defines subclasses within the broader class of regular languages.

The informal question of “how simple a regular language is” can now be made precise. Let $\mathcal{C}$ be a class of regular languages—typically defined by a syntactic fragment of a descriptive formalism. The $\mathcal{C}$-membership problem asks whether a given regular language belongs to $\mathcal{C}$. Over the years, several such problems have been resolved, beginning with the class SF of star-free languages. Over an alphabet $A$, this class consists of all regular languages that can be built from singletons $\{a\}$ for $a \in A$, using only concatenation $K, L \mapsto KL$ and Boolean operations—including complement, which preserves regularity—while disallowing the Kleene star$^1$. Schützenberger [37] provided an algorithm to decide SF-membership, laying the foundation for understanding the expressiveness of logical formalisms. Indeed, McNaughton and Papert later proved [19] that SF precisely corresponds to the class of languages definable in first-order logic $FO(<)$.

Two other notable language classes are worth mentioning. The class PT of piecewise-testable languages consists of all Boolean combinations of languages of the form $A^*a_1A^* \cdots a_nA^*$. This class is exactly the set of languages definable in $\mathcal{B}\Sigma_1(<)$, that is, by first-order sentences without quantifier alternation [46]. The PT-membership problem was solved by Simon [38]. Finally, Thérien and Wilke [45] addressed the membership problem for the class of languages definable in $FO^2(<)$, i.e., by first-order sentences that use only two variable names.

Although many membership problems have been solved, few corresponding algorithms have been implemented with performance in mind. PySemigroup [20] runs several but does not emphasize efficiency. Some tools compute an algebraic abstraction of the language, its *syntactic monoid*, but only derive a few membership tests as a byproduct. This includes Semigroupe [22,24], and, to some extent AUTOMATE [4], Automata [6] and AMoRE [18]. Others, such as LANGUAGE [3] and TESTAS [48], target a limited set of membership problems and implement them efficiently on automata, avoiding to compute the syntactic monoid.

The main factor that contributes to the lack of software support is that most known membership algorithms rely on computing the aforementioned *syntactic monoid* of the input language—a structure that can be exponentially larger than

<footnote n="1">¹ We use a slightly different but equivalent definition of this original formulation of SF.</footnote>
the size of the input automaton: algorithms working directly on automata, such as the one for PT-languages [40], are rare (see also [12] for the< class of so-called locally testable languages). In fact, even over a binary alphabet, there exist deterministic automata with *n*-states whose syntactic monoids contain more than $n^n(1 - \frac{2}{\sqrt{n}})$ elements [10]. For example, over a binary alphabet and with just 7 states, some deterministic automata have syntactic monoids of size 610871—in fact the maximum possible in this case. This exponential blowup makes any membership algorithm with quadratic or higher complexity impractical.

This issue can be tackled in two ways. One approach is to restrict attention to algorithms with linear complexity in the size of the syntactic monoid, which requires careful algorithm selection. Indeed, membership tests are often framed as equations this monoid must satisfy. Verifying an equation with *k* variables over a monoid of size *m* takes $\Theta(m^k)$ time in the worst case. For example, a language belongs to the class PT if and only if, for all *s*, *t* in the syntactic monoid, the identity $(st)^\ell s = (st)^\ell = t(st)^\ell$ holds (for some *ℓ*), yielding quadratic complexity. Fortunately, in some key cases (e.g., the class PT), such equations are equivalent to properties that can be tested in *linear time* on the Cayley graph of the syntactic morphism. This is a common approach in the software mentioned above.

Regrettably, this strategy only applies in rare cases (such as the three mentioned above: languages definable in FO(<), $B\Sigma_1(<)$ and FO<fnref n="2" />(<)). For most classes, algorithms must verify equations with variables under additional constraints, often requiring costly precomputations. As a result, existing software is either limited to a small set of membership tests or performs these precomputations in a straightforward but inefficient way, making it impractical even for small automata. In this paper, we focus on a specific bottleneck precomputation that suffices for most classes we consider: the *kernel* of the syntactic morphism—a standard, naturally defined subset of the syntactic monoid.

The second approach to mitigating the combinatorial explosion of the syntactic monoid plays a central role in this article. It involves significantly *restricting* the subset of the monoid where the equation must be tested, without losing correctness. To the best of our knowledge, this strategy has not been explored in the literature.

**Contributions.** This paper is the first in a two-part series, continued in [33]. It introduces the free software MeSCaL<fnref n="2" /> [34], which implements optimized membership algorithms for several classes of regular languages. We present the most important data structures and foundational algorithms used in MeSCaL.

MeSCaL provides a shell interface where users can define languages via regular expressions or automata, visualize their minimal automata and perform membership queries. It currently supports *over a hundred* classes. MeSCaL can also, for example, enumerate all deterministic automata up to a user-defined (reasonable) size to find a language belonging to one class but not to another.

This paper presents optimizations of the membership algorithms used in MeSCaL, targeting around twenty natural classes that extend the three discussed above. These classes can be described either by regular expressions or by logical formalisms. Nine of them arise by enriching the signatures of the classes defined

<footnote n="2">² https://github.com/thomas-place/mescal</footnote>
in FO(<), $\mathcal{B}\Sigma_1(<)$ and FO$^2$(<) with additional predicates—for example, testing
the value of a position in a word modulo some integer, or counting occurrences
of a specific letter before a position modulo some integer. Additional classes,
introduced in the body of the paper, are defined using unary temporal logic.

**Organization.** Section 2 introduces the core concepts and presents data structures for their efficient implementation in MeSCaL. Section 3 defines the classes of languages considered in this paper, reviews their corresponding membership algorithms, and outlines key optimizations. Finally, Section 4 focuses on the computation of kernels. Due to space constraints, proofs are deferred to [26].

## 2 Preliminaries

**Words, regular languages, classes, membership.** We fix a *finite alphabet A*. As usual, $A^*$ is the set of all finite words over A, including the empty one $\varepsilon$. For $w \in A^*$, we write $|w|$ for the length of w. For $u, v \in A^*$, we let $uv$ be the word obtained by concatenating u and v. A *language* is a subset of $A^*$. For $K, L \subseteq A^*$, we let $KL = \{uv \mid u \in K \text{ and } v \in L\}$.

A class of languages is a set of languages. A class $\mathcal{C}$ is a Boolean algebra if $\emptyset \in \mathcal{C}$, $A^* \in \mathcal{C}$ and $\mathcal{C}$ is closed under union, intersection and complement: for all $K, L \in \mathcal{C}$, we have $K \cup L \in \mathcal{C}$, $K \cap L \in \mathcal{C}$ and $A^* \setminus L \in \mathcal{C}$. Moreover, $\mathcal{C}$ is closed under quotients when for all $L \in \mathcal{C}$ and $u \in A^*$, the languages $\{v \in A^* \mid uv \in L\}$ and $\{v \in A^* \mid vu \in L\}$ both belong to $\mathcal{C}$. A prevariety is a Boolean algebra closed under quotients and containing only regular languages. Regular languages are those that can be equivalently defined by finite automata or finite monoids.

We are interested in implementing *membership algorithms* for several classes. Given a class $\mathcal{C}$, the $\mathcal{C}$-membership problem asks whether an input regular language belongs to $\mathcal{C}$. We focus on specific classes $\mathcal{C}$, built by applying operators to input classes. An operator Op takes as input a class $\mathcal{D}$ and produces a larger class Op($\mathcal{D}$). Membership for these classes is handled via known transfer theorems, which imply that Op($\mathcal{D}$)-membership reduces to a more involved problem called $\mathcal{D}$-separation. It takes as input two regular languages $L_1, L_2 \subseteq A^*$, and asks whether there exists a language $K \in \mathcal{D}$ such that $L_1 \subseteq K$ and $L_2 \cap K = \emptyset$.

**Monoids and morphisms.** We define regular languages via monoids. A *monoid* is a set $M$ endowed with an associative multiplication $(s, t) \mapsto st$ that has an identity element $1_M$. Clearly, $A^*$ forms a monoid under concatenation, with $\varepsilon$ as the identity. In the paper, all monoids other than $A^*$ are assumed to be finite. A *morphism* is a map $\alpha : A^* \to M$, where $M$ is a monoid, such that $\alpha(\varepsilon) = 1_M$ and $\alpha(uv) = \alpha(u)\alpha(v)$ for all $u, v \in A^*$. The right (resp. left) *Cayley graph* of a morphism $\alpha : A^* \to M$ is the directed graph whose vertex set is $M$, and there is an edge $s \stackrel{a}{\to} t$ when $t = s\alpha(a)$ (resp. $t = \alpha(a)s$).

A language $L \subseteq A^*$ is *recognized* by a morphism $\alpha : A^* \to M$ when there exists a set $F \subseteq M$ such that $L = \alpha^{-1}(F)$. In this case, we also say that $M$ *itself* recognizes $L$. It is well-known that a language is regular if and only if it is recognized by a *finite* monoid. Moreover, every regular language is recognized
by a canonical morphism: its syntactic morphism. It can be computed from any
recognizer, such as an automaton or an arbitrary recognizing morphism.

## MeSCaL Data Structures 1: representation of finite monoids

We represent a morphism $\alpha : A^* \to M$ (with $M$ finite) by its Cayley graphs. This representation has the advantage that it requires $\Theta(|M||A|)$ space only, instead of $\Theta(|M|^2)$ for storing the full multiplication table. This is important, as syntactic monoids can be huge, even for simple languages. However, the drawback is that computing a product “st” is not $O(1)$ time: for instance, if we use the left Cayley graph and if $s = \alpha(a_1 \cdots a_k)$ with $a_i \in A$ for all $i \le k$, the element st is obtained from vertex t by following the path labeled $a_k \cdots a_1$.

## MeSCaL Data Structures 2: representation of elements in a monoid

Each element is represented by a product of at most $|M|$ generators $\alpha(a)$ for $a \in A$. A naive approach would take $O(|M|^2)$ space. Instead, we use a spanning tree of the right Cayley graph of $\alpha$ rooted at $1_M$, which takes $O(|M|)$ space.

**Green's relations.** Over any monoid $M$, we define preorders $\leq_{\mathcal{R}}$, $\leq_{\mathcal{L}}$, $\leq_{\mathcal{G}}$ as follows. For $q, s \in M$, we write $q \leq_{\mathcal{R}} s$ (resp. $q \leq_{\mathcal{L}} s$, resp. $q \leq_{\mathcal{G}} s$) when there exist $p, r \in M$ such that $s = qr$ (resp. $s = pq$, resp. $s = pqr$). For $\mathcal{K} \in \{\mathcal{R}, \mathcal{L}, \mathcal{G}\}$, we let $\mathcal{K}$ be the equivalence relation associated with $\leq_{\mathcal{K}}$, i.e., defined by $s \mathcal{K} t$ if and only if $s \leq_{\mathcal{K}} t$ and $t \leq_{\mathcal{K}} s$. Finally, $s \mathcal{H} t$ when $s \mathcal{R} t$ and $s \mathcal{L} t$. The equivalence relations $\mathcal{H}, \mathcal{R}, \mathcal{L}, \mathcal{G}$ are standard and called the *Green's relations*. Sometimes, we consider a submonoid $N$ of a monoid $M$. In this case, for $s, t \in N$ and $\mathcal{K} \in \{\mathcal{H}, \mathcal{R}, \mathcal{L}, \mathcal{G}\}$, the notation $s \mathcal{K} t$ is ambiguous. In general, the relation $\mathcal{K}$ over $N$ is not the restriction to $N \times N$ of the relation $\mathcal{K}$ over $M$. When such an ambiguity arises, we write $\mathcal{K}_N$ and $\mathcal{K}_M$ to distinguish both relations.

## MeSCaL Data Structures 3: computing Green's relations

From the Cayley graphs of a surjective morphism $\alpha : A^* \to M$, we can compute
the Green's relations $\mathcal{R}, \mathcal{L}$ and $\mathcal{G}$ on $M$ in $O(|M||A|)$ time.

Indeed, by definition, two elements of $M$ are $\mathcal{R}$- (resp. $\mathcal{L}$-) equivalent if and only if they lie in the same strongly connected component in the right (resp. left) Cayley graph. Tarjan's algorithm [42] identifies these components in $O(|M||A|)$ time. The relation $\mathcal{G}$ is computed similarly in $O(|M||A|)$ time, using a merging of both Cayley graphs. Finally, to obtain $\mathcal{H}$, we sort each $\mathcal{J}$-class according to the $\mathcal{R}$- and $\mathcal{L}$-class of each element, so that $\mathcal{H}$-equivalent elements occur consecutively. This takes $O(|M||A| \log(|M|))$ time to compute $\mathcal{H}$.

**Special elements.** Let $M$ be a *finite* monoid. An *idempotent* in $M$ is an element $e \in M$ such that $ee = e$. We write $E(M)$ for the set of idempotents of $M$. It is folklore that for every *finite* monoid $M$, there is a natural number $\omega(M) \ge 1$ (written $\omega$ when $M$ is understood) such that $s^\omega$ is idempotent for all $s \in M$. An element is *regular* when it is $\mathcal{J}$-equivalent to some idempotent. It is standard that in this case, it is also $\mathcal{R}$- (resp. $\mathcal{L}$-) equivalent to some idempotent. Finally, we say that a $\mathcal{K}$-class is *regular* (for $\mathcal{K} \in \{\mathcal{H}, \mathcal{R}, \mathcal{L}, \mathcal{G}\}$) if it contains an idempotent.
# 3 Operators and classes

We now introduce the classes studied in this paper, present the challenges of implementing their membership algorithms, and outline the strategy used in MeSCaL. These classes are built via closure operators, which we first describe.

## 3.1 Closure operators

**Star-free closure.** Let $\mathcal{C}$ be a prevariety. Its star-free closure, denoted $\text{SF}(\mathcal{C})$, is the least class containing $\mathcal{C}$ and closed under Boolean operations (if $K, L \in \mathcal{C}$, then $K \cup L \in \mathcal{C}$ and $A^* \setminus K \in \text{SF}(\mathcal{C})$) and marked concatenation (if $K, L \in \mathcal{C}$ and $a \in A$, then $KaL \stackrel{\text{def}}{=} K\{a\}L \in \text{SF}(\mathcal{C})$).

Just as SF consists in languages definable in first-order logic $\text{FO}(<)$ [19], the languages of $\text{SF}(\mathcal{C})$ are captured by a variant of this logic, denoted $\text{FO}(\mathbb{I}_{\mathcal{C}})$, whose signature depends on the class $\mathcal{C}$ [27]. The definition of $\mathbb{I}_{\mathcal{C}}$ is natural: each language $L$ in $\mathcal{C}$ gives rise to a binary predicate $I_L$, where $x I_L y$ holds when $x < y$ and the infix strictly between $x$ and $y$ belongs to $L$. Star-free languages also have a well-known characterization in temporal logic [11]: they are exactly those definable in pure-future linear-time temporal logic LTL, and equivalently in full linear-time temporal logic. These characterizations extend to $\text{SF}(\mathcal{C})$ as well [32].

**Boolean polynomial closure.** Let $\mathcal{C}$ be a prevariety. Its polynomial closure $\text{Pol}(\mathcal{C})$ is the least class containing $\mathcal{C}$ closed under union and marked concatenation: if $K, L \in \text{Pol}(\mathcal{C})$, then $K \cup L \in \text{Pol}(\mathcal{C})$ and $KaL \in \text{Pol}(\mathcal{C})$ for $a \in A$. In general, $\text{Pol}(\mathcal{C})$ is not closed under complement. This motivates the definition of BPol($\mathcal{C}$) as the least Boolean algebra containing $\text{Pol}(\mathcal{C})$.

The class PT = BPol($\{\emptyset, A^*\}$) of piecewise testable languages corresponds to the class of languages definable in $\mathcal{B}\Sigma_1(<)$, i.e., in the quantifier-alternation free fragment of $\text{FO}(<)$ [46]. As for the full class of star-free languages, this correspondence extends to classes of the form BPol($\mathcal{C}$). Indeed, when $\mathcal{C}$ is a prevariety, the classes BPol($\mathcal{C}$) and $\mathcal{B}\Sigma_1(\mathbb{I}_{\mathcal{C}})$ coincide [27].

**Temporal closures.** Consider the class $\text{FO}^2(<)$ mentioned in the introduction. It consists of languages definable in $\text{FO}(<)$ using two variable names. Just as $\text{FO}(<)$ corresponds to LTL, the class $\text{FO}^2(<)$ corresponds to unary temporal logic TL [7]. We introduce three operators from [29] inspired by temporal logic: TL($\mathcal{C}$), FL($\mathcal{C}$) and PL($\mathcal{C}$). Let $\mathcal{C}$ be a prevariety. Formulas in $\text{TL}[\mathcal{C}]$ are defined by the grammar $\varphi := a \mid \varphi \lor \varphi \mid \varphi \land \varphi \mid \neg\varphi \mid F_L \varphi \mid P_L \varphi$ where $a \in A$ and $L \in \mathcal{C}$. Formulas in $\text{FL}[\mathcal{C}]$ (resp. in $\text{PL}[\mathcal{C}]$) are those that do not use $P_L$ (resp. $F_L$).

A TL[$\mathcal{C}$]-formula is evaluated on a pair $(w, i)$ where $w = a_1 \cdots a_n$ is a word ($a_i \in A$) and $i \in \{0, 1, \dots, |w| + 1\}$ is a position in $w$. We view $0$ and $|w| + 1$ as dummy positions, which carry no letter. In contrast, if $1 \le i \le |w|$, position $i$ carries letter $a_i$. For two positions $i < j$, we write $w(i, j) = a_{i+1} \cdots a_{j-1}$. We define by induction what it means for the pair $(w, i)$ to satisfy $\varphi$, denoted $w, i \models \varphi$. First, for $a \in A$, we have $w, i \models a$ if position $i$ carries an “a”. The semantics of the Boolean connectives $\neg$, $\land$, $\lor$ is standard. Finally, let $L \in \mathcal{C}$. We have $w, i \models F_L \psi$ if there exists a position $j > i$ such that $w(i, j) \in L$ and $w, j \models \psi$. Similarly, $w, i \models P_L \psi$ holds if there exists $j < i$ such that $w(j, i) \in L$ and $w, j \models \psi$.
For a formula $\varphi \in \text{TL}[C]$, we define $L_{\min}(\varphi) = \{w \in A^* | w, 0 \models \varphi\}$ and $L_{\max}(\varphi) = \{w \in A^* | w, |w| + 1 \models \varphi\}$. We are ready to define our three classes:

- $\text{TL}(C)$ is the class consisting of all languages $L_{\min}(\varphi)$ with $\varphi \in \text{TL}[C]$.

- $\text{FL}(C)$ is the class consisting of all languages $L_{\min}(\varphi)$ with $\varphi \in \text{FL}[C]$.

- $\text{PL}(C)$ is the class consisting of all languages $L_{\max}(\varphi)$ with $\varphi \in \text{PL}[C]$.

In particular, for $C = \{\emptyset, A^*\}$ the standard unary temporal logic TL defines exactly $\text{TL}(\{\emptyset, A^*\})$. Moreover, as for the two preceding operators, we have a correspondence result: $\text{TL}(C)$ defines the same languages as $\text{FO}^2(\mathbb{I}_C)$. Classes of the form $\text{TL}(C)$ were first investigated for specific input classes $C$, sometimes under the form $\text{FO}^2(\mathbb{I}_C)$, see [5] and [15,14,13]. Finally, a generic membership algorithm for $\text{TL}(C)$, based on a reduction to $C$-separation, was given in [31].

## 3.2 Main input classes: group prevarieties

A monoid $G$ is a group if every element $g \in G$ has an inverse $g^{-1}$, i.e., such that $gg^{-1} = g^{-1}g = 1_G$. A group language is a language recognized by a finite group.

We consider input classes that are group prevarieties, i.e., prevarieties consisting only of group languages. We are interested in four main group prevarieties:

- The prevariety GR of all group languages.

- The prevariety AMT of alphabet modulo testable languages consists of all finite Boolean combinations of languages $\{w \in A^* | \#_a w \equiv r \pmod q\}$, where $\#_a w$ is the number of occurrences of "a" in $w$. It is standard that AMT consists of all regular languages recognized by a finite commutative group.

- The prevariety MOD of modulo languages consists of all finite unions of languages of the form $(A^q)^* A^r = \{w \in A^* | |w| \equiv r \pmod q\}$ for $0 \le r < q$.

- Finally, the prevariety ST = $\{\emptyset, A^*\}$ is the trivial class.

**Remark 1.** Considering group prevarieties as input of our operators is natural. Indeed, languages definable in first-order logic $\text{FO}(<)$ are characterized by the fact that their syntactic monoid is group-free (i.e., it contains no nontrivial group).

**Remark 2.** Some classes we tackle in MeSCaL have nice interpretations in terms of first-order logic. Indeed, as discussed in Section 3.1, the classes $\text{SF}(C)$, $\text{BPol}(C)$ and $\text{TL}(C)$ correspond to fragments of first order logic for a suitable signature $\mathbb{I}_C$ (namely, to $\text{FO}(\mathbb{I}_C)$, $\mathcal{B}\Sigma_1(\mathbb{I}_C)$ and $\text{FO}^2(\mathbb{I}_C)$, respectively). In addition to the letter predicates $a(x), b(x), \dots$ which are always present, and the linear order $<$:

- The signature $\mathbb{I}_{\text{MOD}}$ contains all modular predicates. A modular predicate is of the form "$x \equiv r \pmod q$", where $q, r$ are integers such that $0 \le r < q$.

- The signature $\mathbb{I}_{\text{AMT}}$ consists of all "letter modular predicates", of the form "$\#_a(x) \equiv r \pmod q$", where $q, r$ are integers such that $0 \le r < q$ and $\#_a(x)$ denotes the number of "a"s that occur before position $x$, for $a \in A$.

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

### MeSCaL features

We are ready to list the 20 classes discussed in this paper. We present optimized algorithms implemented in MeSCaL for deciding membership in classes of the form $\text{Op}(C)$, where "Op()" is one of the five operators $\text{SF()}$, $\text{BPol()}$, $\text{TL()}$, $\text{FL()}$ and $\text{PL()}$, and $C$ is one of the four classes GR, AMT, MOD and ST.
### 3.3 Characterizations and membership

The membership tests implemented in MeSCaL for the aforementioned classes are based on generic characterizations of the operators SF, BPol, TL, FL and PL, which are specific to input classes $\mathcal{G}$ that are group prevarieties. For each operator Op, they imply that $\text{Op}(\mathcal{G})$-membership reduces to $\mathcal{G}$-separation. We present these characterizations and discuss the challenges involved in implementing them.

**Kernels.** Most characterizations are based on a specific object: $\mathcal{G}$-kernels. Let $\mathcal{G}$ be a group prevariety and $\alpha: A^* \to M$ be a morphism. The $\mathcal{G}$-kernel of $\alpha$ is the subset of $M$ that consists of all elements $s \in M$ such that $\{\varepsilon\}$ is not $\mathcal{G}$-separable from $\alpha^{-1}(s)$. In other words, every group language of $\mathcal{G}$ that contains $\{\varepsilon\}$ must intersect $\alpha^{-1}(s)$. The computation of the GR-kernel was, for many years, a central question in semigroup theory, linked to a conjecture by Rhodes [9], eventually solved by Ash [1]. The following result is standard (see [29, Fact 5.5]).

**Lemma 3.** Let $\mathcal{G}$ be a group prevariety and $\alpha: A^* \to M$ be a surjective morphism. Then, the $\mathcal{G}$-kernel of $\alpha$ is a submonoid of $M$ containing $E(M)$.

When their input is a group prevariety $\mathcal{G}$, the four operators SF, TL, FL and PL are characterized in terms of $\mathcal{G}$-kernels. Let us present these characterizations. For each of the Green's relations $K \in \{J, \mathcal{R}, \mathcal{L}, \mathcal{H}\}$, a monoid is said to be $K$-trivial if all of its $K$-classes are singletons. In particular, $\mathcal{H}$-trivial monoids are known as *aperiodic* monoids. The following is proved in [32, Corollary 5.13].

**Theorem 4.** Let $\mathcal{G}$ be a group prevariety. A regular language belongs to $\text{SF}(\mathcal{G})$ if and only if the $\mathcal{G}$-kernel of its syntactic morphism is aperiodic.

We now turn to the temporal closures. The characterization of $C \mapsto \text{TL}(C)$ relies on the class of monoids DA, typically defined by an equation: a finite monoid $M$ belongs to DA if, for all $s, t \in M$, we have $(st)^\omega s(st)^\omega = (st)^\omega$. The following is proved in [29, Theorem 10.1] and [31, Theorems 37 and 38].

**Theorem 5.** Let $\mathcal{G}$ be a group prevariety and $L$ be a regular language.

- $L \in \text{PL}(\mathcal{G})$ if and only if the $\mathcal{G}$-kernel of its syntactic morphism is $\mathcal{R}$-trivial.

- $L \in \text{FL}(\mathcal{G})$ if and only if the $\mathcal{G}$-kernel of its syntactic morphism is $\mathcal{L}$-trivial.

- $L \in \text{TL}(\mathcal{G})$ if and only if the $\mathcal{G}$-kernel of its syntactic morphism is in DA.

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

#### MeSCaL Optimization 1: regular elements suffice

In view of Theorems 4 and 5, we need to compute $\mathcal{G}$-kernels and check whether they are $\mathcal{K}$-trivial for $\mathcal{K} \in \{\mathcal{H}, \mathcal{R}, \mathcal{L}\}$. A simple but useful observation [23, Proposition 2.26], used for instance in [22], states that a monoid is $\mathcal{K}$-trivial if and only if all its regular $\mathcal{K}$-classes are trivial. This result plays a crucial role in our implementation: focusing only on the regular elements in the $\mathcal{G}$-kernel allows for a much more efficient computation than handling the full structure.

Similarly, in order to test whether the $\mathcal{G}$-kernel belongs to DA, it suffices to look at its regular elements. Indeed, it is known that a monoid belongs to DA if and only if all its regular elements are idempotent [23, Proposition 4.29].
## MeSCaL Data Structures 4: kernels and their Green's relations

According to Optimization 1, deciding membership tests for the above four operators when the input class is a group prevariety $\mathcal{G}$ presents two challenges.

- First, we must be able to represent $\mathcal{G}$-kernels efficiently. So far, we can only represent by a Cayley graph an A-generated monoid, but not a submonoid.

- Second, we have to compute $\mathcal{G}$-kernels (or at least their restriction to regular elements) and their Green's relations. Again, the difficulty is that we do not have in hand the generators of this $\mathcal{G}$-kernel.

**The BPol operator.** There exists a generic characterization of the classes BPol($\mathcal{G}$) when $\mathcal{G}$ is a group prevariety. However, it depends on more information than just the $\mathcal{G}$-kernel of its syntactic morphism. To present it, we need an additional notion: C-pairs. Let $\mathcal{C}$ be a class of languages and $\alpha: A^* \to M$ be a morphism. We say that $(s, t) \in M^2$ is a C-pair (for $\alpha$) when $\alpha^{-1}(s)$ is not C-separable from $\alpha^{-1}(t)$. We rely on the following characterization from [28].

**Theorem 6.** Let $\mathcal{G}$ be a group prevariety. Then, a regular language belongs to BPol($\mathcal{G}$) if and only if its syntactic morphism $\alpha: A^* \to M$ satisfies:

$$ (qr)^\omega st(st)^\omega = (qr)^\omega qt(st)^\omega \text{ for all } q, r, s, t \in M \text{ where } (q, s) \text{ is a } \mathcal{G}\text{-pair.} \quad (1) $$

*Remark 7.* In two cases, when $\mathcal{G} = \text{ST}$ or $\mathcal{G} = \text{GR}$, Theorem 6 is not needed. Firstly, BPol(ST) is the class of piecewise testable languages and Simon's original characterization [38] can be used: the syntactic monoid must be $\mathcal{J}$-trivial. Secondly, the class BPol(GR) admits an alternate characterization based on Green's relations [9,21]: a language belongs to BPol(GR) if every regular $\mathcal{R}$-class and every regular $\mathcal{L}$-class in its syntactic monoid contains exactly one idempotent.

## MeSCaL Optimization 2: bypassing the brute force computation

The naive BPol($\mathcal{G}$)-membership algorithm derived from Theorem 6 is inefficient: testing (1) requires a loop ranging over four variables. Instead, we rely on the following Corollary of Theorem 5. We say that a pair $(s, t) \in M^2$ is a C-cancel for $\alpha$ if $\alpha^{-1}(s)\alpha^{-1}(t)$ is not C-separable from $\{\varepsilon\}$. Although this notion is well-defined for any class $\mathcal{C}$, we use it when $\mathcal{C}$ is a group prevariety.

**Corollary 8.** Let $\mathcal{G}$ be a group prevariety. Then, a regular language belongs to BPol($\mathcal{G}$) if and only if its syntactic morphism $\alpha: A^* \to M$ satisfies:

$$ ef = qt \text{ for all } e, f \in E(M) \text{ and } \mathcal{G}\text{-cancel } (q, t) \text{ where } e \in \mathcal{R} \text{ and } t \in \mathcal{L} \text{ f.} \quad (2) $$

Corollary 8 offers two main advantages. First, it narrows the range of two variables by requiring $e$ and $f$ to be idempotent, which are often much fewer than the set of all elements. Second, once $e$ and $f$ are fixed, $q$ (resp. $t$) is constrained to the $\mathcal{R}$-class of $q$ (resp. $\mathcal{L}$-class of $f$), significantly reducing the search space in practice, and improving the running time.

On the other hand, we have to determine whether $(q, t)$ is a $\mathcal{G}$-cancel. This is linked to the computation of $\mathcal{G}$-kernels, addressed in the next section. More precisely, we use Proposition 11 to carry out this test.
# 4 Computing kernels

Let us recapitulate our objectives in view of Theorem 5 and Corollary 8. Fix a morphism $\alpha : A^* \to M$ in this section. We need to design algorithms for computing the following information for the three group prevarieties $G \in \{\text{MOD}, \text{AMT}, \text{GR}\}$:

- The $G$-kernel of $\alpha$ restricted to *regular elements*, as well as its Green's relations.

- The $G$-cancels $(q, t) \in M^2$ of $\alpha$ where $q, t$ are *regular elements*.

*Remark 9.* For $G = \text{ST}$, these computations are trivial. Indeed, since $\text{ST} = \{\emptyset, A^*\}$, two nonempty languages are not ST-separable. Since the syntactic morphism is surjective, the ST-kernel of a syntactic morphism $\alpha : A^* \to M$ is the whole syntactic monoid $M$, and the set of ST-cancels for $\alpha$ is $M \times M$.

We must adapt known separation algorithms to compute $G$-kernels and $G$-cancels. Indeed, the original algorithms can be slow for arbitrary input languages. For instance, AMT-separation is co-NP-complete [30]. Fortunately, we are only interested in *regular elements*. The first part of this section (Subsection 4.1) is devoted to explaining how this assumption can be exploited to obtain significantly more efficient procedures. Then, in dedicated subsections 4.2, 4.3 and 4.4, we describe how to compute kernels and cancels for MOD, AMT and GR. Finally in Section 4.5, we discuss the computation of their Green's relations.

## 4.1 Separation and regular elements for MOD, AMT and GR

Our approach relies on nondeterministic finite automata (NFAs) in a crucial way. An NFA is a pair $A = (Q, \delta)$ with $Q$ a finite set of states and $\delta \subseteq Q \times A \times Q$ a set of transitions. Let $w \in A^*$ and $q, r \in Q$. There is a run labeled by $w$ from $q$ to $r$ if either $w = \varepsilon$ and $q = r$, or $w = a_1 \cdots a_n$ for $n \ge 1$ and $a_1, \dots, a_n \in A$, and there are $q_0, \dots, q_n \in Q$ such that $q_0 = q, q_n = r$ and $(q_{i-1}, a_i, q_i) \in \delta$ for $1 \le i \le n$. For $q, r \in Q$, let $L(A, q, r)$ be the language of words labeling a run from $q$ to $r$.

When dealing with $G$-cancels, we will consider *mirrors* of NFAs. For an NFA $A = (Q, \delta)$, we define a transition relation $\gamma = \{(q, a, r) \in Q \times A \times Q \mid (r, a, q) \in \delta\}$. The *mirror* of $A$ is then the NFA $\text{mir}(A) = (Q, \gamma)$.

We come back to kernels and cancels. With each morphism $\alpha : A^* \to M$, we associate two NFAs $A_R[\alpha] = (M, \delta_R)$ and $A_L[\alpha] = (M, \delta_L)$ with the transitions, $\delta_R = \{(s, a, t) \mid s \notin \mathcal{R} \text{ and } s\alpha(a) = t\}$ and $\delta_L = \{(s, a, t) \mid s \notin \mathcal{L} \text{ and } \alpha(a)s = t\}$.

Observe that $A_R[\alpha]$ (resp. $A_L[\alpha]$) is the restriction of the right (resp. left) Cayley graph of $\alpha$ to its strongly connected components: the $\mathcal{R}$-classes (resp. $\mathcal{L}$-classes). In particular, $A_R[\alpha]$ and $A_L[\alpha]$ are *not* connected in general: every run stays within a single strongly connected component of the corresponding Cayley graph.

We turn to the computation of the regular elements of $G$-kernels. The main ingredient for speeding up this process is the following proposition.

**Proposition 10.** Let $G$ be a group prevariety and $\alpha : A^* \to M$ be a surjective morphism. Let $e \in E(M)$ and $s \in M$ such that $e \notin \mathcal{R} s$. Then, $s$ belongs to the $G$-kernel of $\alpha$ if and only if $\{e\}$ is not $G$-separable from $L(A_R[\alpha], e, s)$.
### MeSCaL Optimization 3: computing kernels

Proposition 10 yields two optimizations, speeding up the algorithms in practice.

- First, it implies that to decide if a regular element $s \in M$ is in the $G$-kernel of $\alpha$, it suffices to consider a small NFA compared to the whole right Cayley graph of $\alpha$: the strongly connected component of $A_R[\alpha]$ of state $s$.

- Second, this NFA forms a single strongly connected component, a property that will be crucial for enhancing our $G$-separation algorithms.

We turn to the computation of $G$-cancels required by Corollary 8.

**Proposition 11.** Let $G$ be a group prevariety and $\alpha: A^* \to M$ be a morphism. Let $e, f \in E(M)$ and $q, t \in M$ such that $e \in \mathbb{R}q$ and $t \in \mathcal{L}f$. Then, $(q, t)$ is a $G$-cancel if and only if $L(A_R[\alpha], e, q)$ is not $G$-separable from $L(mir(A_L[\alpha]), f, t)$.

### MeSCaL Optimization 4: computing cancels

In this case as well, Proposition 11 implies that in order to decide whether a pair of regular elements $(q, t) \in M^2$ is a $G$-cancel, it suffices to separate two small NFAs corresponding to the $\mathbb{R}$-class of $q$ and the $\mathcal{L}$-class of $t$. Again, these NFAs both consist of a single strongly connected component.

## 4.2 Computing GR-kernels and GR-cancels

Both definitions of the $G$-kernel and of $G$-cancels are based on $G$-separation. For $G = \text{GR}$, the decidability of GR-separation is a difficult result due to Ash [1]. Alternative proofs were found [25,35,2]. We follow the recent approach from [30]. It relies on a construction on automata that we introduce first.

Let $A = (Q, \delta)$ be an NFA. We associate with it an NFA $\langle A \rangle$ with transitions labeled by an extended alphabet $\tilde{A}$. For each $a \in A$, we create a fresh letter $a^{-1}$ and define $A^{-1} = \{a^{-1} | a \in A\}$. We let $\tilde{A}$ be the disjoint union $\tilde{A} = A \cup A^{-1}$. We define $\langle A \rangle = (Q, \langle \delta \rangle)$, where $\langle \delta \rangle$ is the following extended set of transitions:

$$ \langle \delta \rangle = \delta \cup \{(r, a^{-1}, q) \mid (q, a, r) \in \delta \text{ and } L(A, r, q) \neq \emptyset\}. $$

In other words, for each transition $(q, a, r) \in \delta$ inside a strongly connected component of $A$, we add to $\langle \delta \rangle$ the transition $(r, a^{-1}, q)$ in the opposite direction.

By definition, all languages $L(\langle A \rangle, q, r)$ are over the extended alphabet $\tilde{A}$. We use a standard rewriting rule on words in $\tilde{A}^*$. Given $w, w' \in \tilde{A}^*$, we write $w \to w'$ if there exist $x, y \in \tilde{A}^*$ and $a \in A$ such that either $w = xaa^{-1}y$ or $w = xa^{-1}ay$, and $w' = xy$. The reflexive transitive closure of “$\to$” is denoted by “$\to^*$”. Finally, for every language $K \subseteq \tilde{A}^*$, we let,

$$ \lfloor K \rfloor = \{w \in \tilde{A}^* \mid \text{there exists } u \in K \text{ such that } u \xrightarrow{*} w\}. $$

The following result is proved in [30].

**Theorem 12.** Let $A = (Q, \delta)$ be an NFA and $q_1, r_1, q_2, r_2 \in Q$. Then, $L(A, q_1, r_1)$ is not GR-separable from $L(A, q_2, r_2)$ iff $\lfloor L(\langle A \rangle, q_1, r_1) \rfloor \cap \lfloor L(\langle A \rangle, q_2, r_2) \rfloor \neq \emptyset$.
The criterion provided by Theorem 12 is decidable. In [30], the intersection is checked by computing an NFA (with $\epsilon$-transitions) recognizing $\lfloor L(\langle \mathcal{A} \rangle, q_1, r_1) \rfloor$ and $\lfloor L(\langle \mathcal{A} \rangle, q_2, r_2) \rfloor$. This is costly: $\epsilon$-transitions are *recursively* added between states connected by a word $aa^{-1}$ or $a^{-1}a$. A rough analysis yields a $|Q|^3$ time complexity. Fortunately, we can do better for the *specific* NFAs that we consider.

Indeed, we only use the NFAs $\mathcal{A}_L[\alpha]$ and $\mathcal{A}_R[\alpha]$ via Propositions 10 and 11. Thanks to Optimization 1, it suffices to compute the *regular* elements of the GR-kernel of $\alpha$. By Proposition 10, $s$ belongs to the GR-kernel of $\alpha$ if and only if $\{\epsilon\}$ is not GR-separable from $L(\mathcal{A}_R[\alpha], e, s)$, where $e$ is any idempotent $\mathcal{R}$-equivalent to $s$. Since $e$ and $s$ lie in the same strongly connected component $\mathcal{A}_e$ of $\mathcal{A}_R[\alpha]$, we have $L(\mathcal{A}_R[\alpha], e, s) = L(\mathcal{A}_e, e, s)$. Hence, in view of Theorem 12, we have to test whether $\epsilon$ belongs to $\lfloor L(\langle \mathcal{A}_e \rangle, e, s) \rfloor$. Since $\mathcal{A}_e$ is strongly connected, one can verify that $\lfloor L(\langle \mathcal{A}_e \rangle, e, s) \rfloor$ is recognized by the *Stallings' folding* of $\mathcal{A}_e$ [39], obtained by repeatedly merging states with identical forward or backward transitions: we identify any two states $r, s$ whenever there exist transitions $r \xrightarrow{a} t$ and $s \xrightarrow{a} t$, or transitions $t \xrightarrow{a} r$ and $t \xrightarrow{a} s$. The folding can be computed using the union-find algorithm [43], yielding an $O(|M||A| \cdot \text{Ackinv}(|M|))$ upper bound (see also [47]), where Ackinv is the inverse Ackermann function. The same kind of optimization is used in MeSCAL for computing GR-cancels.

## 4.3 Computing AMT-kernels and AMT-cancels

We first recall an AMT-separation procedure from [30]. It relies on the extended alphabet $\tilde{A}$ and the NFA construction $\mathcal{A} \mapsto \langle \mathcal{A} \rangle$ introduced above.

We start with a preliminary definition. Let $n = |A|$ and let $A = \{a_1, \dots, a_n\}$. We define a map $\zeta : \tilde{A}^* \to \mathbb{Z}^n$ as follows:

$$ \zeta(w) = (|w|_{a_1} - |w|_{a_1^{-1}}, \dots, |w|_{a_n} - |w|_{a_n^{-1}}). $$

We extend $\zeta$ to languages by letting $\zeta(K) = \{\zeta(w) \mid w \in K\}$ for $K \subseteq A^*$. Our starting point is the following result [30], analogous to Theorem 12.

**Theorem 13.** Let $\mathcal{A} = (Q, \delta)$ be an NFA and $q_1, r_1, q_2, r_2 \in Q$. Then, $L(\mathcal{A}, q_1, r_1)$ is *not* AMT-separable from $L(\mathcal{A}, q_2, r_2)$ iff $\zeta(L(\langle \mathcal{A} \rangle, q_1, r_1)) \cap \zeta(L(\langle \mathcal{A} \rangle, q_2, r_2)) \neq \emptyset$.

In [30], it is argued that verifying the criterion provided by Theorem 13 amounts to checking whether an existential Presburger formula is true. Although such a formula can be constructed in polynomial time [8], the existential fragment of Presburger logic is NP-complete [36]. Unfortunately, this lower bound also applies to deciding AMT-separation, which is known to be co-NP-complete [30]. As a result, we avoid relying on the generic AMT-separation algorithm. Instead, we adopt an efficient, purpose-specific approach tailored to our needs. It applies to the computation of both AMT-kernels and AMT-cancels. We explain it for kernels.

According to Optimization 1, we only need to compute *regular* elements of the AMT-kernel of $\alpha: A^* \to M$. Let $s$ be such an element. Proposition 10 states that $s$ belongs to the AMT-kernel of $\alpha$ if and only if $\{\epsilon\}$ is not AMT-separable from $L(\mathcal{A}_R[\alpha], e, s)$, where $e$ is any idempotent $\mathcal{R}$-equivalent to $s$. By Theorem 13, this amounts to testing that $\emptyset \notin \zeta(L(\langle \mathcal{A}_R[\alpha] \rangle, e, s))$, where $\emptyset = (0, \dots, 0) \in \mathbb{Z}^n$.
Let $SCC_R(e)$ be the strongly connected component of $e$ in the graph induced by $\langle \mathcal{A}_R \rangle$: its vertices are the elements of the $\mathcal{R}$-class of $e$, and its edges are of the form $r \xrightarrow{a} t$ and $t \xrightarrow{a^{-1}} r$, with $r\alpha(a) = t$. Indeed, recall that if $r, t$ lie in the same strongly connected component and if $r\alpha(a) = t$, we have transitions $(r, a, t)$ and $(r, a^{-1}, r)$ in $\langle \delta_R \rangle$. For a path $P$ labeled by a word $w \in \tilde{A}^*$ in $SCC_R(e)$, we let $\zeta(P) = \zeta(w)$. Then, for any $s \in \mathcal{R}$-equivalent to $e$, deciding whether $\emptyset \notin \zeta(L(\langle \mathcal{A}_R[\alpha] \rangle, e, s))$ amounts to finding a path $P$ from $e$ to $s$ with $\zeta(P) = \emptyset$.

We decide this question by computing a cycle basis. Let $T_R(e)$ be a spanning tree of $SCC_R(e)$. Let $r \xrightarrow{a} t$ be an edge of $SCC_R(e)$ with $a \in A$. If neither $r \xrightarrow{a} t$ nor $t \xrightarrow{a^{-1}} r$ is an edge of $T_R(e)$, we define a cycle by gluing the path from $t$ to $r$ in $T_R(e)$ with the edge $r \xrightarrow{a} t$. It is known [17,16] that the cycles $C_1, \dots, C_k$ we obtain form an integral cycle basis. This means that for any cycle $C$ in $SCC_R(e)$, the value $\zeta(C) \in \mathbb{Z}^n$ is a $\mathbb{Z}$-linear combination of the $\zeta(C_i)$ for $1 \le i \le k$.

Fix two paths $P, P'$ from $e$ to $s$ in $SCC_R(e)$. The path obtained by following $P$ forwards from $e$ to $s$ and then $P'$ backwards from $s$ to $e$ is a cycle $C$, and we have $\zeta(C) = \zeta(P) - \zeta(P')$. Since $(C_1, \dots, C_k)$ is an integral cycle basis, we have,

$$ \zeta(P) = \zeta(P') + \sum_{i=1}^{k} \lambda_i \zeta(C_i), \quad \text{for some integers } \lambda_1, \dots, \lambda_k. $$

Recall that deciding whether a (regular) element $s$ of the $\mathcal{R}$-class of $e$ is in the AMT-kernel is equivalent to determining whether there is a path $P$ from $e$ to $s$ with $\zeta(P) = \emptyset$. This leads to the following algorithm for answering this question:

- Pick $e \in E(M)$ such that $e \in \mathcal{R} s$.

- Compute a spanning tree of $SCC_R(e)$ and extract from this spanning tree:

* a cycle basis $(C_i)_{1 \le i \le k}$ of $SCC_R(e)$,

* the path $P'$ connecting $s$ to $e$ in this spanning tree.

- Solve the system $\zeta(P') + \sum_{i=1}^{k} \lambda_i \zeta(C_i) = \emptyset$ of unknowns $\lambda_1, \dots, \lambda_k \in \mathbb{Z}$.

Altogether, this boils down to solving an integer system. We do this in MeSCaL using Hermite normal forms along with the Flint library [44]. A rough analysis yields an overall $O(|M||A|\log(|M|))$ time complexity, for treating all $\mathcal{R}$-classes.

**Remark 14.** In MeSCaL, one single idempotent $e$ is chosen for each $\mathcal{R}$-class. The spanning tree is computed once, and used for all elements $s$ of this $\mathcal{R}$-class.

## 4.4 Computing MOD-kernels and MOD-cancels

Finally, separation for MOD is handled by reduction to either GR or AMT. Let $U = \{\}$ be a single-letter alphabet and $\mu: A^* \to U^*$ be the morphism defined by $\mu(a) = \$$ for every $a \in A$. The following is proved in [30, Theorem 26].

**Theorem 15.** Let $K, L \subseteq A^*$. The following conditions are equivalent:

1. $K$ is not MOD-separable from $L$.

2. $\mu(K)$ is not AMT-separable from $\mu(L)$.

3. $\mu(K)$ is not GR-separable from $\mu(L)$.
Clearly, if $L \subseteq A^*$ is recognized by an input NFA $\mathcal{A}$, one can compute an NFA recognizing $\mu(L)$ in linear time: one has to relabel all transitions with "$$". Therefore, we can compute MOD-kernels and MOD-cancels by using either the procedure for GR or that for AMT, yielding an efficient algorithm.

**Remark 16.** The MOD-kernel of a morphism $\alpha : A^* \to M$ was originally introduced by Straubing [41] under the name *stable monoid* using a specialized definition unrelated to MOD-separation. The image $\alpha(A)$ can be viewed as an element of the monoid $2^M$, equipped with the natural multiplication. Observe that this monoid has exponential size in $M$, hence doubly exponential in the size of the corresponding minimal automaton. The stable monoid can then be defined as $(\alpha(A))^\omega \cup \{1_M\}$. While interesting, this original definition leads to a significantly less efficient algorithm than the one we presented.

## 4.5 Green's relations

By Theorems 4 and 5, solving SF($\mathcal{G}$)-, PL($\mathcal{G}$)-, FL($\mathcal{G}$)- and TL($\mathcal{G}$)-membership requires computing the Green's relations of the $\mathcal{G}$-kernel. For the full syntactic monoid, the computation of its Green's relations amounts to computing the strongly connected components of its Cayley graphs. This approach is efficient because we have a small set of generators available for the syntactic monoid: the images of letters. Unfortunately, this is *not* the case for a submonoid.

In MeSCaL, we use an approach *specific to $\mathcal{G}$-kernels*. As seen in Optimization 1, we only need the Green's relations over *regular elements*. For $\mathcal{G}$-kernels, they are computed by restricting the Green's relations of the underlying monoid.

**Lemma 17.** Let $\mathcal{G}$ be a group variety, $\alpha : A^* \to M$ be a surjective morphism and $N$ be the $\mathcal{G}$-kernel of $\alpha$. Let $s, t \in N$. Assume that $s, t$ are regular in $M$. Then, for $\mathcal{K} \in \{\mathcal{H}, \mathcal{L}, \mathcal{R}\}$, we have $s \in \mathcal{K}_N$ if and only if $t \in \mathcal{K}_M$.

# 5 Conclusion

We presented an overview of the MeSCaL software, which is designed to test properties of regular languages. We explained that directly implementing algorithms from the literature often proves inefficient, but that careful optimization can significantly improve performance.

A key insight is that certain tasks—such as kernel computations—can be restricted to *regular* $\mathcal{R}$- or $\mathcal{L}$-classes. This not only reduces the computational space but also limits processing to strongly connected components of the Cayley graphs, resulting in substantial algorithmic simplifications.

We applied these techniques to classes Op($\mathcal{G}$), for $\text{Op} \in \{\text{SF, BPOL, TL, FL, PL}\}$ and $\mathcal{G} \in \{\text{ST, MOD, AMT, GR}\}$. MeSCaL currently supports around a hundred classes. A second paper will address additional classes, drawn from two distinct hierarchies, for which kernel and cancel precomputations are no longer sufficient.

*Acknowledgments.* We wish to thank the reviewers for some useful comments.
References

1. Ash, C.J.: Inevitable graphs: a proof of the type II conjecture and some related decision procedures. International Journal of Algebra and Computation 1(1), 127–146 (1991)

2. Auinger, K.: A new proof of the Rhodes type II conjecture. International Journal of Algebra and Computation 14(5-6), 551–568 (2004)

3. Caron, P.: LANGAGE: A Maple package for automaton characterization of regular languages. Theoretical Computer Science 231(1), 5–15 (2000). https://doi.org/10.1016/S0304-3975(99)00013-4

4. Champarnaud, J.M., Hansel, G.: AUTOMATE, a computing package for automata and finite semigroups. Journal of Symbolic Computation 12(2), 197–220 (1991). https://doi.org/10.1016/S0747-7171(08)80125-3

5. Dartois, L., Paperman, C.: Two-variable first order logic with modular predicates over words. In: Proceedings of the 30th International Symposium on Theoretical Aspects of Computer Science, STACS’13. pp. 329–340. Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2013). https://doi.org/10.4230/LIPIcs.STACS.2013.329

6. Delgado, M., Hoffmann, R., Linton, S., Morais, J.J.: Automata, a package on automata, Version 1.16. https://gap-packages.github.io/automata/ (2024), GAP package. See also https://cmup.fc.up.pt/cmup/mdelgado/varia/package-automata.pdf

7. Etessami, K., Vardi, M.Y., Wilke, T.: First-order logic with two variables and unary temporal logic. Information and Computation 179(2), 279–295 (2002). https://doi.org/10.1006/inco.2001.2953

8. Habermehl, P., Muscholl, A., Schwentick, T., Seidl, H.: Counting in trees for free. In: Proceedings of the 31st International Colloquium on Automata, Languages and Programming. pp. 1136–1149. ICALP’04, Springer (2004). https://doi.org/10.1007/978-3-540-27836-8_94

9. Henckell, K., Margolis, S., Pin, J.É., Rhodes, J.: Ash’s type II theorem, profinite topology and Malcev products. International Journal of Algebra and Computation 1, 411–436 (1991). https://doi.org/10.1142/S0218196791000298

10. Holzer, M., König, B.: On deterministic finite automata and syntactic monoid size. Theoretical Computer Science 327(3), 319–347 (2004). https://doi.org/10.1016/J.TCS.2004.04.010

11. Kamp, H.W.: Tense Logic and the Theory of Linear Order. PhD thesis, Computer Science Department, University of California at Los Angeles, USA (1968)

12. Kim, S.M., McNaughton, R., McCloskey, R.: A polynomial time algorithm for the local testability problem of deterministic finite automata. IEEE Trans. Computers 40(10), 1087–1093 (1991). https://doi.org/10.1109/12.93741

13. Krebs, A., Lodaya, K., Pandya, P.K., Straubing, H.: Two-variable logic with a between relation. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’16. pp. 106–115 (2016). https://doi.org/10.1145/2933575.2935308

14. Krebs, A., Lodaya, K., Pandya, P.K., Straubing, H.: An algebraic decision procedure for two-variable logic with a between relation. In: 27th EACSL Annual Conference on Computer Science Logic, CSL’18. Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2018). https://doi.org/10.4230/LIPIcs.CSL.2018.28
15. Krebs, A., Lodaya, K., Pandya, P.K., Straubing, H.: Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership. Logical Methods in Computer Science **Volume 16, Issue 3** (2020). https://doi.org/10.23638/LMCS-16(3:16)2020

16. Liebchen, C., Peeters, L.: Integral cycle bases for cyclic timetabling. Discrete Optimization **6**(1), 98–109 (2009). https://doi.org/10.1016/j.disopt.2008.09.003

17. Liebchen, C., Peeters, L.: On cyclic timetabling and cycles in graphs. Technical report, Technische Universität Berlin (2009), https://api-depositonce.tu-berlin.de/server/api/core/bitstreams/64451d02-8d8e-40b2-8399-0b63f8f7dfbf/content

18. Matz, O., Miller, A., Potthoff, A., Thomas, W., Valkema, E.: Report on the program AMORE. Tech. rep., Institut für Informatik und Praktische Mathematik, Christian-Albrechts Universität, Kiel (1995), https://sourceforge.net/projects/amore/

19. McNaughton, R., Papert, S.A.: Counter-Free Automata. MIT Press (1971)

20. Paperman, C.: Python module Pysemigroup (2024), https://gitlab.inria.fr/cpaperma/pysemigroup, online version at https://paperman.name/semigroup/

21. Pin, J.É.: PG = BG, a success story. NATO Advanced Study Institute, Semigroups, Formal Languages and Groups pp. 33–47 (1995), https://www.irif.fr/~jep/PDF/BGPG.pdf

22. Pin, J.É.: Semigroup. https://www.irif.fr/~jep/Logiciels/Semigroupe2.0/semigroupe2.html (2009)

23. Pin, J.É.: Mathematical foundations of automata theory (2025), http://www.irif.fr/~jep/PDF/MPRI/MPRI.pdf, in preparation

24. Pin, J.É., Delcroix, V.: Algorithms for computing finite semigroups. In: Cucker, F., Shub, M. (eds.) Foundations of Computational Mathematics. pp. 112–126. Springer, Rio de Janeiro, Brazil (1997), https://hal.science/hal-00143949v1/file/Rio97AMS.pdf

25. Pin, J.É., Reutenauer, C.: A conjecture on the Hall topology for the free group. Bulletin of the London Mathematical Society **23**(4), 356–362 (1991). https://doi.org/10.1112/blms/23.4.356

26. Place, T., Zeitoun, M.: A first taste of MeSCaL, a tool for solving membership problems for regular languages, https://www.labri.fr/perso/zeitoun/research/pdf/mescal1.pdf, long version.

27. Place, T., Zeitoun, M.: Generic results for concatenation hierarchies. Theory of Computing Systems (ToCS) **63**(4), 849–901 (2019). https://doi.org/10.1007/s00224-018-9867-0, selected papers from CSR’17

28. Place, T., Zeitoun, M.: Characterizing level one in group-based concatenation hierarchies. In: Proceeding of the 17th International Computer Science Symposium in Russia, CSR’22. Lecture Notes in Computer Science (2022). https://doi.org/10.1007/978-3-031-09574-0_20

29. Place, T., Zeitoun, M.: All about unambiguous polynomial closure. TheoretiCS **2** (2023). https://doi.org/10.46298/THEORETICS.23.11

30. Place, T., Zeitoun, M.: Group separation strikes back. In: 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’23. pp. 1–13. IEEE Computer Society (2023). https://doi.org/10.1109/LICS56636.2023.10175683, full version at https://arxiv.org/pdf/2205.01632

31. Place, T., Zeitoun, M.: A generic characterization of generalized unary temporal logic and two-variable first-order logic. In: Murano, A., Silva, A. (eds.) Proceedings of the 32nd EACSL Annual Conference on Computer Science Logic, CSL’24. LIPIcs,
vol. 288, pp. 45:1–45:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2024).
https://doi.org/10.4230/LIPICS.CSL.2024.45

32. Place, T., Zeitoun, M.: Closing star-free closure. ACM Transactions on Computational Logic (2025). https://doi.org/10.1145/3733831

33. Place, T., Zeitoun, M.: In orbit with MeSCaL: higher in concatenation and navigational hierarchies of regular languages. In: Castiglione, G., Mantaci, S. (eds.) Proceedings of the 29th International Conference on Implementation and Application of Automata, CIAA 2025. Lecture Notes in Computer Science, Springer, Palermo, Italy (2025)

34. Place, T., Zeitoun, M.: MeSCaL, MEmbership and Separation for CLasses of Languages. https://github.com/thomas-place/mescal (2025)

35. Ribes, L., Zalesskii, P.A.: On the profinite topology on a free group. Bulletin of the London Mathematical Society 25(1), 37–43 (1993). https://doi.org/10.1112/blms/25.1.37

36. Scarpellini, B.: Complexity of subcases of Presburger arithmetic. Transactions of the American Mathematical Society 284, 203–218 (1984). https://doi.org/10.2307/1999283

37. Schützenberger, M.P.: On finite monoids having only trivial subgroups. Information and Control 8(2), 190–194 (1965). https://doi.org/10.1016/S0019-9958(65)90108-7

38. Simon, I.: Piecewise testable events. In: Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages. pp. 214–222. Springer (1975). https://doi.org/10.1007/3-540-07407-4_23

39. Stallings, J.R.: Topology of finite graphs. Inventiones mathematicae **71**(3), 551–565 (Mar 1983). https://doi.org/10.1007/BF02095993

40. Stern, J.: Complexity of some problems from the theory of automata. Information and Control **66**(3), 163–176 (1985). https://doi.org/10.1016/S0019-9958(85)80058-9

41. Straubing, H.: On logical descriptions of regular languages. In: LATIN 2002: Theoretical Informatics, 5th Latin American Symposium. lncs, vol. 2286, pp. 528–538. springer (2002). https://doi.org/10.1007/3-540-45995-2_46

42. Tarjan, R.: Depth-first search and linear graph algorithms. SIAM Journal on Computing **1**(2), 146–160 (1972). https://doi.org/10.1137/0201010

43. Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM **22**(2), 215–225 (1975). https://doi.org/10.1145/321879.321884

44. The FLINT team: FLINT: Fast Library for Number Theory (2025), version 3.2.1, https://flintlib.org

45. Thérien, D., Wilke, T.: Over words, two variables are as powerful as one quantifier alternation. In: Proceedings of the 30th Annual ACM Symposium on Theory of Computing. pp. 234–240. STOC’98, ACM (1998). https://doi.org/10.1145/276698.276749

46. Thomas, W.: Classifying regular events in symbolic logic. Journal of Computer and System Sciences **25**(3), 360–376 (1982). https://doi.org/10.1016/0022-0000(82)90016-2

47. Touikan, N.W.M.: A fast algorithm for Stallings’ folding process. International Journal of Algebra and Computation **16**(06), 1031–1045 (2006). https://doi.org/10.1142/S0218196706003396

48. Trahtman, A.N.: A package TESTAS for checking some kinds of testability. CoRR abs/2105.12583 (2021), https://arxiv.org/abs/2105.12583