In orbit with MeSCaL: higher in concatenation and navigational hierarchies of 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 paper is the second in a two-part series presenting "MeSCaL", a program dedicated to testing properties of regular languages. It provides users with an interface that allows them to define regular languages through regular expressions or finite automata. They can then perform property tests on the defined languages. These properties consist of checking membership in predefined classes of regular languages. MeSCaL supports about a hundred classes. The first paper in the series details some of its data structures, explains why existing algorithms from the literature are unlikely to run in reasonable time even for simple input languages, and describes optimizations that make the software more efficient than those algorithms. It applies to 20 different classes. This second article continues that work, but remains largely independent of the first: it considers 44 new classes for which membership tests require the precomputation of new objects, called *orbits*. The computation of these orbits uses some results from the first part as a black box. The classes to which the presented optimizations apply are levels of language hierarchies, which come in two types: concatenation hierarchies and navigational hierarchies. While the first part focused on level one of these hierarchies, this second article addresses level two, as well as intermediate levels between one and two. It also explains how to handle hierarchies whose base level (level zero) was not covered in the first article.

**Keywords:** Regular languages · Finite monoids · Implementation · Membership problem · Separation problem · Concatenation hierarchies · Navigational hierarchies

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

**Context.** This article is the second in a series of two, completing [25]. These papers introduce a recent software tool called MeSCaL<fnref n="1" /> [26] (MEmbership and Separation for ClAsses of Languages). MeSCaL implements “membership algorithms” for subclasses of regular languages of finite words. Each membership algorithm is tailored to a specific class *C*, and determines whether a given regular language belongs to the class *C*. The associated “*C*-membership problem” amounts, in terms of computability theory, to asking whether the class *C* is recursive. Such questions are fundamental in computer science. In the context of regular languages, they provide a way to measure the “complexity” of a language, by determining whether it lies within simple subclasses. This second paper focuses on the implementation of membership algorithms for classes that belong to natural hierarchies within the class of regular languages. More precisely, we consider two types of hierarchies:

1. Concatenation hierarchies, introduced by Brzozowski and Cohen [1].

2. Navigational hierarchies, a closely related framework introduced in [27].

Concatenation hierarchies are a foundational and historically significant concept in automata theory. Each hierarchy is defined uniformly from a single parameter: a class *C*, called its *basis*. The hierarchy consists of classes of regular languages—its *levels*—indexed by natural numbers. Level 0 is the base class *C*, and level *n* + 1 is obtained by forming all Boolean combinations of languages of the form $L_0 a_1 L_1 \cdots a_n L_n$, where each $a_i$ is a letter of the alphabet and each $L_i$ is a language of level *n*. Intuitively, each level in the hierarchy reflects the number of required alternations between concatenation and Boolean operations.

The interest in concatenation hierarchies stems from the fact that they correspond, level by level, to the quantifier alternation hierarchies in first-order logic. It is well known that regular languages are those defined by monadic second-order logic, and that first-order logic defines a strict subclass [11,28]. Thomas [30] established that level *n* of the concatenation hierarchy of basis {$\emptyset, \{\varepsilon\}, A^+, A^*$} (where *A* denotes the alphabet) corresponds to the logical fragment $B\Sigma_n(<, +1)$ of first-order logic, which allows at most *n* blocks of quantifiers $\exists^*/\forall^*$. More generally, for any (well-behaved) class *C*, there exists a set of predicates $\mathbb{I}_C$ such that level *n* in the concatenation hierarchy of basis *C* contains exactly the languages defined in $B\Sigma_n(\mathbb{I}_C)$ [18]. Deciding membership in levels of concatenation hierarchies remains one of the last “old” problems still open for regular languages.

Navigational hierarchies are a more recent development [27]. Like concatenation hierarchies, they are built from a base class *C* by repeatedly applying an operator that produces increasingly large levels. They come in three variants. In the first one, the operator is inspired by full unary temporal logic [6,29], using the *finally* (F) and *past* (P) modalities. The operator $C \mapsto \text{TL}(C)$ extends *C* by allowing the use of similar modalities, each guarded by a language of *C*. The semantics is natural: a language used as a guard restrict the jumps of the modality. For instance, a formula $F_L \varphi$ holds in *w* at position *i* if there exists a

<footnote n="1">¹ https://github.com/thomas-place/mescal</footnote>
position $j > i$ such that $\varphi$ holds in $w$ at position $j$, and the infix between $i$ and $j$ belongs to $L$. The other variants are based on restricted operators $C \mapsto \text{FL}(C)$ and $C \mapsto \text{PL}(C)$: the FL- (resp. PL-)hierarchy disallows $P_L$ (resp. $F_L$) modalities.

**Related work.** Several programs in the literature do implement membership tests. For example, PySemigroup [12] offers a range of such tests, though efficiency is not its main concern. Others tools, such as Semigroupe [14,16] and, to some extent, AUTOMATE [3], AMORE [10] and Automata [5], are built around the computation and manipulation of the syntactic monoid of a language, with a few membership results derived as a byproduct. In contrast, tools like LANGUAGE [2] and TESTAS [31] concentrate on a limited set of membership problems, which they handle efficiently directly on automata, bypassing the computation of the syntactic monoid. However, none of these tools cover the classes we target here—first, because the corresponding algorithms are relatively recent, and second, because they are difficult to implement efficiently: due to the size of the monoids in which computations are performed, naive implementations would be impractical.

**Contributions.** We address computational challenges for several known membership algorithms, optimizing their performance in order to implement them in MeSCaL. We consider 44 specific classes $\mathcal{C}$. All of them are the form $\text{Op}(\mathcal{G})$ or $\text{Op}(\mathcal{G}^+)$, where $\mathcal{G}$ spans four standard classes of languages, $\mathcal{G}^+$ denotes an extension of such a class, and $\text{Op}$ denotes specific levels of concatenation hierarchies, or levels one or two in the TL, FL or PL hierarchies. More precisely, the four base classes $\mathcal{G}$ in our hierarchies are: the trivial class $\text{ST} = \{\emptyset, A^*\}$, the class $\text{MOD}$ of all unions of languages of the form $(A^q)*A^r$, the class $\text{AMT}$ of Boolean combinations of languages counting letter occurrences modulo some integer, and the class $\text{GR}$ of group languages, recognized by DFAs where each letter induces a permutation on states. The inclusion of $\text{MOD}$ and $\text{AMT}$ is justified from the logical perspective, as they yield natural predicates in the aforementioned signature $\mathbb{I}_{\mathcal{C}}$ constructed from $\mathcal{C}$.

Some levels we study are based on additional operators. The class $\text{Pol}(\mathcal{C})$ consists of unions of languages of the form $L_0a_1L_1\cdots a_nL_n$, where the $a_i$'s are letters and the $L_i$'s belong to $\mathcal{C}$. The class $\text{Bool}(\mathcal{C})$ is the Boolean closure of $\mathcal{C}$, and we let $\text{BPol}(\mathcal{C}) = \text{Bool}(\text{Pol}(\mathcal{C}))$. Moreover, we inductively set $\text{BPol}_0(\mathcal{C}) = \mathcal{C}$ and, for $n \ge 1$, define $\text{BPol}_n(\mathcal{C}) = \text{BPol}(\text{BPol}_{n-1}(\mathcal{C}))$. Furthermore, $\text{IPol}(\mathcal{C})$ is the greatest Boolean algebra included in $\text{Pol}(\mathcal{C})$. At last, we define $\text{TL}_2(\mathcal{C}) = \text{TL}(\text{TL}(\mathcal{C}))$. We are ready to present the 44 classes studied in this paper. For $\mathcal{G} \in \{\text{ST}, \text{MOD}, \text{AMT}, \text{GR}\}$,

- The 8 classes of the form $\text{IPol}(\text{BPol}_2(\mathcal{G}))$ and $\text{IPol}(\text{BPol}_2(\mathcal{G}^+))$,

- The 12 classes $\text{TL}(\mathcal{G}^+)$, $\text{FL}(\mathcal{G}^+)$ and $\text{PL}(\mathcal{G}^+)$. The non-+ variants were already treated in [25].

- The 24 classes $\text{TL}_2(\mathcal{G})$, $\text{FL}_2(\mathcal{G})$, $\text{PL}_2(\mathcal{G})$, $\text{TL}_2(\mathcal{G}^+)$, $\text{FL}_2(\mathcal{G}^+)$ and $\text{PL}_2(\mathcal{G}^+)$.

A crucial point is that the $\text{Op}(\mathcal{C})$-membership algorithms implemented in MeSCaL (for the involved operators $\text{Op}$) rely on the precomputation of subsets of the syntactic monoid of the input language, called its $\mathcal{C}$-orbits. Such subsets are expensive to compute, and much of the work presented in this article consists of optimizing this calculation.
*Remark 1.* As stated above, this paper is the second one introducing the MeSCaL software in a two-part series. It is written to be self-contained and can be read independently of the first [25]. That said, some of the algorithms presented here build on simpler procedures described in [25]. However, these are used as black boxes, so that the two papers remain largely independent.

**Organization.** Section 2 introduces the fundamental objects manipulated in MeSCaL. In Section 3, we define the classes discussed in the paper, describe the corresponding membership algorithms, and highlight key optimizations. Finally, Section 4 and Section 5 focus on the computation of orbits. Due to space constraints, proofs are deferred to [17].

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

MeSCaL implements *membership algorithms* for several classes. For a class $\mathcal{C}$, $\mathcal{C}$-*membership* 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*. The $\mathcal{D}$-separation problem 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$ 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 every recognizer, such as an automaton or an arbitrary recognizing morphism.

## MeSCaL Data Structures 1

In MeSCaL, syntactic morphisms are represented using Cayley graphs instead of explicitly storing (potentially large) multiplication tables. As a result, element multiplication is not constant-time, so we strive to limit such multiplications. For further details on how MeSCaL represents morphisms, see [25].

**Green's relations.** Over any monoid $M$, we define preorders $\leq_R$, $\leq_L$, $\leq_g$ as follows. For $q, s \in M$, we write $q \leq_R s$ (resp. $q \leq_L s$, resp. $q \leq_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{J}\}$, we let $\mathcal{K}$ be the equivalence relation associated with $\leq_K$, i.e., defined by $s \mathcal{K} t$ if and only if $s \leq_K t$ and $t \leq_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{J}$ 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{J}\}$, 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.

**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{J}\}$) if it contains an idempotent.

# 3 Concatenation hierarchies and navigational hierarchies

We look at two types of hierarchies: the *concatenation hierarchies* introduced by Brzozowski and Cohen [1], and the more recently defined navigational hierarchies [27]. Each hierarchy is built using a specific operator. Starting from an initial class $\mathcal{C}$, referred to as the basis (this is level zero), subsequent levels are built iteratively: level $n+1$ is obtained by applying the operator to level $n$.

For most of the well-known bases studied in the literature, MeSCaL provides membership tests for the lower levels of both hierarchy types—typically up to level two. The algorithms rely on algebraic characterizations of the operators. In this section, we review the definitions of these hierarchies along with their characterizations, and we discuss the challenges posed by their implementation.

## 3.1 Operators and hierarchies

**Concatenation hierarchies.** For every class $\mathcal{C}$, the *polynomial closure of* $\mathcal{C}$, written $\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 \stackrel{\text{def}}{=} K\{a\}L \in \text{Pol}(\mathcal{C})$
for all $a \in A$. In general, $\text{Pol}(C)$ is not closed under Boolean operations. We write $\text{BPol}(C)$ for the least Boolean algebra containing $\text{Pol}(C)$.

We now define concatenation hierarchies. Consider an arbitrary class $\mathcal{C}$. With each $n \in \mathbb{N}$, we associate a class $\text{BPol}_n(\mathcal{C})$. First, we let $\text{BPol}_0(\mathcal{C}) = \mathcal{C}$. Then, we let $\text{BPol}_{n+1}(\mathcal{C}) = \text{BPol}(\text{BPol}_n(\mathcal{C}))$. Clearly, $\text{BPol}_n(\mathcal{C}) \subseteq \text{BPol}_{n+1}(\mathcal{C})$ for all $n$. Hence, this defines a hierarchy of classes: the *concatenation hierarchy* of basis $\mathcal{C}$.

Membership is difficult to handle for $\text{BPol}_n(\mathcal{C})$. For $t<\text{his reason, we also look at intermediary levels. For a class } \mathcal{D}, \text{ we let co-}\mathcal{D} \text{ be the class of all complements of languages in } \mathcal{D}. That is, } \text{co-}\mathcal{D} = \{A^* \setminus L \mid L \in \mathcal{D}\}$. For every class $\mathcal{C}$, $\text{IPol}(\mathcal{C}) = \text{Pol}(\mathcal{C}) \cap \text{co-Pol}(\mathcal{C})$ is the greatest Boolean algebra contained in $\text{Pol}(\mathcal{C})$. The classes $\text{IPol}(\text{BPol}_n(\mathcal{C}))$ are called *intermediary levels* in the concatenation hierarchy of basis $\mathcal{C}$, and are simpler to handle with respect to membership.

**Remark 2.** For a prevariety $\mathcal{D}$, $\text{IPol}(\mathcal{D})$ is exactly the *unambiguous polynomial closure* $\text{UPol}(\mathcal{D})$ of $\mathcal{D}$ [13,22]. $\text{UPol}$ is defined from $\text{Pol}$ by restricting the marked concatenations to those that are *unambiguous*: $\text{KaL}$ is unambiguous if and only if every word $w \in \text{KaL}$ admits a *unique* decomposition witnessing this membership.

Historically, the first concatenation hierarchy is the *dot-depth* [1] of basis $\{\emptyset, \{\varepsilon\}, A^+, A^*\}$. In particular, Thomas [30] proved that the dot-depth corresponds exactly to the *quantifier alternation hierarchy* of first-order logic equipped with predicates for the linear order and the successor $\text{FO}(<, +1)$. Specifically, $\text{BPol}_n(\{\emptyset, \{\varepsilon\}, A^+, A^*\}) = \mathcal{B}\Sigma_n(<, +1)$ for all $n \in \mathbb{N}$. This extends to arbitrary concatenation hierarchies [18]: for every prevariety $\mathcal{C}$, there exists a suitable set $\mathbb{I}_\mathcal{C}$ of first-order predicates such that $\text{BPol}_n(\mathcal{C}) = \mathcal{B}\Sigma_n(\mathbb{I}_\mathcal{C})$ for all $n \in \mathbb{N}$ (see [25]).

**Navigational hierarchies.** This notion was introduced in [27]. Navigational hierarchies are built with three operators from [22] inspired by temporal logic: $\text{TL}(\mathcal{C})$, $\text{FL}(\mathcal{C})$ and $\text{PL}(\mathcal{C})$. Let $\mathcal{C}$ be a prevariety. Formulas in $\text{TL}[\mathcal{C}]$ are defined by the grammar $\varphi := a \mid \varphi \land \varphi \mid \varphi \lor \varphi \mid \neg\varphi \mid \text{F}_L \varphi \mid \text{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 $\text{P}_L$ (resp. $\text{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, \ldots, |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 \text{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 \text{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}[\mathcal{C}]$, we define $L_{\min}(\varphi) = \{w \in A^* \mid w, 0 \models \varphi\}$ and $L_{\max}(\varphi) = \{w \in A^* \mid w, |w| + 1 \models \varphi\}$. We are ready to define our three classes:
– $\text{TL}(\mathcal{C})$ is the class consisting of all languages $L_{\min}(\varphi)$ with $\varphi \in \text{TL}[\mathcal{C}]$.
– $\text{FL}(\mathcal{C})$ is the class consisting of all languages $L_{\min}(\varphi)$ with $\varphi \in \text{FL}[\mathcal{C}]$.
– $\text{PL}(\mathcal{C})$ is the class consisting of all languages $L_{\max}(\varphi)$ with $\varphi \in \text{PL}[\mathcal{C}]$.

A correspondence result between the operator TL and the two-variable fragment of first-order logic is known [22]. We have $\text{TL}(\mathcal{C}) = \text{FO}^2(\mathbb{I}_\mathcal{C})$ for each prevariety $\mathcal{C}$.
We are ready to define three navigational hierarchies. Their construction parallels that of concatenation hierarchies. Given a base class $\mathcal{C}$, we define three levels for each $n \in \mathbb{N}$: $\text{TL}_n(\mathcal{C})$, $\text{FL}_n(\mathcal{C})$, and $\text{PL}_n(\mathcal{C})$.

- We let $\text{TL}_0(\mathcal{C}) = \text{FL}_0(\mathcal{C}) = \text{PL}_0(\mathcal{C}) = \mathcal{C}$

- For every $n \in \mathbb{N}$, we let $\text{TL}_{n+1}(\mathcal{C}) = \text{TL}(\text{TL}_n(\mathcal{C}))$, $\text{FL}_{n+1}(\mathcal{C}) = \text{FL}(\text{FL}_n(\mathcal{C}))$ and $\text{PL}_{n+1}(\mathcal{C}) = \text{PL}(\text{PL}_n(\mathcal{C}))$.

These hierarchies are closely related to concatenation hierarchies. It is shown in [27] that $\bigcup_{n \in \mathbb{N}} \text{BPol}_n(\mathcal{C}) = \bigcup_{n \in \mathbb{N}} \text{TL}_n(\mathcal{C}) = \bigcup_{n \in \mathbb{N}} \text{FL}_n(\mathcal{C}) = \bigcup_{n \in \mathbb{N}} \text{PL}_n(\mathcal{C})$ for all prevarieties $\mathcal{C}$. However, the levels themselves differ: in general, $\text{BPol}_n(\mathcal{C})$ is strictly contained in $\text{TL}_n(\mathcal{C})$, $\text{FL}_n(\mathcal{C})$, and $\text{PL}_n(\mathcal{C})$. Although navigational hierarchies were formally introduced in [27], specific levels had already been studied in earlier works [4,7,8,9,29].

## 3.2 Prominent bases: group prevarieties and well-suited extensions

Prominent hierarchies in the literature use specific bases. A group $G$ is a monoid in which 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. Our bases are either group prevarieties (i.e., prevarieties consisting only of group languages) or extensions of such classes. 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^* \mid \#_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 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^* \mid |w| \equiv r \pmod q\}$ for $0 \le r < q$.

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

*Remark 3.* The significance of these base classes is underscored by their connection to quantifier alternation hierarchies in first-order logic. The bases ST, MOD, and AMT correspond to natural logical predicates:

- ST yields the hierarchy of first-order logic with linear order only, $\text{FO}(<)$.

- MOD extends this with *modular predicates* of the form "$x \equiv r \pmod q$."

- AMT further adds *letter modular predicates* of the form "$\#_a(x) \equiv r \pmod q$," where $\#_a(x)$ counts the occurrences of letter $a \in A$ before position $x$.

We also look at well-suited extensions. For a class $\mathcal{G}$, the *well-suited extension of* $\mathcal{G}$ is the class $\mathcal{G}^+$ consisting of all languages $L \cap A^+$ and $L \cup \{\varepsilon\}$ with $L \in \mathcal{G}$.

*Remark 4.* From a logical perspective, using a well-suited-extension as the basis of a concatenation hierarchy corresponds to enriching the logic with the successor predicate “+1.” For example, the basis $\text{ST}^+ = \{\emptyset, \{\varepsilon\}, A^+, A^*\}$ of the dot-depth hierarchy yields the quantifier alternation hierarchy of $\text{FO}(<, +1)$.

In the case of temporal closures, a well-suited-extension expands the set of temporal modalities by adding the classical ones *tomorrow* (X) and *yesterday* (Y).
<figure><img src="image_1.png" /></figure>

## MeSCaL features

MeSCaL supports membership for level one in all hierarchies discussed, using bases $\mathcal{G}$ or $\mathcal{G}^+$, with $\mathcal{G} \in \{\text{GR, AMT, MOD, ST}\}$. The case of bases $\mathcal{G}$ is detailed in [25]. Here, we focus the classes $\text{TL}(\mathcal{G}^+)$, $\text{FL}(\mathcal{G}^+)$, and $\text{PL}(\mathcal{G}^+)$. MeSCaL also includes procedures for the classes $\text{BPol}(\mathcal{G}^+)$, but we omit them here.

MeSCaL also handles level two membership for all three navigational hierarchies over the bases $\mathcal{G}$ and $\mathcal{G}^+$ for $\mathcal{G} \in \{\text{GR, AMT, MOD, ST}\}$. We detail the implementation in this paper.

For concatenation hierarchies, level two is implemented only for $\text{BPol}_2(\text{ST})$ (we omit the details in this paper). However, MeSCaL supports all classes of the form $\text{IPol}(\text{BPol}_2(\mathcal{G}))$ and $\text{IPol}(\text{BPol}_2(\mathcal{G}^+))$, for $\mathcal{G} \in \{\text{GR, AMT, MOD, ST}\}$; we present the algorithms here.

**Remark 5.** In the above discussion, we omit the intermediate levels $\text{IPol}(\text{BPol}(\mathcal{G}))$ and $\text{IPol}(\text{BPol}(\mathcal{G}^+))$. This is because when $\mathcal{G}$ is a group prevariety, they correspond exactly [29,22] to $\text{TL}(\mathcal{G})$ and $\text{TL}(\mathcal{G}^+)$, respectively.

## 3.3 Algebraic characterizations and membership

Membership tests implemented in MeSCaL are based on characterization theorems. For each operator Op, they imply that $\text{Op}(C)$-membership reduces to a more general problem for $C$, typically, $C$-separation.

**C-orbits.** Most characterizations rely on a key object: C-orbits. In order to define them, we need a preliminary notion: C-pairs. Let $C$ be a prevariety and $\alpha : A^* \to M$ a morphism. A C-pair (for $\alpha$) is a pair $(s, t) \in M^2$ such that $\alpha^{-1}(s)$ is not C-separable from $\alpha^{-1}(t)$. The next lemma is proved in [22, Lemma 5.12].

**Lemma 6.** Let $C$ be a prevariety and $\alpha : A^* \to M$ be a morphism. Moreover, let $(s, t), (s', t') \in M^2$ be two C-pairs. Then $(ss', tt')$ is a C-pair.

We are ready to define C-orbits. Let $\alpha : A^* \to M$ be a morphism. Let $e \in E(M)$ be an idempotent. Clearly, $eMe$ is a monoid (its identity is $e$). For each prevariety $C$, we define a submonoid $M_e$ of $eMe$: the C-orbit of $e$ for $\alpha$. We let $M_e = \{s \in eMe \mid (e, s) \text{ is a C-pair for } \alpha\}$. Lemma 6 implies that $M_e$ is indeed a submonoid of $eMe$. Computing C-orbits clearly reduces to solving C-separation.

Most of the operators defined in the section can be characterized using C-orbits (the only exception is BPol). We start with the temporal closures. The characterization of $C \mapsto \text{TL}(C)$ uses the class of monoids DA. Typically, it is 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 theorem is proved in [24, Theorems 37 and 38].

**Theorem 7.** Let $C$ be a prevariety and $L$ be a regular language:

- $L \in \text{PL}(C)$ if and only if all C-orbits for its syntactic morphism are $\mathcal{L}$-trivial.

- $L \in \text{FL}(C)$ if and only if all C-orbits for its syntactic morphism are $\mathcal{R}$-trivial.

- $L \in \text{TL}(C)$ if and only if all C-orbits for its syntactic morphism are in DA.
The operator $C \mapsto \text{IPol}(\text{BPol}(C))$ is characterized by an equation involving the $C$-orbits of the morphism. The following result is proved in [22, Theorem 6.7].

**Theorem 8.** Let $C$ be a prevariety, $L$ be a regular language and $\alpha: A^* \to M$ be its syntactic morphism. For every $e \in E(M)$, let $M_e \subseteq eMe$ be the $C$-orbit of $e$ for $\alpha$. Then, $L \in \text{IPol}(\text{BPol}(C))$ if and only if $\alpha$ satisfies the following property:

$$ (st)^{\omega+1} = (st)^{\omega}t(st)^{\omega} \text{ for all } e \in E(M), \text{ all } s \in M_e \text{ and all } t \in eMe. \quad (1) $$

*Remark 9.* We omit the algorithms used in MeSCaL to decide the classes built with BPOL, as this involves objects that go beyond $C$-orbits and would require introducing too much material. We come back to BPOL in the conclusion.

**Computing orbits.** MeSCaL includes efficient algorithms that compute $C$-orbits when $C$ is level zero or one in the concatenation and navigational hierarchies of bases $G$ or $G^+$ where $G$ is ST, MOD, AMT or GR. The membership procedures tests from Theorem 7 and Theorem 8. Let us first make an important remark concerning the information that we have to compute.

### MeSCaL Optimization 1: Green's relations for regular elements

Implementing Theorem 7 requires checking whether the $C$-orbits are $R$-trivial, $L$-trivial, or belong to DA. A standard result (see, e.g., [15, Proposition 2.26]) states that for $\mathcal{K} \in \{\mathcal{R}, \mathcal{L}\}$, a monoid is $\mathcal{K}$-trivial if and only if all its regular $\mathcal{K}$-classes are trivial. Similarly, a monoid lies in DA if and only if all its regular elements are idempotent. This is crucial: to implement Theorem 7, it suffices to compute the regular elements of the $C$-orbits and their Green's relations.

In contrast, implementing Theorem 8 requires all elements in the $C$-orbits, though the Green's relations are not needed.

We now concentrate on computing of $C$-orbits. We start with a key optimization, common to all classes $C$.

**Lemma 10.** Let $\alpha: A^* \to M$ be a morphism and $e, f \in E(M)$ such that $e \mathcal{J} f$. There is an isomorphism $\gamma: eMe \to fMf$ such that for all prevarieties $C$, if $M_e \subseteq eMe$ and $M_f \subseteq fMf$ are the $C$-orbits of $e$ and $f$ for $\alpha$, then $\gamma(M_e) = M_f$.

### MeSCaL Optimization 2: Factorizing the $C$-orbits

When a new syntactic morphism $\alpha: A^* \to M$ is computed in MeSCaL, a single witness idempotent is chosen in each regular $\mathcal{J}$-class of $M$. For each input class $C$, MeSCaL computes only the $C$-orbits of these witnesses. By Lemma 10, this is sufficient to determine which properties hold for all $C$-orbits: every omitted $C$-orbit is isomorphic to one that has been computed.

## 4 Computing $G$-orbits and $G^+$-orbits

We now turn to the computations of $G$- and $G^+$-orbits, which rely on an important object already discussed in [25]: the $G$-kernel.
**G-kernel.** Let $\mathcal{G}$ be a group prevariety and $\alpha : A^* \to M$ be a morphism. The $\mathcal{G}$-kernel of $\alpha$ is the set $N \subseteq M$ that consists of all elements $s \in M$ such that $\{\varepsilon\}$ is not $\mathcal{G}$-separable from $\alpha^{-1}(s)$. We have the following lemma (see [22, Fact 5.5]).

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

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

### MeSCaL Optimization 3: Computing regular elements in $\mathcal{G}$-kernels

MeSCaL implements efficient procedures for computing the $\mathcal{G}$-kernel when $\mathcal{G}$ is either ST, MOD, AMT or GR, as detailed in [25]. Here, we treat these procedures as black boxes. Crucially, computing only the regular elements of the $\mathcal{G}$-kernel is significantly more efficient than computing the entire kernel—and this is always sufficient for our purposes.

**$\mathcal{G}$-orbits.** When $\mathcal{G}$ is a group prevariety, we do not need the $\mathcal{G}$-orbits. Instead, the $\mathcal{G}$-kernel alone suffices. Indeed, we have the following lemma.

**Lemma 12.** Let $\mathcal{G}$ be a group prevariety, $\alpha : A^* \to M$ be an onto morphism and $N \subseteq M$ be its $\mathcal{G}$-kernel. For all $e \in E(M)$, the $\mathcal{G}$-orbit of $e$ for $\alpha$ is $eNe \subseteq N$. In particular, the $\mathcal{G}$-orbit of $1_M$ for $\alpha$ is $N$.

By Lemma 12, if $\mathcal{G}$ is a group prevariety, we only need a single $\mathcal{G}$-orbit: that of $1_M$, which is also the $\mathcal{G}$-kernel. This forms the foundation of how MeSCaL implements membership for classes $\text{Op}(\mathcal{G})$. Kernel computations are detailed in [25].

**$\mathcal{G}^+$-orbits.** We now consider the computation of the $\mathcal{G}^+$-orbits for the well-suited extension $\mathcal{G}^+$ of a group prevariety $\mathcal{G}$. This computation is based on the $\mathcal{G}$-kernel.

**Proposition 13.** Let $\mathcal{G}$ be a group prevariety, $\alpha : A^* \to M$ be an onto morphism, $S = \alpha(A^+)$ and $N \subseteq M$ be the $\mathcal{G}$-kernel of $\alpha$. For all $e \in E(S)$, the $\mathcal{G}^+$-orbit of $e$ for $\alpha$ is $eNe \subseteq N$. Moreover, if $1_M \notin S$, then the $\mathcal{G}$-orbit of $1_M$ for $\alpha$ is $\{1_M\}$.

**Remark 14.** When $\mathcal{G} = \text{ST} = \{\emptyset, A^*\}$, the ST-kernel is the whole monoid $M$. By Proposition 13, it follows that for $e \in S$, the ST$^+$-orbit of $e$ is the monoid $eSe$. This is a well-known object in semigroup theory, called the *local monoid of e*.

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

### MeSCaL Optimization 4: Computation of $\mathcal{G}^+$-orbits

Once we have the $\mathcal{G}$-kernel $N$ in hand, Proposition 13 shows that for $e \in E(S)$, the $\mathcal{G}^+$-orbit of $e$ can be computed by intersecting $N$ with $eM$ and $Me$. Computing $eM$ and $Me$ is straightforward and done in MeSCaL via traversals of the right and left Cayley graphs of $\alpha$, which takes $O(|M||A|)$ time.

Finally, since the $\mathcal{G}^+$-orbit of $e$ is included in $N$, the restriction of $N$ to its regular elements is sufficient to compute all regular elements of this $\mathcal{G}^+$-orbit.

Moreover, once a $\mathcal{G}^+$-orbit is obtained, computing its Green's relations restricted to regular elements becomes straightforward (recall from *Optimization 1* that this information is sufficient to decide level 1 in navigational hierarchies). The next lemma shows that, for regular elements, this amounts to restricting the Green's relations of the underlying monoid $M$.
**Lemma 15.** Let $\mathcal{G}$ be a group prevariety, $\alpha : A^* \to M$ be an onto morphism, $e \in E(M)$ and $M_e$ be the $\mathcal{G}^+$-orbit of $e$ for $\alpha$. Let $s, t \in M_e$ be regular in $M$. Then, for $\mathcal{K} \in \{\mathcal{H}, \mathcal{L}, \mathcal{R}\}$, we have $s \mathcal{K}_{M_e}$ t if and only if $s \mathcal{K}_M$ t.

Finally, yet another important optimization is available for $\mathcal{G}^+$-orbits. We already mentioned after Lemma 10 that for an arbitrary prevariety $\mathcal{C}$, computing one $\mathcal{C}$-orbit per regular $\mathcal{J}$-class suffices. This can be pushed further when $\mathcal{C} = \mathcal{G}^+$.

Let $\alpha : A^* \to M$ be a morphism. Let $S = \alpha(A^+)$. A *root set* (of idempotents) for $\alpha$ is a set $T \subseteq E(S)$ that satisfies the two following properties:

1. $e_1 \leq g e_2$ for all $e_1, e_2 \in T$, and,

2. for all $f \in E(S)$, there exists $e \in T$ such that $e \leq g f$.

By definition, root sets are typically small in practice. Importantly, we only need
the $\mathcal{G}^+$-orbits of the idempotents they contain.

**Proposition 16.** *Let $\mathcal{G}$ be a group prevariety, $\alpha : A^* \to M$ be an onto morphism and $S = \alpha(A^+)$. Let $e, f \in E(S)$, $M_e$ be the $\mathcal{G}^+$-orbit of $e$, $M_f$ be the $\mathcal{G}^+$-orbit of $f$. Assume that there exists $q, r \in M$ such that $f = qr$ (i.e., $e \leq q \leq r$). Then, $M_f$ is isomorphic to a subsemigroup of $M_e$ and $M_f \subseteq qM_e$.*

MeSCaL Optimization 5: Factorizing the $G^+$-orbits

When a new syntactic morphism $\alpha : A^* \to M$ is computed in MeSCaL, a root set is computed for $\alpha$. Given a group prevariety $\mathcal{G}$, MeSCaL computes only the $\mathcal{G}^+$-orbits of the idempotents in this root set. By Proposition 16, this is sufficient to determine which properties hold for all $\mathcal{G}^+$-orbits: every omitted $\mathcal{G}^+$-orbit is isomorphic to a subsemigroup of one that has been computed.

5 Orbits for more complex classes

As announced in Section 3, MeSCaL includes membership tests for the classes
TL<sub>2</sub>(C), FL<sub>2</sub>(C), PL<sub>2</sub>(C) and IPol(BPol<sub>2</sub>(C)) when C ∈ {G, G<sup>+</sup>} for one of the
group prevarieties ST, MOD, AMT and GR. By Theorem 7 and Theorem 8,
this means that MeSCaL computes orbits for the classes TL(C), FL(C), PL(C)
and BPol(C) when C is among the aforementioned bases. Fortunately, there are
actually fewer classes to consider in practice, thanks to the following proposition.

**Proposition 17.** Let $\mathcal{G}$ be a group prevariety and $\alpha : A^* \to M$ be a surjective morphism. Let $\mathcal{C} \in \{\mathcal{G}, \mathcal{G}^+\}$ and $\mathcal{D} \in \{\text{BPol}(\mathcal{C}), \text{FL}(\mathcal{C}), \text{PL}(\mathcal{C}), \text{TL}(\mathcal{C})\}$. For every $e \in E(M)$ the *D*-orbit of $e$ for $\alpha$ is exactly the co-Pol($\mathcal{C}$)-orbit of $e$ for $\alpha$.

MeSCaL implements algorithms for computing co-Pol($\mathcal{G}$)- and co-Pol($\mathcal{G}^+$)-
orbits when $\mathcal{G} \in \{\text{ST}, \text{MOD}, \text{AMT}, \text{GR}\}$. For co-Pol(ST)-orbits, a simple special-
ized algorithm is used. For the other classes, MeSCaL relies on generic algorithms
based on $\mathcal{G}$-kernels and $\mathcal{G}^+$-orbits.
## 5.1 Computing co-Pol(ST)-orbits

Let $\alpha : A^* \to M$ be a morphism. For each idempotent $e \in E(M)$, we associate a subalphabet of $A$. The *alphabet of $e$* (for $\alpha$) consists of all letters $b \in A$ which label an edge inside the strongly connected component of $e$ within the right Cayley graph of $\alpha$. The following proposition describes the co-Pol(ST)-orbits.

**Proposition 18.** Let $\alpha : A^* \to M$ be a surjective morphism, $e \in E(M)$ and $B$ be the alphabet of $e$. The co-Pol(ST)-orbit of $e$ for $\alpha$ is $M_e = \{e\alpha(w)e \mid w \in B^*\}$. Moreover, for every $s, t \in M_e$,

- we have $s \leq_R t$ in $M_e$ if and only if there exists $u \in B^*$ such that $s\alpha(u) = t$.

- we have $s \leq_L t$ in $M_e$ if and only if there exists $v \in B^*$ such that $\alpha(v)s = t$.

## MeSCaL Optimization 6: Computation of co-Pol(ST)-orbits

**Proposition 18** provides an efficient procedure for computing the co-Pol(ST)-orbits. Let $e \in E(M)$. We want to compute its co-Pol(ST)-orbit $M_e \subseteq eMe$.

Computing the alphabet $B \subseteq A$ of $e$ is straightforward provided that we have the strongly connected components of the right Cayley graph in hand. This is the case in MeSCaL, as these are the $\mathcal{R}$-classes of $M$.

We restrict the left and right Cayley graphs of $\alpha$ by keeping the edges labeled by a letter in $B$ and discarding the others. We are able to compute the sets $\{e\alpha(w) \mid w \in B^*\}$ and $\{\alpha(w)e \mid w \in B^*\}$ by exploring these restrictions. By Proposition 18, $M_e$ is their intersection. The Green's relations of $M_e$ are given by the strongly connected components (obtained via Tarjan's algorithm).

## 5.2 General case

It was shown in [19,21] that if separation is decidable for a group prevariety $\mathcal{G}$, then it is also decidable for $\mathrm{Pol}(\mathcal{G})$, $\mathrm{Pol}(\mathcal{G}^+)$. This extends to co-Pol($\mathcal{G}$) and co-Pol($\mathcal{G}^+$) since separation for a class co-$\mathcal{D}$ reduces to separation for $\mathcal{D}$ ($H$ is co-$\mathcal{D}$-separable from $L$ if and only if $L$ is $\mathcal{D}$-separable from $H$). Hence, in this case, we have algorithms that compute the co-Pol($\mathcal{G}$)- and co-Pol($\mathcal{G}^+$)-pairs and, in turn, the co-Pol($\mathcal{G}$)- and co-Pol($\mathcal{G}^+$)-orbits.

In fact, the results of [19,21] imply that one can directly compute co-Pol($\mathcal{G}$)- and co-Pol($\mathcal{G}^+$)-pairs from the $\mathcal{G}$-kernel and the $\mathcal{G}^+$-orbits respectively. Here, we present these procedures and explain how they are implemented in MeSCaL.

**The classes co-Pol($\mathcal{G}$).** Consider a monoid $M$. A set of pairs $P \subseteq M^2$ is said to be *stable* if it is closed under multiplication: for all $(s, t), (s', t') \in P$, we have $(ss, tt') \in P$. The next theorem follows from results of [19,21].

**Theorem 19.** Let $\mathcal{G}$ be a group prevariety and $\alpha : A^* \to M$ be an onto morphism. The set of co-Pol($\mathcal{G}$)-pairs for $\alpha$ is the least stable set $P \subseteq M^2$ such that,

- $(\alpha(a), \alpha(a)) \in P$ for every $a \in A$, and,

- $(t, 1_M) \in P$ for all $t$ in the $\mathcal{G}$-kernel of $\alpha$.
By Theorem 19, computing co-Pol($\mathcal{G}$)-pairs reduces to graph traversal. The graph has vertices in $M^2$, with edges from each $(q, r) \in M^2$ to all $(q\alpha(a), r\alpha(a))$ for $a \in A$, and to $(qt, r)$ for each $t$ in the $\mathcal{G}$-kernel. According to Theorem 19, a pair $(q, r)$ is a co-Pol($\mathcal{G}$)-pair if and only if there is a path from $(1_M, 1_M)$ to $(q, r)$ in this graph. Yet, there are two drawbacks to this naive approach in practice:

1. There are $|M|^2$ vertices and $|M|^2 \times (|N|+|A|)$ edges (where $N$ is the $\mathcal{G}$-kernel).

2. Seemingly, we need the whole $\mathcal{G}$-kernel whereas the algorithms of MeSCaL are only efficient when the computation is restricted to regular elements. Fortunately, we are not interested in all co-Pol($\mathcal{G}$)-pairs, only in those required to compute orbits. For this reason, we may improve the procedure significantly.

Consider a group prevariety $\mathcal{G}$, a morphism $\alpha : A^* \to M$ and let $N \subseteq M$ be the $\mathcal{G}$-kernel of $\alpha$. For each idempotent $e \in E(M)$, we associate a graph $V_{\mathcal{G},\alpha}(e)$. Let $R_e \subseteq eM$ be the $\mathcal{R}$-class of $e$. The vertices of $V_{\mathcal{G},\alpha}(e)$ are the pairs in $R_e \times eM$. There are two kinds of edges. Let $(q, r) \in R_e \times eM$ be a vertex.

- For all $a \in A$ such that $q\alpha(a) \in \mathcal{R} e$, we add an edge $(q, r) \to (q\alpha(a), r\alpha(a))$.

- For all $t \in N$ such that $t \notin \mathcal{R} e$ and $qt \notin \mathcal{R} e$, we add an edge $(q, r) \to (qt, r)$.

**Corollary 20.** Let $\mathcal{G}$ be a group prevariety, $\alpha : A^* \to M$ be an onto morphism and $e \in E(M)$. The co-Pol($\mathcal{G}$)-orbit of $e$ for $\alpha$ consists of all elements $s \in eMe$ such that there is a path from $(e, e)$ to $(e, s)$ in $V_{\mathcal{G},\alpha}(e)$.

## MeSCaL Optimization 7: Computation of co-Pol($\mathcal{G}$)-orbits

Corollary 20 improves significantly on the above drawbacks. Computing the co-Pol($\mathcal{G}$)-orbit of $e \in E(M)$ is achieved by traversing a graph with $|R_e| \times |eM|$ vertices ($R_e$ is the $\mathcal{R}$-class of $e$). This is much smaller than $|M|^2$. In particular, recall that MeSCaL only computes one orbit per $\mathcal{J}$-class (see Lemma 10).

In order to compute the edges of $V_{\mathcal{G},\alpha}(e)$, MeSCaL precomputes all products $qt$ with $q \in \mathcal{R} e$ and $t \notin \mathcal{R} e$. This is achieved in time $O(|R_e| \times |J_e|)$ (where $J_e$ is the $\mathcal{J}$-class of $e$). This involves some Green's theory, since MeSCaL does not store multiplication tables: we only have the right Cayley graph.

Finally, observe that computing the whole co-Pol($\mathcal{G}$)-orbit of $e$ only requires the elements $t$ of the $\mathcal{G}$-kernel such that $t \notin \mathcal{R} e$: these are regular elements.

**The classes co-Pol($\mathcal{G}^+$).** The computation of co-Pol($\mathcal{G}^+$)-orbits is based on the next theorem which also follows from results of [19,21].

**Theorem 21.** Let $\mathcal{G}$ be a group prevariety and $\alpha : A^* \to M$ be an onto morphism. The set of co-Pol($\mathcal{G}^+$)-pairs for $\alpha$ is the least stable set $P \subseteq M^2$ such that,

1. $(\alpha(a), \alpha(a)) \in P$ for every $a \in A$, and,

2. $(t, f) \in P$ for all $f \in E(M)$ and $t$ in the $\mathcal{G}^+$-orbit of $f$ for $\alpha$.

A naive implementation of the algorithm from Theorem 21 suffers from the same drawbacks noted after Theorem 19 in the context of computing co-Pol($\mathcal{G}$)-orbits. We address these issues using the same strategy.

Let $\mathcal{G}$ be a group prevariety, $\alpha : A^* \to M$ be a morphism, and for each $f \in E(M)$, let $M_f \subseteq fMf$ denote the $\mathcal{G}^+$-orbit of $f$ for $\alpha$. For every idempotent $e \in E(M)$ and each root set $T$ for $\alpha$, we define a graph $V_{\mathcal{G},\alpha}^+(e, T)$. Let $R_e \subseteq eM$
be the $\mathcal{R}$-class of $e$. The vertices of $V_{\mathcal{G},\alpha}^{+}(e, T)$ are pairs in $R_e \times eM$, and edges
are defined as follows for each vertex $(q, r) \in R_e \times eM$:

- For all $a \in A$, if $q\alpha(a) \in \mathcal{R} e$, add an edge $(q, r) \to (q\alpha(a), r\alpha(a))$.

- For all $f \in T$ and $t \in M_f$, if $t \notin \mathcal{R} e$ and $qt \notin \mathcal{R} e$, add an edge $(q, r) \to (qt, rf)$.

**Corollary 22.** Let $\mathcal{G}$ be a group prevariety, $\alpha : A^* \to M$ be an onto morphism, $T$ be a root set for $\alpha$ and $e \in E(M)$. The co-Pol($\mathcal{G}^+$)-orbit of $e$ for $\alpha$ consists of all elements $s \in eMe$ such that there is a path from $(e, e)$ to $(e, s)$ in $V_{\mathcal{G},\alpha}^{+}(e, T)$.

## MeSCaL Optimization 8: Computation of co-Pol($\mathcal{G}^+$)-orbits

The implementation of Corollary 22 follows the same approach as discussed above for Corollary 20. Notably, it only requires the *regular elements* of the $\mathcal{G}^+$-orbits. Moreover, we only need the $\mathcal{G}^+$-orbits of the idempotents in a root set—which is exactly what MeSCaL computes (see Proposition 16).

## MeSCaL Optimization 9: Computation of Green's relations

Computing Green's relations for co-Pol($\mathcal{G}$)- and co-Pol($\mathcal{G}^+$)-orbits is nontrivial. They do not, in general, align with those of the original monoid—two elements may be $\mathcal{R}$-equivalent and regular in the monoid but not within a given orbit.

A naive approach is expensive: unlike syntactic monoids, we lack generators for the orbits. However, we want to implement two specific characterizations:

- For Theorem 7, the Green's relations restricted to *regular* elements suffice.

- For Theorem 8, we do not need the Green's relations.

Using Green's theory, one can efficiently identify which elements remain regular within a subsemigroup and compute the Green's relations restricted to them. In MeSCaL, this is implemented with time complexity $O(|M| \times \max)$, where $M$ is the original monoid and $\max$ is the maximum size of an $\mathcal{R}$- or $\mathcal{L}$-class.

# 6 Conclusion

In this paper, we presented optimizations for algorithms that compute information associated with a morphism, named its $\mathcal{C}$-orbits, where $\mathcal{C}$ is a prevariety. This information is instrumental in solving various membership problems. In MeSCaL, such precomputations are applied to test membership of classes of the form $\text{Op}(\mathcal{G})$ or $\text{Op}(\mathcal{G}^+)$, where $\mathcal{G}$ belongs to $\{\text{ST}, \text{MOD}, \text{AMT}, \text{GR}\}$ and where $\text{Op} \in \{\text{IPol}(\text{BPol}), \text{TL}, \text{FL}, \text{PL}, \text{IPol}(\text{BPol}_2), \text{TL}_2, \text{FL}_2, \text{PL}_2\}$.

This paper omits the classes built using the BPol operator. However, MeSCaL does implement membership tests for BPol($\mathcal{G}$) with $\mathcal{G} \in \{\text{ST}, \text{MOD}, \text{AMT}, \text{GR}\}$, as discussed in [25]. It also supports membership tests for BPol($\mathcal{G}^+$), based on a generic characterization from [20]. The implementation combines techniques from [25] (for BPol($\mathcal{G}$)) and from Section 4 (for computing $\mathcal{G}^+$-orbits). Also, MeSCaL implements membership for $\text{BPol}_2(\text{ST})$, using a characterization of [23]. This generalizes the approach used to compute co-Pol(ST)-orbits in Section 5.

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

1. Brzozowski, J.A., Cohen, R.S.: Dot-depth of star-free events. Journal of Computer and System Sciences 5(1), 1–16 (1971). https://doi.org/10.1016/S0022-0000(71)80003-X

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

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

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

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

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

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

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

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

10. 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/

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

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

13. Éric Pin, J., Weil, P.: Polynomial closure and unambiguous product. Theory of Computing Systems 30(4), 383–422 (1997)

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

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

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

17. Place, T., Zeitoun, M.: In orbit with MeSCaL: higher in concatenation and navigational hierarchies of regular languages, https://www.labri.fr/perso/zeitoun/research/pdf/mescal2.pdf, long version.

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

19. Place, T., Zeitoun, M.: Separation and covering for group based concatenation hierarchies. In: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 1–13. LICS’19 (2019). https://doi.org/10.1109/LICS.2019.8785655

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

21. Place, T., Zeitoun, M.: A generic polynomial time approach to separation by first-order logic without quantifier alternation. In: Dawar, A., Guruswami, V. (eds.) 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS’22. Leibniz International Proceedings in Informatics (LIPIcs), IARCS (2022). https://doi.org/10.4230/LIPIcs.FSTTCS.2022.43

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

23. Place, T., Zeitoun, M.: Dot-depth three, return of the J-class. In: Sobocinski, P., Lago, U.D., Esparza, J. (eds.) Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024. pp. 64:1–64:15. ACM (2024). https://doi.org/10.1145/3661814.3662082

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

25. Place, T., Zeitoun, M.: A first taste of MeSCaL, a tool for solving membership problems for 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)

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

27. Place, T., Zeitoun, M.: Navigational hierarchies of regular languages. In: Proceedings of the 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025 (2025), full version at https://arxiv.org/abs/2402.10080

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

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

30. 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
31. Trahtman, A.N.: A package TESTAS for checking some kinds of testability. CoRR abs/2105.12583 (2021), https://arxiv.org/abs/2105.12583