# Tree Algebras and Bisimulation-Invariant MSO on Finite Graphs

Thomas Colcombet, Amina Doumane, Denis Kuperberg

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

## To cite this version:

Thomas Colcombet, Amina Doumane, Denis Kuperberg. Tree Algebras and Bisimulation-Invariant MSO on Finite Graphs. ICALP, Jul 2025, Aarhus, Denmark. 10.4230/LIPIcs.ICALP.2025.152. [https://hal.science/hal-05392710v1](https://hal.science/hal-05392710v1)

HAL Id: hal-05392710

[https://hal.science/hal-05392710v1](https://hal.science/hal-05392710v1)

Submitted on 2 Dec 2025

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

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

<figure><img src="image_2.png" /></figure>
# Tree algebras and bisimulation-invariant MSO on finite graphs

Thomas Colcombet ☐^h>D

CNRS, IRIF, Université Paris Diderot, France

Amina Doumane ☐^h

CNRS, LIP, ENS Lyon, France

Denis Kuperberg ☐^h>D

CNRS, LIP, ENS Lyon, France

## Abstract

We establish that the bisimulation invariant fragment of MSO over finite transition systems is expressively equivalent over finite transition systems to modal µ-calculus, a question that had remained open for several decades.

The proof goes by translating the question to an algebraic framework, and showing that the languages of regular trees that are recognised by finitary tree algebras whose sorts zero and one are finite are the regular ones, ie. the ones expressible in µ-calculus. This corresponds for trees to a weak form of the key translation of Wilke algebras to omega-semigroup over infinite words, and was also a missing piece in the algebraic theory of regular languages of infinite trees for twenty years.

**2012 ACM Subject Classification** Theory of computation → Finite Model Theory; Theory of computation → Modal and temporal logics; Theory of computation → Algebraic language theory; Theory of computation → Regular languages

**Keywords and phrases** MSO, mu-calculus, finite graphs, bisimulation, tree algebra

**Digital Object Identifier** 10.4230/LIPIcs...

**Funding** Denis Kuperberg: ANR ReCiProg

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

<table><tr><td>1</td><td>Introduction</td><td>3</td></tr><tr><td>2</td><td>Set-systems and systems</td><td>5</td></tr><tr><td>2.1</td><td>Intuitions</td><td>5</td></tr><tr><td>2.2</td><td>Set-systems and systems</td><td>6</td></tr><tr><td>2.3</td><td>Morphisms of set-systems</td><td>8</td></tr><tr><td>2.4</td><td>Unfoldings and regular-trees</td><td>10</td></tr><tr><td>2.5</td><td>Yields of set-systems and yield-equivalence</td><td>11</td></tr><tr><td>2.6</td><td>Flattening</td><td>12</td></tr><tr><td>2.7</td><td>Unfold-equivalence is a congruence</td><td>14</td></tr><tr><td>2.8</td><td>Set-contexts, contexts, and their decomposition</td><td>15</td></tr><tr><td>2.9</td><td>Resolutions and flatten-resolutions</td><td>17</td></tr><tr><td>3</td><td>Algebras</td><td>22</td></tr><tr><td>3.1</td><td>Algebras</td><td>22</td></tr><tr><td>3.2</td><td>Languages and their recognition by algebras</td><td>23</td></tr><tr><td>3.3</td><td>MSO over systems and the composition method</td><td>24</td></tr><tr><td>4</td><td>Yield algebras</td><td>24</td></tr><tr><td>4.1</td><td>Yield-algebras</td><td>25</td></tr><tr><td>4.2</td><td>Syntactic yield-algebra for a language of regular-trees</td><td>26</td></tr><tr><td>4.3</td><td>Rankwise finite yield-algebras</td><td>28</td></tr><tr><td>5</td><td>The automaton property</td><td>32</td></tr><tr><td>5.1</td><td>Deterministic elements and deterministic yield-algebras</td><td>32</td></tr><tr><td>5.2</td><td>Rankwise finite syntactic yield-algebras have the automaton property</td><td>33</td></tr><tr><td>6</td><td>MSO, automata, bisimulation and μ-calculus</td><td>36</td></tr><tr><td>6.1</td><td>Transition systems as systems, and bisimulation</td><td>37</td></tr><tr><td>6.2</td><td>Monadic second-order logic, and the composition method</td><td>38</td></tr><tr><td>6.3</td><td>From algebra to automata in the unfold-invariant setting</td><td>39</td></tr><tr><td>6.4</td><td>The bisimulation-invariant case</td><td>41</td></tr><tr><td>7</td><td>Conclusion</td><td>43</td></tr></table>
# 1 Introduction

A well-known result of Janin and Walukiewicz states:

► **Theorem 1** ([14]). For a property of transition systems, the following statements are equivalent:

- being MSO-definable and bisimulation-invariant, and

- being $\mu$-calculus-definable<fnref n="1" />.

In which a property of transition systems is bisimulation-invariant if for any two bisimilar transitions systems, both satisfy the property, or none.

It is enlightening to see this result keeping in mind the following well known finite model property: two $\mu$-calculus sentences that can be separated by some transition system, can always be separated by a finite one. In other words, the semantics of a $\mu$-calculus sentence is entirely defined by what it expresses over finite transition systems. For this reason, the question whether a version of Theorem 1 for finite transition systems would hold is extremely natural. It remained an important open question in the field for almost three decades. One contribution of this paper is to provide a positive answer to it:

► **Theorem 2.** For a property of finite transition systems, the following statements are equivalent:

- being MSO-definable and bisimulation-invariant, and

- being $\mu$-calculus-definable.

For both Theorem 1 and Theorem 2, the upward direction is the same, and is the easy one. It follows from two well known facts: (1) $\mu$-calculus sentences can be effectively translated into equivalent MSO-sentences, and (2) properties definable in $\mu$-calculus are invariant under bisimulation.

The difficult direction is to show that bisimulation-invariant MSO-definable properties can be translated to equivalent $\mu$-calculus sentences. In the classical result of Janin and Walukiewicz, the crucial remark is that for all transition systems there exists a (potentially infinite) bisimilar one which is a tree. Thus the result amounts to show that if an MSO-definable property of (potentially infinite) trees is bisimulation-invariant, then it is $\mu$-calculus definable. This explains why the inner machinery of their proof relies, in the spirit of the seminal work of Rabin for binary trees [17], on a theory of automata over infinite trees (with unrestricted branching) that correspond in expressiveness to $\mu$-calculus.

This approach cannot be used in our case since, in general, finite transition systems are not bisimilar to any finite trees. This is problematic since in Theorem 2 we are given an MSO-sentence which is bisimulation-invariant over finite transition systems only, and thus, given a finite transition system, there is in general no tree which is equivalent on which we could try to analyse the semantics of the MSO-sentence<fnref n="2" />.

We adopt a different strategy. Our proof of the downward implication in Theorem 2 uses a translation of the problem to an algebraic formalism. From now on, all transition systems are assumed to be finite.

<footnote n="1">¹ In this work, $\mu$-calculus refers to the standard propositional modal $\mu$-calculus, i.e. the temporal logic constructed from propositions, modalities $\Box$ and $\diamond$, boolean connectives, and least and greatest fixpoints.</footnote>

<footnote n="2">² The fact that the tree automata approach fails in our case can be also be illustrated via an example. Indeed, it is possible to write an MSO-sentence which accepts a transition system if and only if it is a tree and has a branch of length $\omega$. This property is bisimulation-invariant over finite transition systems (since it accepts none of them). But it accepts all infinite trees. Thus, a $\mu$-calculus-definable property that would suit the conclusion of Theorem 2 has to be empty, and thus cannot coincide with the MSO formula over trees.</footnote>
XX:4 Tree algebras and bisimulation-invariant MSO on finite graphs

The first step is to extend the notion of transition system in order to be able to compose
them in a sufficiently powerful way. The generalized notion of transition systems we use
have a finite number of identified variables (that we can understand as exit vertices). Such
objects should be understood as pieces of transition systems that can be plugged in a context.
A system S with two free variables and a context C[□₂] as well as their composition are
illustrated below:

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

This approach gives rises to a notion of a multi-sorted algebra, in which we are considering,
for each finite set of variables $X = \{x_1, \dots, x_k\}$ the set of generalized transition systems that
would use variables in $X$. Up to now, this is classical and has been explored in various ways
[6, 3]. The novelty here is to extend this algebra by a kind of powerset construction, where
the interpretation of the union is a conjunction. We will also define two sets of starting
vertices: initial vertices which are used for composing with other elements, and roots that
will have the ability to “reset” the whole system and act as a global root in any context.
We then equip these extended algebra, called *yield-algebras*, with the usual composition
operations, associativity rules, Myhill-Nerode-like equivalence relation, etc.

If a language of transition systems is recognised by an MSO-sentence, then (by usual compositional method), its syntactic algebra is *rankwise finite*, i.e. the sort relative to each finite set of variables *X* is finite. We then show that its *syntactic yield-algebra* is also *rankwise finite* as well, and moreover has what we call the *automaton property*: every element behaves as a combination of elements of sorts 0 and 1. This in turn allows to design an automaton model equivalent to the original formula. If the language we started with is bisimulation-invariant, then this can be seen in the transition structure of the automaton, from which we can finally go back to the *μ*-calculus following arguments similar to [14].

Moreover, we can show that this transformation is effective, i.e. from an MSO-formula
that is assumed to be bisimulation-invariant on finite structures (though this property itself
is not decidable), we can compute the wanted μ-calculus formula.

**Related work**

**Bisimulation-invariant logics** The seminal Hennessy-Milner theorem [13] gives a first characterisation of modal logics via bisimulation-equivalence.

This was generalised to First-Order logic (FO) in [22]. The result was then transferred to
finite structures [19], and specialised to particular classes of finite structures [10, 12].

An intermediate logic strictly between FO and MSO, obtained by extending FO with
fixed-point operators, is considered in [16], where it is shown that the two-way bisimulation-
invariant fragment of this logic is equivalent to two-way $\mu$-calculus on finite structures.

Going to MSO, [14] gives the equivalence with μ-calculus on general structures. On finite structures, this equivalence is shown for structures of bounded Cantor-Bendixson rank in [5].

**Composition method and tree algebra** The composition method that we use here was pioneered in [11] for FO and used intensively for MSO in [20, 18].

There is a long line of research pursuing a well-behaved notion of algebra for regular languages of infinite trees [23, 15, 1, 7, 2].
Two-sorted algebras for regular trees are defined in [6], where the two sorts are closed trees and trees with 1 output, and MSO-definable composition operation. The formalism of $\omega$-hyperclones for tree algebras is proposed in [3], and is later shown in [8] to be somewhat ill-behaved with respect to regularity: there are example of rankwise finite algebras that define non-regular languages of infinite trees. Similarly, [4] shows that no distributive law exists in this framework. This is due to the fact that these algebras must treat non-regular trees, in the same way that $\omega$-semigroup must be able to evaluate words that are not ultimately periodic.

# Structure of the document

In Section 2 we provide definitions and properties of the objects we will manipulate, and in particular systems and set-systems as well as morphisms between them and other important tools for the development of this work. In Section 3, we define algebras, and describe the translation from MSO-definable to rankwise finite algebras. In Section 4, we define yield-algebras, and prove the key result of the section which is that the syntactic yield-algebras of a language of regular-trees recognisable by a rankwise finite algebra is also rankwise finite. In Section 5, we describe the core technical argument that will allow to translate rankwise finite yield-algebra to automata over infinite-trees. In Section 6, we show how this property indeed allows us to show that any language recognised by a rankwise finite algebra is regular in the classical sense. We also adapt this to the bisimulation-invariant setting to obtain an equivalent $\mu$-calculus formula.

The document is better read in electronic form since the use of notions is hyperlinked to their definition.

# 2 Set-systems and systems

## 2.1 Intuitions

A *ranked set* $\Sigma$ (or *alphabet*) is a family of sets $\Sigma_n$ indexed by naturals. We write $a \in \Sigma$ for $a \in \Sigma_n$ for some $n$. For $a \in \Sigma$, the *rank* of $\Sigma$, noted rk($a$), is the integer $n$ such that $a \in A_n$.

A *map of ranked sets* $f$ of $\Sigma$ to $\Gamma$ is a map that preserve the ranks, ie a family of maps $f_n: \Sigma_n \to \Gamma_n$ for all naturals $n$. A *ranked set* $\Sigma$ is *rankwise finite* if $\Sigma_n$ is finite for all $n$. An *ordered ranked set* is a ranked set $\Sigma$ together with an order on each $\Sigma_n$. A *map of ordered ranked set* is a map of ranked set which preserves the order.

► **Remark 3.** As defined here, *ranked sets* (resp. *ordered ranked set*) equipped with their maps form a category, that we call the *category of ranked sets* (resp. the *category of ordered ranked sets*).

We fix an infinite set $Vars = \{x_1, x_2, \dots\}$ of variables. Variables can be seen as having rank 0. For $n \in \mathbb{N}$, we denote $[n]$ the set $\{1, \dots, n\}$, and $Vars[n]$ the variables $\{x_1, \dots, x_n\}$.

The central notion here is the one of *$\Sigma$-set-system*. It is illustrated in Figure 1. They are a more general version of the more usual notion of *system*, which itself abstracts the notion of *transition system*.

- At high level, *set-systems* consists of finite sets of vertices, to each vertex is attached a symbol of some rank $k$, and the vertex is then connected to $k$ different directions. In the set-system version, to each direction is associated a set of possible successor vertices. In the simpler systems, there is only one. The complete definition also has initial vertices, root vertices, and variables, see Section 2.2.
XX:6 Tree algebras and bisimulation-invariant MSO on finite graphs

Let us emphasize that [set-]systems are finite. This is a key feature in this work since our
goal is to understand the expressive power of MSO over finite graphs.

- One way to see systems is as representing infinite regular trees over a ranked alphabet in a folded way. The represented tree is obtained via the usual notion of unravelling. We shall never perform such a complete unravelling since our systems have to remain finite. Instead, systems are considered modulo (partial) unfolding, and regular trees correspond to an equivalence class of systems under the generated unfold-equivalence.

- Set-systems in their general form are of a non-deterministic nature: there may be several initial vertices, and several successors when advancing through a symbol in a particular direction. They also have a set of root vertices. The intuition here is similar to the case of systems, but instead of 'representing' a unique infinite tree, it would represent a set of them. Hence the name set-system. This is formalized using the concept of resolution: a resolution of a set-system is a system that could be produced by resolving the non-deterministic choices.

- Another orthogonal aspect of these objects is that [set-]systems use variables and initial vertices. These are used as handles for composing several [set-]systems into more complex ones. When 'composing', the general idea is to connect a variable (which is a descriptor of a possible 'exit' of the system) to an initial vertex (which is describing 'entry points' of the system). This ability to combine systems together equips systems with an algebraic structure. This is formalised using the flatten operation, which is a building tool for combining systems together. See Section 2.6.

2.2 Set-systems and systems

In this section, we define the notions of systems (the natural model), and of set-systems (that generalizes it with a form of non-determinism and a notion of root).

<figure><img src="image_5.png" /><figcaption>■ **Figure 1** A Σ-set-system $S_1$ and a Σ-system $S_2$, both over variables $\{x_1, x_2\}$ (ie of rank 2), for Σ containing symbols $b_1$ of rank 1, $a_2$ of rank 2, and $c_3$ of rank 3. The topmost outgoing edge of a symbol has direction 1, the next one 2, and so on. The circle $\circ$ denotes an initial vertex, the symbol $\searrow$ denotes a root vertex, and $\diamond$ emphasizes the presence of multiple successors in the same direction. Implicitly, edges are directed from left to right unless explicitly using an arrow notation.</figcaption></figure>

► **Definition 4 (set-systems).** Given a ranked set $\Sigma$, a $\Sigma$-set-system of rank $n$, $S = (V_S, Vi_S, Vr_S, \text{label}_S, \text{Edges}_S)$, consists of

- a *finite set* of *of vertices* $V$,

- a set of initial vertices $Vi \subseteq V$,

- a set of root vertices $Vr \subseteq V$,

- a labelling function $\text{label}: V \to \Sigma$; in practice, we simply write $S(s)$ for $\text{label}(s)$,

- an edge relation $\text{Edges} \subseteq V \times \mathbb{N} \times (V \uplus \{x_1, \dots, x_n\})$ consisting of edges of the form $(v, d, f)$ with $d \in [\text{rk}(S(v))]$; $d$ is called the direction of the edge; if $f$ is a vertex, then $(v, d, f)$ is called a transition edge; otherwise $f$ is a variable and $(v, d, f)$ is a variable edge. We also denote $\text{Edges}(v)$ the set $\{(d, f) \mid (v, d, f) \in \text{Edges}\}$, and $\text{Edges}(v, d) = \{f \mid (v, d, f) \in \text{Edges}\}$.
A $\Sigma$-set-system is closed if it has rank 0. Two $\Sigma$-set-systems $S, S'$ are of same shape if they differ only on their labelling, ie $V_S = V_{S'}$, $V_i_S = V_{iS'}$, $Vr_S = V_{rS'}$, and $Edges_S = Edges_{S'}$.

Given a map of ranked sets $\eta$ from $\Sigma$ to $\Gamma$, we denote $\bar{\eta}$ the map from $\Sigma$-set-systems to $\Gamma$-set-systems that sends $S$ to $\bar{\eta}(S) = (V_S, V_{iS}, V_{rS}, \eta \circ \text{label}_S, Edges_S)$.

We may drop the mention of the alphabet $\Sigma$, and simply talk about set-systems. The variables used in a [set-]system of rank $n$ are $x_1, \dots, x_n$. We sometimes use other variable names $x, y, z$ for convenience if there is no ambiguity about the meaning.

**Definition 5 (systems).** A $\Sigma$-system $T$ is a $\Sigma$-set-system such that $V_iS$ is a singleton, $V_rS$ is empty, and for all vertices $v \in V_S$ and all directions $d \in [\text{rk}(\text{label}(v))]$, $Edges_S(v, d)$ is a singleton.

**Remark 6 (the nature of set-systems).** If we forget about root vertices, it is almost valid to think about $\Sigma$-set-systems of rank $n$ as co-algebras for the set functor $SS: X \mapsto \mathcal{P}(\text{Vars}[n] + \sum_{a \in \Sigma} X^{\text{rk}(a)})$. The only subtlety is informally that set-systems are "not allowed to have variables at the first level". This aspect appears in the fact that variables can appear as target of edges, but not as initial vertices$^3$, and could be simulated using a functor of set$^2$. If we keep this intuition, then the notion of morphisms to be introduced in the next section corresponds to the classical morphisms of co-algebras.

In the same way, $\Sigma$-systems of rank $n$ can be understood as co-algebras for the set functor $S: X \mapsto \text{Vars}[n] + \sum_{a \in \Sigma} X^{\text{rk}(a)}$, under the same caveat. Again morphisms are consistent with this interpretation.

However, the notion of root vertices of set-systems does not fit nicely in this description, and has a more algebraic nature similar to the initial state of word automata seen as algebras. The notion of morphisms also fit with this intuition.

**Remark 7 (category of set-systems and systems).** For $\Sigma$ fixed, the $\Sigma$-set-systems form a ranked set, denoted Set-systems($\Sigma$). Furthermore, the lifting of maps of ranked sets, $f \mapsto \bar{f}$ turns Set-systems into an endofunctor of the category of ranked sets. The ranked set Systems($\Sigma$) is defined in the same way. As above, Systems is an endofunctor of the category of ranked sets, and more precisely a subfunctor of Set-systems.

We conclude this section with the introduction of some operations and notations useful for the development of this work.

- The $\Sigma$-set-system uproot($S$) is $(V_S, V_{rS}, \emptyset, \text{label}_S, Edges_S)$. It consists in forgetting the initial vertices, and transforming root vertices into initial ones. This definition shall be used for describing the semantics of root vertices (namely root yields).

- The $\Sigma$-set-system plant($S$) is $(V_S, \emptyset, V_{rS} \cup V_{iS}, \text{label}_S, Edges_S)$. If we interpret initial vertices as the cuts of a branches of a tree, then planting amounts to put them in the ground, thus turning them into roots. We shall also apply plant to set of systems, with the expected meaning.

- Given two $\Sigma$-set-systems of same rank $S$ and $S'$, then $S + S'$ is their disjoint unions (defined in the natural way).

- Given a binary relation $R \subseteq [m] \times [n]$, and a set-system $S$ of rank $m$, we denote $\hat{R}(S)$ the set-system which is identical to $S$, but for the variable edges that are defined by $(r, i, x_j) \in Edges_{\hat{R}(S)}$ if $(k, j) \in R$ and $(r, i, x_k) \in Edges_S$ for some $k \in [m]$. As a particular

<footnote>$^3$ This is technically similar to not allowing the empty words when reasoning with words of length $\omega$. A typical problem is for instance that, in general, constructing the $\omega$-iteration $u^\omega$ of a finite word $u$ yields a word of length $\omega$, except for the empty word $\varepsilon$, for which $\varepsilon^\omega = \varepsilon$.</footnote>
XX:8 Tree algebras and bisimulation-invariant MSO on finite graphs

case, for $\sigma: [m] \rightarrow [n]$, $\hat{\sigma}$ turns set-systems of rank $m$ into set-systems of rank $n$ (it preserves the systems), and $\sigma^{-1}$ turns set-systems of rank $n$ into set-systems of rank $m$ (however, note that it does not preserve systems in general).

For the sake of writing examples, we shall sometimes denote set-systems as expressions. The main notation is that, given a symbol $a \in \Sigma$ of rank $n$, and $S_1, \dots, S_n$ that are either set-systems of rank $m$ or variables in $\text{Vars}[m]$, $a(S_1, \dots, S_n)$ is the set-system obtained as expected: it has a single new vertex which is initial and labelled $a$, which is connected in direction $d$ to either a variable $y$ if $S_d = y$, or to all the initial vertices of a fresh copy of $S_d$ otherwise (initial vertices in $S_d$ are not initial anymore in the copy). This notation is consistent with what one expects for finite trees: for instance $a_2(x_1, a_2(b, x_2))$ denotes the expected system of tree shape.

2.3 Morphisms of set-systems

The morphisms will be key in the development of this work. Other notions such as unfoldings, unfold-equivalence, and yields derive from them. In fact, we somehow already silently used them in the previous section since operations such as the disjoint union are implicitly defined “up to isomorphism”.

► **Definition 8.** Given two $\Sigma$-set-systems $S$ and $S'$ of same rank, a morphism from $S$ to $S'$ is a map $\eta: V_S \to V_{S'}$ such that

$\eta(\mathrm{Vi}_S) \subseteq \mathrm{Vi}_{S'}$,

$\eta(\mathrm{Vr}_S) \subseteq \mathrm{Vr}_{S'}$,

$\tilde{\eta}(\mathrm{Edges}_S) \subseteq \mathrm{Edges}_{S'}$ where $\tilde{\eta}$ is the extension to edges of $\eta$, ie $\tilde{\eta}(v, d, v') = (\eta(v), d, \eta(v'))$, if $v' \in V$, and $\tilde{\eta}(v, d, y) = (\eta(v), d, y)$ for $y \in \text{Vars}$.

It is locally surjective if $\eta(\mathrm{Vi}_S) = \mathrm{Vi}_{S'}$, $\eta(\mathrm{Vr}_S) = \mathrm{Vr}_{S'}$, and $\tilde{\eta}(\mathrm{Edges}_S(v)) = \mathrm{Edges}_{S'}(\eta(v))$ for all $v \in V_S$.

A first consistency check in the definition of morphisms is their closure under composition.

**Lemma 9 (composition).** If $\eta$ is a morphism of set-systems from $S$ to $S'$, and $\eta'$ is a morphism of set-systems from $S'$ to $S''$, then $\eta' \circ \eta$ is a morphism of set-systems from $S$ to $S''$. If $\eta$ and $\eta'$ are locally surjective then $\eta' \circ \eta$ is also locally surjective.

In many proofs we shall concentrate on initial vertices only rather than root vertices. The following remark explains why many arguments involving initial vertices directly transfer to root vertices.

**Remark 10.** If $\eta$ is a [locally surjective] morphism from $S$ to $S'$, then it is also a [locally surjective] morphism from $\mathrm{uproot}(S)$ to $\mathrm{uproot}(S')$. It is also a [locally surjective] morphism from $\mathrm{plant}(S)$ to $\mathrm{plant}(S')$

The morphisms admit pullbacks. We will use this as a technical tool.

**Lemma 11 (pullbacks).** Let $S, S', T$ be $\Sigma$-set-systems, and $\eta: S \to T$, $\eta': S' \to T$ be morphisms, there exist a $\Sigma$-set-system $P$ and morphisms $\pi: P \to S$ and $\pi': P \to S'$ such that $\eta \circ \pi = \eta' \circ \pi'$, and $P$ is universal with this property, ie, for all $\Sigma$-set-systems $U$ and morphisms $\tau: U \to S$ and $\tau': U \to S'$, if $\eta \circ \tau = \eta' \circ \tau'$, then there exists a unique morphism $\theta: U \to P$ such that $\tau = \pi \circ \theta$ and $\tau' = \pi' \circ \theta$.
<figure><img src="image_6.png" /></figure>

Furthermore, if $\eta$ is locally surjective, then $\pi'$ is also locally surjective.

**Proof.** Let $S, S', T$ be $\Sigma$-set-systems and $\eta: S \to T, \eta': S' \to T$ be morphisms. We construct the new $\Sigma$-set-system $P = (V_P, Vi_P, Vr_P, \text{label}_P, \text{Edges}_P)$ as follows:

- $V_P := \{(v, v') \in V_S \times V_{S'} | \eta(v) = \eta'(v')\}$,

- $Vi_P := \{(v, v') \in Vi_S \times Vi_{S'} | \eta(v) = \eta'(v')\}$,

- $Vr_P := \{(v, v') \in Vr_S \times Vr_{S'} | \eta(v) = \eta'(v')\}$,

- $\text{label}_P(v, v') := \text{label}_S(v) (= \text{label}_T(\eta(v)) = \text{label}_T(\eta'(v') = \text{label}_{S'}(v')))$,

- there is a transition edge $((v, v'), d, (w, w')) \in \text{Edges}_P$ if $(v, d, w) \in \text{Edges}_S$ and $(v', d, w') \in \text{Edges}_{S'}$, and

- there is a variable edge $((v, v'), d, y) \in \text{Edges}_P$ if $(v, d, y) \in \text{Edges}_S$ and $(v', d, x) \in \text{Edges}_{S'}$. We define the morphisms of set-systems $\pi: P \to S$ and $\pi': P \to S'$ to be the projections on the first, and the second component respectively. It is straightforward to check that these are indeed morphisms and that $\eta \circ \pi = \eta' \circ \pi'$.

Let us show that it is universal with this property. Let us consider some $\Sigma$-set-system $U$ together with morphisms $\tau: U \to S$ and $\tau': U \to S'$ such that $\eta \circ \tau = \eta' \circ \tau'$. Define now $\theta: U \to P$ by $\theta(u) = (\tau(u), \tau'(u))$ for all $u \in V_U$. Since $\eta(\tau(u)) = \eta'(\tau'(u))$, we indeed have $(\tau(u), \tau'(u)) \in V_P$. Hence $\theta$ is indeed a morphism such that $\tau = \theta \circ \pi$ and $\tau' = \theta \circ \pi'$. Furthermore, this $\theta$ is unique. Indeed, assume the existence of a morphism $\rho$ from $U$ to $P$ such that $\tau = \rho \circ \pi$ and $\tau' = \rho \circ \pi'$, and consider some vertex $u$ in $U$. Let $(v, v') := \rho(u) \in V_P$. Since $\tau = \rho \circ \pi$ and by definition of $\pi$ and $\theta$, we have $v = \pi(v, v') = \pi(\rho(v)) = \tau(u)$. In the same way, $v' = \tau'(u)$. Overall $\rho(u) = (\tau(u), \tau'(u))$ so $\rho = \theta$.

Let us finally show that if $\eta$ is locally surjective, then $\pi'$ also is. The interesting case is, for $u \in V_P$, the surjectivity of $\tilde{\pi}'$ from $\text{Edges}_P(u)$ onto $\text{Edges}_{S'}(\pi(u))$. By definition of $V_P$, $u = (v, v')$ with $\eta(v) = \eta'(v')$. Let $(v', d, w') \in \text{Edges}_{S'}(v')$. Since $\eta'$ is a morphism, $(\eta'(v'), d, \eta'(w')) \in \text{Edges}_T(\eta'(v'))$. Since $\eta(v) = \eta'(v')$ and using the local surjectivity of $\eta$, there exists $(v, d, w) \in \text{Edges}_S(v)$ such that $\tilde{\eta}(v, d, w) = (\eta(v), d, \eta'(w'))$. Hence, by definition of $\text{Edges}_P$, $((v, v'), d, (w, w')) \in \text{Edges}_P(v)$ and is such that $\tilde{\pi}'((v, v'), d, (w, w')) = (v', d, w')$. Hence $\tilde{\pi}'$ is surjective from $\text{Edges}_P(u)$ onto $\text{Edges}_{S'}(\pi(u))$. $\quad \blacksquare$

Our morphisms are defined from a given rank to the same one. The following lemma is a tool for transforming morphisms between set-systems of a rank into morphisms between set-systems of another rank.

**Lemma 12.** Given a set-system $S$ of rank $m$, a set-system $S'$ of rank $n$, and a map $\sigma: [m] \to [n]$, then, for a map $\rho$ from vertices of $S$ to vertices of $S'$, the following properties are equivalent

- $\rho$ is a morphism from $\hat{\sigma}(S)$ to $S'$, and

- $\rho$ is a morphism from $S$ to $\hat{\sigma^{-1}(S')}$.

**Proof.** Assume $\rho$ is a morphism from $\hat{\sigma}(S)$ to $S'$. The only thing we have to check is for variable edges. Consider a variable edge $(s, i, x_j) \in \text{Edges}_S$. This implies that $(s, i, x_{\sigma(j)}) \in \text{Edges}_{\hat{\sigma}(S)}$. Hence, by morphism, $(\rho(s), i, x_{\sigma(j)}) \in \text{Edges}_{S'}$. And thus $(\rho(s), i, x_j) \in \text{Edges}_{\hat{\sigma^{-1}(S')}}$.
XX:10 Tree algebras and bisimulation-invariant MSO on finite graphs

Assume $\rho$ is a morphism from $S$ to $\sigma^{-1}(S')$. The only thing we have to check is for variable edges. Consider a variable edge $(s, i, x_j) \in Edges_{\hat{\sigma}(S)}$. By definition, of $\hat{\sigma}$, there is a variable edge $(s, i, x_k) \in Edges_S$ with $j = \sigma(k)$. Since $\rho$ is a morphism, $(\rho(s), i, x_k) \in Edges_{\sigma^{-1}(S')}$. Hence, by definition of $\sigma^{-1}$ there is variable edge $(\rho(s), i, x_j) \in Edges_{S'}$. ◀

## 2.4 Unfoldings and regular-trees

If we specialize morphisms to $\Sigma$-systems we obtain the notions of unfolding and then of unfold-equivalence. The notion of regular-tree shall then be understood as an unfold-equivalence class of systems.

Definition 13 (unfolding). If there is a morphism of set-systems from a $\Sigma$-system $T$ to another one $T'$, then $T$ is called an unfolding of $T'$, and $T'$ a folding of $T$.

Remark 14. Note that if there is a morphism $\eta$ from a system $T$ to a system $T'$, then it is locally surjective.

We shall reason about systems “modulo unfolding”, and this argument is simplified by the following lemma.

**Lemma 15.** *The binary relation between $\Sigma$-systems "being unfoldable to a common $\Sigma$-system" is an equivalence relation.*

*Proof.* Reflexivity and symmetry are straightforward. For transitivity, assume $T, T'$ both unfold to $S$ and $T', T''$ both unfold to $S'$. By Lemma 11, since $T'$ unfolds to both $S, S'$$, there exists $P$ to which $S$ and $S'$ both unfold. Hence by composition of morphisms, $T$ and $T''$ both unfold to $P$. The relation is transitive. ◀

The previous lemma justifies the following definition.

Definition 16. Two $\Sigma$-systems that have a common unfolding are called unfold-equivalent$^4$. A $\Sigma$-regular-tree is an unfold-equivalence class of $\Sigma$-systems.

This is illustrated in Figure 2.

<figure><img src="image_7.png" /><figcaption>Figure 2 $S_1$ and $S_2$ are unfold-equivalent, $F$ is a common folding of both, and $U$ a common unfolding of both.</figcaption></figure>

Remark 17. Note that if one would “fully unfold” a system (as is classically done), one would obtain an infinite tree which is “regular in the classical sense” (a finite number of subtrees), and that all regular trees (in the classical sense) can be obtained as the “full unfolding” of some system. It is also easy to check that two systems are unfold-equivalent if and only if they have isomorphic “full unfoldings”. Hence, the map which to a regular tree (in the classical sense) associates the set of systems that fully unfold to it is a bijection between regular trees (in the classical sense) and regular-trees as defined in this work.

<footnote>$^4$ This is indeed an equivalence by Lemma 15.</footnote>
► **Remark 18.** If a system $T$ has some unreachable vertices (ie unreachable from the initial vertex by following the transition edges), one could define its “trimmed” version $T'$ in which these unreachable vertices have been removed. In this case, the identity seen as an injective map from $T'$ to $T$, is a morphism, and hence $T$ and $T'$ are unfold-equivalent.

Let us conclude this section with a technical lemma.

► **Lemma 19.** Let $\sigma: [m] \to [n]$. Let $T$ be a system of rank $m$ and $T'$ be a system of rank $n$ which is an unfolding of $\hat{\sigma}(T)$. There exists an unfolding $T''$ of $T$ such that $\hat{\sigma}(T'') = T'$.

**Proof.** Let $\eta$ be the morphism from $T'$ to $\hat{\sigma}(T)$. We define $T''$ to be identical to $T'$, but for the fact that there is a variable edge $(v, d, y) \in Edges_{T''}$ if and only if there is a variable edge $(\eta(v), d, y)$ in $T$. One easily checks that (1) $T''$ is a system, (2) $\eta$ is a morphism from $T''$ to $T$, and (3) $\hat{\sigma}(T'') = T'$.

## 2.5 Yields of set-systems and yield-equivalence

We have seen so far that systems can be dealt with modulo unfold-equivalence. We shall now see how set-systems can be understood as “finite-non-deterministic machines that would non-deterministically produce systems”. Again, these notions derive from morphisms. This defines the notion of init yields which are systems produced starting from some initial vertex, and root yields which correspond to systems produced from a root vertex. Two set-systems are yield-equivalent if they agree on their yields. An important tool developed in this section is that the existence of a morphism entail the inclusion of yields, and their equality if it is locally surjective morphism of set-systems (see Lemma 25).

Our first definition formalizes what is ‘produced’ by a set-system: its yields.

► **Definition 20.** Let $S$ be a set-system. A direct resolution of $S$ is a system $T$ such that there exists a morphism from $T$ to $S$. An init-yield of $S$ is a system that unfolds to a direct resolution of $S$. A root-yield<fnref n="5" /> of $S$ is a set-system of the form plant($T$) for $T$ an init-yield of uproot($S$). A yield is either a root-yield or an init-yield. We set:

$$ \text{InitYields}(S) = \{T \mid T \text{ init-yield of } S\} \quad \text{and} \quad \text{RootYields}(S) = \{T \mid T \text{ root-yield of } S\}. $$

Let<fnref n="6" /> $\text{Yields}(S) = \text{InitYields}(S) \cup \text{RootYields}(S)$. Given $\Sigma$-set-systems $S$ and $S'$ of same rank, $S \subseteq^\text{yields} S'$ if $\text{Yields}(S) \subseteq \text{Yields}(S')$. Furthermore, $S$ and $S'$ are yield-equivalent (also written $S =^\text{yields} S'$) if $S \subseteq^\text{yields} S'$ and $S \supseteq^\text{yields} S'$.

► **Remark 21.** Since the set of direct resolutions is closed under unfolding, $\text{InitYields}(S)$ and $\text{RootYields}(S)$ are closed under unfold-equivalence.

► **Remark 22.** Two systems are unfold-equivalent (as systems) if and only if they are yield-equivalent (as set-systems).

► **Example 23.** In Figure 1, the system $S_2$ is a direct resolution of $S_1$.

Let us now study the nature of locally surjective morphisms and how morphisms entail the inclusion of yields. Lemma 24 is a technical step needed for Lemma 25.

<footnote n="5">⁵ When definitions are unravelled, init-yields begin in an initial vertex, and root-yields begin in a root vertex.</footnote>

<footnote n="6">⁶ Note that there is no possible confusion between elements in $\text{InitYields}$ and $\text{RootYields}$.</footnote>
XX:12 Tree algebras and bisimulation-invariant MSO on finite graphs

**Lemma 24.** If there is a locally surjective morphism from a set-system $S$ to a system $T$, then $T$ unfolds to a direct resolution of $S$.

**Proof.** Let $\eta$ be the locally surjective morphism from $S$ to $T$. We assume some fixed linear order on the vertices of $S$.

We define $T'$ as identical to $S$ but for the following changes:

- Since $\eta$ is locally surjective, $\eta(Vi_T) = Vi_T$, which is a singleton since $T$ is a system. Hence $Vi_T$ is not empty. It is meaningful to set $Vi_{T'} = \{\min(Vi_S)\}$.

- Let $v$ be a vertex of $S$ and $d \in [\mathrm{rk}(S(v))]$ be a direction. Since $\eta$ is locally surjective, $\tilde{\eta}(\mathrm{Edges}_S(v, d)) = \mathrm{Edges}_T(\eta(v), d)$ which is a singleton since $T$ is a system. Let $(\eta(v), d, f)$ be the only edge in $\mathrm{Edges}_T(\eta(v), d)$. Two cases may occur:

- If $(\eta(v), d, f)$ is a variable edge of $T$, then $(v, d, f)$ is also a variable edge of $S$ for some variable $y$, and we put $(v, d, y) \in \mathrm{Edges}_{T'}$.

- If $(\eta(v), d, f)$ is a transition edge of $T$, then there is at least one $w$ such that $(v, d, w) \in \mathrm{Edges}_S$. We insert the edge $(v, d, w')$ in $\mathrm{Edges}_{T'}$ for $w'$ the least such $w$.

The way it is defined, it should be clear that $T'$ is a system, that it is an unfolding of $T$ witnessed by the morphism $\eta$, and that it is a direct resolution of $S$ witnessed by the identity map.

**Lemma 25.** If there is a morphism of $\Sigma$-set-systems from $S$ to $S'$, then $S \subseteq^{\mathrm{yields}} S'$. If furthermore it is locally surjective then $S =^{\mathrm{yields}} S'$.

*Proof.* Let $\eta$ be the morphism from $S$ to $S'$.

Consider some direct resolution $T$ of $S$, witnessed by a morphism $\rho$ from $T$ to $S$. Then $\eta \circ \rho$ is a morphism witnessing that $T$ is a direct resolution of $S'$. It follows that $\mathrm{InitYields}(S) \subseteq \mathrm{InitYields}(S')$. Using the trick of Remark 10, we get $S \subseteq^{\mathrm{yields}} S'$.

For the second part, let us assume furthermore that $\eta$ is locally surjective. Let $T$ be a direct resolution of $S'$ witnessed by the morphism $\rho$ from $T$ to $S'$. Using Lemma 11, there exists a set-system $P$ and morphisms $\pi: P \to S$ and $\pi': P \to T$, such that $\eta \circ \pi = \rho \circ \pi'$. Furthermore, since $\eta$ is locally surjective, $\pi'$ is also locally surjective. Hence, by Lemma 24 applied to $P$ and $T$, $T$ unfolds to some direct resolution $T'$ of $P$. Hence, there is a morphism from $T'$ to $P$, and hence also to $S$. Thus $T'$ is a direct resolution of $S$. This is shown in the following drawing:

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

Again using the trick of Remark 10, we get $S' \subseteq^{\mathrm{yields}} S$, and hence $S =^{\mathrm{yields}} S'$.

## 2.6 Flattening

We describe in this section the operations used for constructing complex set-systems out of simpler ones. In particular, the notion of context and application of a context to a system derive from it. The general idea is to perform the disjoint union of systems, connecting variables of subsystems to initial vertices of others according to a pattern. The operation for this is *flatten* that we define below.

It is better explained through an example first.
**► Example 26.** The following illustration shows a set-system of set-systems and its flattening. The subsystems are drawn inside the dashed boxes, and boxes are organised in an outer system structure called the pattern. Direction names for edges going out of a node $v$ will always be implicit, the topmost one being 1, then 2, and so on, ending with rk(`label(v)`) for the bottommost.

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

As is shown in Example 26, the `flatten` operation glues the subsystems together, keeping their internal structures. If an edge of a subsystem ends in a variable $x_d$, then it is connected instead to all the initial vertices of the subsystems reachable following direction $d$ in the pattern, as well as to the variables reachable following direction $d$. After flattening, the initial vertices are the initial vertices of the subsystems that were themselves initial vertices in the pattern. Root vertices are treated very differently. Root vertices from subsystems remain root vertices during the process, while initial vertices of subsystems that are root get to be promoted to be roots.

Formally, we already noted that $\Sigma$-set-systems do form a ranked set. Hence, the notion of $(\Sigma$-set-system)-set-systems is meaningful. The `flatten` operation maps $(\Sigma$-set-system)-set-systems to $\Sigma$-set-systems, and is defined as follows.

**► Definition 27 (flattening).** Given a $(\Sigma$-set-system)-set-system $S = (V, Vi, Vr, label, Edges)$ with $S(v) := (V_v, Vi_v, Vr_v, label_v, Edges_v)$, we define `flatten$(S) := (V'_v, Vi'_v, Vr'_v, label'_v, Edges'_v)$` where:

- $V' := \{(v, w) | v \in V, w \in V_v\}$,

- $Vi' := \{(v, w) | v \in Vi, w \in Vi_v\}$,

- $Vr' := \{(v, w) | v \in V, w \in Vr_v\} \cup \{(v, w) | v \in Vr, w \in Vi\}$,

- $label'(v, w) := label_v(w)$,

- The definition of $Edges'$ identifies three distinct cases:

$$ 
\begin{align*}
Edges' &:= \{((v, w), d, (v, w')) | (w, d, w') \in Edges_v\} && \text{(intra-subsystem)} \\
      &\cup \{((v, w), d, (v', w')) | (w, d, x_e) \in Edges_v, x_e \in \text{Vars}, (v, e, v') \in Edges, w' \in Vi_v\} && \text{(inter-subsystem)} \\
      &\cup \{((v, w), d, y) | (w, d, x_e) \in Edges_v, x_e \in \text{Vars}, (v, e, y) \in Edges, y \in \text{Vars}\} && \text{(variable)}
\end{align*}
$$

We can also use `flatten` for systems as justified by the following lemma.

**► Lemma 28.** The flattening of a $(\Sigma$-system)-system is a $\Sigma$-system.

Let us also provide two simple results stating that morphisms behave well with respect to flattening.

**► Lemma 29.** Given $(\Sigma$-set-system)-set-systems $S, S'$ of same shape such that there is a set-system morphism $\eta_v$ from $label_S(v)$ to $label_{S'}(v)$ for all $v \in V_S$. Then $\eta$ defined as $\eta(v, w) = (v, \eta_v(w))$ is a morphism from `flatten$(S)$` to `flatten$(S')$`. Furthermore if $\eta_v$ is locally surjective for all $v$, then $\eta$ is locally surjective.
XX:14 Tree algebras and bisimulation-invariant MSO on finite graphs

**Proof.** Simple verification.

**Lemma 30.** Let $S, S'$ be two $(\Sigma\text{-set-system)}$-set-systems, and $\eta$ be a morphism from $S$ to $S'$, then $\eta'$ defined by $\eta'(v, w) = (\eta(v), w)$ is a morphism from $\text{flatten}(S)$ to $\text{flatten}(S')$. Furthermore, if $\eta$ is locally surjective then $\eta'$ is locally surjective.

**Proof.** Simple verification.

We also define the unit operation, which, given $a \in \Sigma$ builds a $\Sigma$-system unit($a$) of rank $rk(a)$ in a natural way. Formally, $\text{unit}(a) = ((\{*\}, \{*\}, \emptyset, \text{label}, \text{Edges})$, where $\text{label}(*) = a$, and $\text{Edges} = \{(*, i, x_i) | i \in [rk(a)]\}$.

The following lemma shows that the identities defining a monad are satisfied.

**Lemma 31.** For all $((\Sigma\text{-set-system)}\text{-set-system})$-set-systems $S_3$ and all $\Sigma$-set-systems $S_1$, we have

$$ \text{flatten} \circ \text{flatten}(S_3) = \text{flatten} \circ \overline{\text{flatten}}(S_3), $$

$$ \text{flatten} \circ \overline{\text{unit}}(S_1) = S_1 $$

$$ \text{and} \quad \text{flatten} \circ \text{unit}(S_1) = S_1. $$

**Remark 32.** What we have shown so far is that the operations *flatten* and *unit* are natural transformations that equip the set-system functor of a monad structure. We call it the *monad of set-systems*. For systems, it defines similarly the *monad of systems*.

We end this section with a technical tool: the *uproot* operation was used for defining *RootYields*. We introduce here the companion operation, *fuproot*, that allows to reason about *uproot* in the context of *flatten*, see Lemma 33.

The operation *fuproot* transforms a (*set-system*)-set-system $S$ into a (*set-system*)-set-system *fuproot*($S$) = $S'$ defined as follows:

$$ \text{V}_{S'} = \{0, 1\} \times \text{V}_{S}, $$

$$ \text{V}_{iS'} = \{0\} \times \text{V}_{S} \cup \{1\} \times \text{V}_{iS}, $$

$$ \text{V}_{iS'} = \emptyset, $$

$$ S'(0, s) = \text{uproot}(S(s)) \text{ and } S'(1, s) = S(s), $$

$$ ((m, s), d, (m', s')) \text{ is a transition edge in } S' \text{ if } (s, d, s') \in \text{Edges}_S \text{ and } m' = 1, $$

$$ ((m, s), d, y) \text{ is a variable edge in } S' \text{ if } (s, d, y) \in \text{Edges}_S. $$

The operation *fuproot* is justified by the following lemma.

**Lemma 33.** For all (*set-system*)-set-system $S$, there exist a locally surjective morphism from $\text{flatten}(\text{fuproot}(S))$ to $\text{uproot}(\text{flatten}(S))$.

## 2.7 Unfold-equivalence is a congruence

The two following lemmas show that *flatten* behaves well with respect to *unfold-equivalence*.

**Lemma 34.** Let $T, T'$ be unfold-equivalent $(\Sigma$-system)-systems, then $\text{flatten}(T)$ and $\text{flatten}(T')$ are unfold-equivalent.

**Proof.** By definition of *unfold-equivalence*, this means that $T$ and $T'$ both *unfold* to some $T''$. By using twice Lemma 30, we get that both $\text{flatten}(T)$ and $\text{flatten}(T')$ *unfold* to $\text{flatten}(T'')$. Hence $\text{flatten}(T)$ and $\text{flatten}(T')$ are *unfold-equivalent*.

**Lemma 35 (unfold-equivalence is a congruence).** Let $T, T'$ be $(\Sigma$-system)-systems of same shape such that $T(t)$ is *unfold-equivalent* to $T'(t)$ for all vertices $t$, then $\text{flatten}(T)$ and $\text{flatten}(T')$ are *unfold-equivalent*.
**Proof.** Let us construct a third (Σ-system)-system $P$ that has the shape of $T$ and $T'$ and such that $P(t)$ is an unfolding of both $T(t)$ and $T'(t)$ for all vertices $t$ (it exists since $T(t)$ and $T'(t)$ are unfold-equivalent). By using twice Lemma 29, we get that flatten($P$) is an unfolding of both flatten($T$) and flatten($T'$). Hence, flatten($T$) and flatten($T'$) are unfold-equivalent. ◀

► Remark 36. The two above lemmas show that flatten can be used as an operation from regular-trees of regular-trees to regular-trees, and that this equips the functor of regular-trees of a monad structure, that we call the *monad of regular-trees*.

## 2.8 Set-contexts, contexts, and their decomposition

A special form of composition, which is derived from flatten is the notion of set-context, which are set-systems with a hole that can be filled. We also explain in this section how set-contexts can be decomposed into pieces which can be recomposed into a yield-equivalent set-context (see Lemma 38).

A Σ-set-context with a k-hole is a (Σ ⊎ {□_k})-set-system, in which □_k is a new symbol of rank k, called the hole symbol, and which labels exactly one vertex, called the hole vertex. This is illustrated in Figure 3. Set-contexts are denoted C[□_k], D[□_k], ... A set-context is closed if it is of rank 0.

Given a Σ-set-context $C[\square_k]$ and a Σ-set-system $S$ of rank $k$, $C[S]$ denotes the Σ-set-system obtained by substituting $S$ for the hole. As shown in this picture: Formally, this

<figure><img src="image_10.png" /><figcaption>Figure 3 Plugging $S$ in the 2-context $C[\square_2]$</figcaption></figure>

amounts to construct the (set-system)-set-system $S'$ of same shape $C$ such that $S'(h) = S$ for $h$ the hole vertex of $C$, and $S'(s) = \text{unit}(C(s))$ for all other vertices $s \in V_C$. We then define $C[S]$ to be $\text{flatten}(S')$.

Note in particular, that this substitution follows the “rules of flattening”, which means that (1) if the hole vertex is initial in $S$, then all initial vertices of $S$ remain initial in $C[S]$, (2) all the root vertices of $S$ remain root vertices in $C[S]$, and (3) if the hole vertex is root in $S$, then all initial vertices of $S$ get to be promoted into root vertices in $C[S]$.

Depending on the situations, we shall use flatten or [set-]contexts. The following technical lemma gives a recipe for transferring properties from one presentation to another.

► Lemma 37. For all reflexive relations $R$ between set-systems of same rank, and all reflexive and transitive relations $R'$ between set-systems of same rank, the following assertions are equivalent:

- For all set-contexts $C[\square_m]$, and all $S \in \mathcal{S}'$ set-systems of rank $m$, $C[S] \cup \mathcal{S}'$.

- For all (set-system)-set-systems $S, S'$ of same shape such that $S(s) \in \mathcal{R}'$ and $S'(s)$ for all vertices $s \in V_S$, flatten($S$) flatten($S'$).

The same holds for contexts and systems instead of set-contexts and set-systems.

**Proof.** The upward direction is straightforward, simply using the definition of $C[S]$ as a flattening.
XX:16 Tree algebras and bisimulation-invariant MSO on finite graphs

For the downward direction. Let us first introduce a notation. Let $S$ be some (set-system)-set-system and $s \in V_S$. Define $S/s[\square_{rk}(S(s))]$ to be the set-context flatten($S[s \leftarrow unit(\square_{rk}(S(s)))]$). In other words, this is flatten($S$) in which the whole part that should have arisen from $S(s)$ is a hole of suitable rank. With this definition, we naturally have that flatten($S$) and $S/s[S(s)]$ are isomorphic.

Let us now assume that the first item holds, and that $S$ and $S'$ are of same shape and such that $S(s) R S'(s)$ for all $s \in V_S$. Let us fix an enumeration $s_1, \dots, s_n$ of $V_S$. Define $S_i$ for all $i \in \{0, \dots, n\}$ as a set-system that has the shape of $S$, and such that $S_i(s_k) = S'(s_k)$ if $k \le i$, and $S_i(s_k) = S(s_k)$ otherwise. Clearly, we have $S_0 = S$, and $S_n = S'$.

Now, for all $1 < i \le n$, we have that $S_{i-1}/s_i = S_i/s_i$. Hence

$$ \text{flatten}(S_{i-1}) = S_{i-1}[S_{i-1}(s_i)] R' S_{i-1}[S_i(s_i)] = S_i/s_i[S_i(s_i)] = \text{flatten}(S_i), $$

which by induction yields $\text{flatten}(S) R' \text{flatten}(S')$.

Given $n+1$ Σ-set-systems $S_0, S_1, \dots, S_n$ of rank 1, define the Context($S_0, S_1, \dots, S_n$) to be the following closed Σ-set-context:

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

Formally, it is the disjoint union $C$ of all the $S_0, S_1, \dots, S_n$'s, together with the following modifications: (1) there is a new vertex $h$ which is labelled $C(h) = \square_n$, (2) the transition edges of $C$ are the transition edges of $S_0, S_1, \dots$, and $S_n$ augmented with new transition edges $(v, d, h)$ for all variable edges $(v, d, x_1)$ in some $S_0, \dots, S_n$, and new transition edges of the form $(h, d, s)$ for all initial vertices $s$ of $S_d$.

Given a closed set-context $C[\square_n]$ of hole vertex $h$, define its pieces $P_0, P_1, \dots, P_n$ as follows:

- $P_0$ is a set-system of rank 1 defined to be identical to $C$ but for (1) the vertex $h$ is removed as well as all the edges starting from $h$, and (2) all the transition edges of the form $(v, d, h) \in \text{Edges}_C$ are turned into variable edges $(v, d, x_1)$ of $P_0$.

- $P_i$, for $i \in [n]$, is a set-system of rank 1 defined to be identical to $C$ but for (1) the hole vertex $h$ is removed as well as all the edges from $h$, (2) the initial vertices $v$ of $P_i$ are the ones such that $(h, i, v)$ is a transition edge in $C$, and (3) all the transition edges of the form $(v, d, h) \in \text{Edges}_C$ are turned into variable edges $(v, d, x_1)$ of $P_i$.

**Lemma 38 (decomposition and recomposition of set-contexts).** Let $(P_0, P_1, \dots, P_n)$ be the pieces of a closed set-context $C[\square_n]$, then $C$ and Context$(P_0, P_1, \dots, P_n)$ are yield-equivalent.

**Proof.** There is an obvious morphism from Context$(P_0, P_1, \dots, P_n)$ to $C$ which consists in sending the hole vertex to the hole vertex, and each vertex that belongs to some piece of $C$ to its originating vertex in $C$. It happens to be locally surjective. This means by Lemma 25 that $C$ and Context$(P, P_1, \dots, P_n)$ are yield-equivalent.

Let us conclude with a simple result that allows to change the ranks when using a normalised context.

**Lemma 39.** Let $P_0, P_1, \dots, P_n$ be set-systems, and $\sigma: [m] \to [n]$, then
$$ \text{Context}(P, P_{\sigma(1)}, \dots, P_{\sigma(m)}) \quad \text{and} \quad \text{Context}(P, P_1, \dots, P_n)[\hat{\sigma}(\square_m)] $$
are yield-equivalent.
## 2.9 Resolutions and flatten-resolutions

The goal of this section is to introduce suitable notions for understanding what are the yields of the flattening of a (set-system)-set-system, namely the notions of resolutions and flatten-resolutions, and provide the key lemmas for working with them, Lemmas 45 and 46. One application of these tools will be Corollary 47 which states that yield-equivalence is a congruence with respect to flattening, but they will also play an important role in the proofs of Section 4, and more particularly Lemma 70.

At rather high level, we would like to “understand” the direct resolutions of a flattening of a (set-system)-set-system as the flattening of a system-system that would have a “similar structure”. In other words, we would like to see the direct resolutions of a combination of set-systems as combinations of direct resolutions of the components. The difficulty is that it simply does not work with direct resolutions, as is illustrated in the following example.

**► Example 40 (direct resolutions are not compositional).** We are using set-contexts rather than flattenings for the sake of description. Let us work with a ranked alphabet that has symbols $b$ and $c$ of rank 0, and $a_2$ of rank 2. Consider the set-context $C[\square_1] = \square_1(b+c)$ and the system $S = a_2(x_1, x_1)$.

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

Then:

- The system $S$ has one direct resolution: $S$ itself.

- The set-context $C[\square_1]$ has two direct resolutions: $C_1[\square_1] = \square_1(b)$ and $C_2[\square_1] = \square_1(c)$.

- The set-system $C[S]$ has four direct resolutions up to unfold-equivalence: $a_2(b, b)$, $a_2(b, c)$, $a_2(c, b)$, and $a_2(c, c)$.

If we combine the direct resolutions of $C[\square_1]$ and $S$ in all possible ways, we only obtain $C_1[S] = a_2(b, b)$ and $C_2[S] = a_2(c, c)$. These are indeed direct resolutions of $C[S]$, but we still miss two of them, namely $a_2(b, c)$ and $a_2(c, b)$. The issue is that the double occurrence of $x_1$ in $a_2(x_1, x_1)$ forbids to use it in a combination of systems for producing, eg, $a_2(x_1, x_2)$.

To overcome the difficulty illustrated in the above example, one should also consider that a “possible outcome” of $S$ could be $a_2(x_1, x_2)$, at the condition that we also keep track that the variables $x_1$ and $x_2$ correspond in fact both to the same variable $x_1$ in $S$. This justifies the following definition of resolutions that combine direct resolutions with renaming of variables for tracking their origin.

► **Definition 41.** Given a $\Sigma$-set-system $S$ of rank $n$, a resolution of $S$ is an ordered pair $(T, \sigma)$ in which:

- $\sigma$ is a map from $[m]$ to $[n]$, and

- $T$ is a $\Sigma$-set-system of rank $m$, such that

- $\hat{\sigma}(T)$ is a direct resolution of $S$.

Two resolutions $(T, \sigma)$ and $(T', \sigma')$ are unfold-equivalent if $\sigma = \sigma'$, and $T$ is unfold-equivalent to $T'$.

In Example 40, we see that $(a_2(x_1, x_2), \sigma)$ with the constant map $\sigma: [2] \to [1]$ is a resolution of $S$, and that it conveys in some form the information that could not be caught by direct resolutions. Hence, it makes sense to understand a direct resolution of $C[S]$ as a combination of resolutions of $C$ and $S$.
XX:18 Tree algebras and bisimulation-invariant MSO on finite graphs

The first important thing to note is that *yield-equivalence* is sufficient for working with *resolutions*: the next lemma shows in particular that two *yield-equivalent set-systems* are also automatically “resolution-equivalent”.

**Lemma 42.** If $S \subseteq^{\text{yields}} S'$, then for all resolutions $(T, \sigma)$ of $S$, there is a resolution $(T', \sigma)$ of $S'$ such that $T$ unfolds to $T'$. Hence all the resolutions of $S$ are resolutions of $S'$ modulo unfold-equivalence.

**Proof.** Let $(T, \sigma)$ be a resolution of $S$. It means that $\hat{\sigma}(T)$ is a direct resolution of $S$. Since $S \subseteq^{\text{yields}} S'$, $\hat{\sigma}(T)$ unfolds to some direct resolution $T'$ of $S'$. By Lemma 19, there exists $T''$ such that $T$ unfolds to $T''$ and $\hat{\sigma}(T'') = T'$. Hence $(T'', \sigma)$ is a resolution of $S'$ such that $T$ unfolds to $T''$. ◀

We shall now define the notion of flatten-resolution which describes how resolutions can be combined together in a coherent way.

Definition 43. Consider $(\Sigma$-set-system)-set-system $S$ and a $(\Sigma$-system)-system $T$, then $T$ is a flatten-resolution of $S$ witnessed by $(\delta, \sigma)$ if:

■ $\delta: V_T \to V_S$ is such that $\delta(V_i_T) \subseteq V_i_S$.

■ For all vertices $t$ of $T$, $(T(t), \sigma_t)$ is a resolution of $S(\delta(t))$.

■ For all transition edges $(t, i, t')$ of $T$, then $(\delta(t), \sigma_t(i), \delta(t'))$ is a transition edge of $S$.

■ For all variable edges $(t, i, y)$ of $T$, then $(\delta(t), \sigma_t(i), y)$ is a variable edge of $S$.

**Example 44.** Let us see how this plays out in the context of Example 40. Let $T$ be the system-system $A_2(b, c)$, with $A_2 = \text{unit}(a_2)$, located at vertex $t$ of the outer system. Then $T$ is a flatten-resolution of $C[S]$ witnessed by $(\delta, \sigma)$, where $\delta(t) = \square_1$ (the unique hole vertex in $C[\square_1]$), and $\sigma_t$ is the constant map $\sigma_t: [2] \to [1]$. The values of $\delta$ on vertices $t_b, t_c$ labelling $b$ and $c$ respectively in $T$ are as expected: $\delta(t_b)$ is the vertex labelled $b$ in $C[S]$, and similarly for $c$. We have that $(T(t), \sigma_t) = a_2(x, y)$ is a resolution of $C[S](\delta(t)) = S$, and the other conditions are satisfied.

Our first lemma shows why it is meaningful to call this object a *flatten-resolution*: each *flatten-resolution* $T$ of a (set-system)-set-system $S$ does flatten into a direct resolution of *flatten*($S$).

**Lemma 45.** It $T$ is a flatten-resolution of $S$ witnessed by $(\delta, \sigma)$, and $\gamma_t$ is the morphism showing that $(T(t), \sigma(t))$ is a resolution of $S(\delta(t))$, then the map

$$ \rho(t, v): V_{\text{flatten}(T)} \to V_{\text{flatten}(S)} \\ (t, v) \mapsto (\delta(t), \gamma_t(v)) $$

is a morphism from *flatten*($T$) to *flatten*($S$), and hence *flatten*($T$) is a direct resolution of *flatten*($S$).

Proof. The only interesting case is when an edge $((t, s), k, (t', s'))$ of *flatten*($T$) is an inter-subsystem transition edge, ie there exists a variable edge $(s, k, x_i)$ in $T(t)$ and a transition edge $(t, i, t')$ in $T$, and $s'$ is initial in $T(t')$. In this case, by definition of a *flatten-resolution*, since $\gamma_t$ is a morphism from $\hat{\sigma}_t(T(t))$ to $S(\delta(t))$, there is a variable edge $(\gamma_t(s), k, x_{\sigma_t(i)})$ in $S(\delta(t))$. From the definition of *flatten-resolution*, $(\delta(t), \sigma_t(i), \delta(t'))$ is a transition edge of $S$. Since $s'$ is initial, we get that $\gamma_{t'}(s')$ is an initial vertex of $S(\delta(t'))$. Overall, this fulfills the assumptions of the intra-subsystem case in the definition of the flattening, and we deduce that $((\delta(t), \gamma_t(s)), k, (\delta(t'), \gamma_{t'}(s')))$ is a transition edge of *flatten*($S$). ◀
Our second lemma is natural yet a bit technical to establish. It can be understood as a form of converse of Lemma 45: all direct resolutions of a flattening can be considered to be flatten-resolutions, up to unfolding.

**▶ Lemma 46.** For all $(\Sigma$-set-system)-set-systems $S$, and all direct resolutions $R$ of flatten($S$), there exists a flatten-resolution $T$ of $S$ such that flatten($T$) is an unfolding of $R$.

**Proof.** Let us fix ourselves $S$ and $R$ as in the statement of the lemma. Let $\delta, \gamma$ be such that $\eta: r \mapsto (\delta(r), \gamma(r))$ is the morphism from $R$ to flatten($S$), ie $\delta$ maps vertices of $R$ to vertices of $S$, and $\gamma$ maps each vertex $r$ of $R$ to a vertex $\gamma(r)$ in $S(\delta(r))$.

We shall now construct the system-system $T$ of the statement. The intuition is that each subsystem $T(t)$ should correspond to a resolution of $S(\delta(t))$ that captures a part of $T$ that has “entered” the subsystem $S(\delta(t))$ “at $t$”. Note that “entering the subsystem $S(\delta(t))$ at $t$” occurs either at an initial vertex of flatten($S$), or through an inter-subsystem transition edge of flatten($S$).

One technical detail of the construction is that a given transition edge $(s, i, s') \in Edges_S$ can be used in several inter-subsystem $((s, t), j, (s', t'))$ of flatten($S$), and each of them can be the image by morphism of several transition edges of $R$. We need to disambiguate them in the construction by giving different directions to them in $T$. This is the subject of the following definition of Dirs that we give now.

For all vertices $s$ of $S$ define:

$$ 
\begin{aligned}
\text{ça}(s) &:= \{(i, r') \mid (r, i, r') \in \text{Edges}_R, \delta(r) = s, (s, j, \delta(r')) \in \text{Edges}_S, \\
& \phantom{:=} (\gamma(r), i, x_j) \in \text{Edges}_{S(s)}, \gamma(r') \in \text{Vi}_{S(\delta(r'))} \} \\
& \cup \{(i, y) \mid (r, i, y) \in \text{Edges}_R, \delta(r) = s\},
\end{aligned}
$$

and for each $s \in V_S$, we define $\text{dir}_s$ to be a bijection from $\text{ça}(s)$ onto $[|\text{ça}(s)|]$.

We now define the expected $(\Sigma$-system)-system $T = (V_T, \text{Vi}_T, \emptyset, \text{label}_T, \text{Edges}_T)$ as follows.

$V_T := \{t \in V_R \mid \gamma(t) \in \text{Vi}_{S(\delta(t))}\}$, ie the vertices of $T$ are the vertices $t$ of $R$ sent by $\gamma$ to an initial vertex of $S(\delta(t))$.

The initial vertex is the initial vertex of $R$, ie $\text{Vi}_T = \text{Vi}_R^7$

For all $t \in V_T$, $T(t)$ is an $\Sigma$-system of rank $|\text{ça}(t)|$ to be defined below.

For all vertices $t$ and all $(j, t') \in \text{ça}(t)$, there is a transition edge $(t, \text{dir}_{\delta(t)}(j, t'), t')$.

For all vertices $t$ and all $(j, x) \in \text{ça}(t)$, there is a variable edge $(t, \text{dir}_{\delta(t)}(j, x), x)$.

We now define, for all $t \in V_T$, the $\Sigma$-system $T(t) = \text{label}_T(t) = (V_t, \text{Vi}_t, \emptyset, \text{label}_t, \text{Edges}_t)$ as follows:

The set of vertices is $V_t := \{r \in V_R \mid \delta(r) = \delta(t)\}$.

The initial vertex of $T(t)$ is $t$ itself.

The labelling of $r \in V_t$ is the labelling of $r$ in $R$, ie $T_t(r) = R(r)$.

There is a transition edge $(r, d, r') \in Edges_t$ if

- $(r, d, r') \in Edges_R$ and $(\gamma(r), d, \gamma(r')) \in Edges_{S(\delta(t))}$, (nota: this corresponds to $\tilde{\eta}(r, d, r')$ being an intra-subsystem case of flatten($S$))

There is a variable edge $(r, d, y) \in Edges_t$ if

<footnote n="7">⁷ Note that if $t$ is initial in $R$, then (by morphism), $(\delta(t), \gamma(t))$ is initial in flatten($S$), hence (by definition of flatten) $\delta(t)$ is initial in $S$. Thus we indeed have $\text{Vi}_T \subseteq V_T$).</footnote>
XX:20 Tree algebras and bisimulation-invariant MSO on finite graphs

- $y = x_{\text{dir}_{\delta(r)}(i,r')}$ with $(r, d, r') \in \text{Edges}_R$, $(\delta(r), i, \delta(r')) \in \text{Edges}_S$, $(\gamma(r), d, x_i) \in S(\delta(t)) \in S(\delta(r))$ and $\gamma(r') \in \text{Vi}_{S(\delta(t))}$ and $(\gamma(r), d, \gamma(r')) \notin \text{Edges}_{S(\delta(t))}$, (nota; this corresponds to $\tilde{\eta}(r, d, r')$ being an inter-subsystem case of flatten($S$)), or

- $y = x_{\text{dir}_{\delta(r)}(i,z)}$ with $(r, d, z) \in \text{Edges}_R$, $(\delta(r), i, z) \in \text{Edges}_S$ and $(\gamma(r), d, x_i) \in S(\delta(t)) \in S(\delta(r))$ (nota; this corresponds to $\tilde{\eta}(r, d, z)$ being a variable case of flatten($S$)).

T is a well-defined (Σ-system)-system. By case analysis. The interesting case is for the edges of $T(t)$. Let $r \in V_T$ and $d \in [\text{rk}(T(r))]$, we have to show that $\text{Edges}_t(r, d)$ is a singleton. First of all, we know that there is exactly one transition $(r, d, f) \in \text{Edges}_R(r, d)$ since $R$ is a system. We distinguish three cases:

- If $\tilde{\eta}(r, d, f)$ is an intra-subsystem case of flatten($S$), this means that $f = r' \in V_R$ and $((\gamma(r), d, \gamma(r')) \in \text{Edges}_{S(\delta(t))})$. Thus $(r, d, r') \in \text{Edges}_t$ by definition of transition edges. However, there cannot be other edges since $(\gamma(r), d, \gamma(r')) \notin \text{Edges}_{S(\delta(t))}$ is explicitly required for the first item of variable edges. Hence $\text{Edges}_t(r, d)$ is a singleton.

- If $\tilde{\eta}(r, d, f)$ is an inter-subsystem case, and this instantiate all the parameters of the first case of variable edges in the definition of $\text{Edges}_t$.

- If $\tilde{\eta}(r, d, f)$ is a variable case, this instantiates all the parameters of the second case of variable edges in the definition of $\text{Edges}_t$.

The direct resolution $R$ unfolds to flatten($T$). For this, we define the map $\varphi$ from vertices of flatten($T$) to $R$ by $\varphi(t, r) := r$ for all $t \in V_T$ and $r \in V_T$. We have to prove that $\varphi$ is a morphism. Again, the verification is of tedious mechanical nature.

Let us treat the most interesting case, which is when $((t, r), i, (t', r'))$ is an inter-subsystem transition edge of flatten($t$). We have to prove that $(r, i, r')$ is a transition edge of $R$. Being an inter-subsystem transition edge means that there exist a variable edge $(r, i, x_k) \in \text{Edges}_t$, a transition edge $(t, k, t') \in \text{Edges}_T$, and that $r' \in \text{Vi}_{t'}$. Since $(r, i, x_k) \in \text{Edges}_t$, by definition of $\text{Edges}_t$, we know that there exists a transition edge $(r, i, r'') \in \text{Edges}_R$ with $k = \text{dir}_{\delta(t)}(j, r'')$ for some $j$. Since $(t, k, t') \in \text{Edges}_T$ and $k = \text{dir}_{\delta(t)}(j, r'')$, by definition of $\text{Edges}_T$, we get $t' = r'$. Since $r' \in \text{Vi}_t$, by definition of $\text{Vi}_{t'}$, we obtain $t' = r'$. To conclude, we have $(r, i, r'') \in \text{Edges}_R$ and $r'' = t' = r'$, and thus $(r, i, r') \in \text{Edges}_R$ as expected.

T is a flatten-resolution of T. For all $t \in V_T$, and all $(j, r) \in \text{ça}(\delta(t))$, let

$$ \sigma_t : [\text{rk}(T(t))] = [[\text{ça}(\delta(t))]] \rightarrow [\text{rk}(S(\delta(t)))] \\ \text{dir}_{\delta(t)}(j, r) \quad \mapsto j. $$

Let also $\gamma_t = \gamma$ for all $t \in V_T$. We have to show that $(\delta, \sigma, \gamma)$ witness that $T$ is a flatten-resolution of $S$.

- As required, $\delta$ sends the root vertex $r$ of $T$ to $\delta(r)$, which is a root vertex of $S$. There are no initial vertices.

- Let $t \in V_T$, We have to show that $(T(t), \sigma_t)$ is a resolution of $S(\delta(t))$, ie that $\gamma_t$ is a morphism from $\hat{\sigma}_t(T(t))$ to $S(\delta(t))$.

To begin with, the initial vertex of $T(t)$ is $t$ itself, and by definition of $V_T$, it is an initial vertex of $S(\delta(t))$.

Consider now some transition edge $(r, i, r') \in \text{Edges}_t$. By definition of $\text{Edges}_t$, this implies that $(r, i, r') \in \text{Edges}_R$ and $(\gamma(t), i, \gamma(r'))$ is a transition edge of $S(\delta(t))$. Hence $(\gamma_t(t), i, \gamma_t(r'))$ is a transition edge of $S(\delta(t))$.

Consider finally some variable edge $(r, i, x_k) \in \text{Edges}_t$. By definition of $\text{Edges}_t$, this implies that there is a variable edge $(\gamma(r), i, x_j) \in \text{Edges}_{S(\delta(t))}$ and that $k = \text{dir}_{\delta(t)}(j, r')$ for some $r'$. Thus $\sigma_t(k) = j$ by definition of $\sigma_t$, and we obtain $(\gamma_t(r), i, x_{\sigma_t(k)}) \in \text{Edges}_{S(\delta(t))}$. Overall, $\gamma_t$ is a morphism from $\hat{\sigma}_t(T(t))$ to $S(\delta(t))$ as aimed for.
For the last point, given a transition edge $(t, k, t') \in Edges_T$, we have to prove that $(\delta(t), \sigma_t(k), \delta(t'))$ is a transition edge of $S$. By definition of $Edges_T$, we know that $k \in [[\text{ Kings}(\delta(t))]]$ and that $k = \text{dir}_{\delta(t)}(j, t')$ for some $j$. By definition of $\sigma_t$, $\sigma_t(k) = j$. Furthermore, by definition of $\text{ Kings}(\delta(t))$, there exists $(r, j, t') \in Edges_R$ with $\delta(r) = \delta(t)$ and $(\delta(r), j, \delta(t')) \in Edges_S$. Thus $(\delta(t), \sigma_t(k), \delta(t')) \in Edges_S$ as expected.

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

From this technical lemma, we can already derive an important consequence.

**Corollary 47 (yield-equivalence is a congruence for the flattening).** Let $S, S'$ be $(\Sigma$-set-system)-set-systems of same shape such that $S(s) \subseteq^\text{yields} S'(s)$ (resp. $S(s) =^\text{yields} S'(S)$) for all vertices $s \in V_S$, then $\text{ flatten}(S) \subseteq^\text{yields} \text{ flatten}(S')$ (resp. $\text{ flatten}(S) =^\text{yields} \text{ flatten}(S')$).

**Proof.** Assume $S(s) \subseteq^\text{yields} S'(s)$ for all $s \in V_S$.

We first claim that for all direct resolutions $R$ of $\text{ flatten}(S)$, there exists an unfold-equivalent direct resolution of $\text{ flatten}(S')$.

Indeed, by Lemma 46, there exists a flatten-resolution $T$ of $S$ witnessed by $(\delta, \sigma)$ such that $\text{ flatten}(T)$ is an unfolding of $R$. For all $t \in V_T$, we know that $(T(t), \sigma_t)$ is a resolution of $S(\delta(t))$. Since $S(\delta(t)) \subseteq^\text{yields} S'(\delta(t))$, we define $T'(t)$ to be some $\Sigma$-system unfold-equivalent to $T(t)$ and such that $(T'(t), \sigma_t)$ is a resolution of $S'(\delta(t))$ (it exists by Lemma 42). Let us define the $(\Sigma$-system)-system $T'$ that has the shape of $T$, and labelling $T'(t)$ as defined above for all $t \in V_T$. It is clear that $T'$ is a flatten-resolution of $S'$. We also get by Lemma 35 that $\text{ flatten}(T)$ and $\text{ flatten}(T')$ are unfold-equivalent, and as a consequence, $\text{ flatten}(T')$ is a direct resolution of $S'$ which is unfold-equivalent to $R$. The claim is proved.

Since this holds for all direct resolutions, we have $\text{ InitYields}(\text{ flatten}(S)) \subseteq \text{ InitYields}(\text{ flatten}(S'))$.

Let us now apply this first inclusion to $\text{fuproot}(S)$ and $\text{fuproot}(S')$ (which also happen to satisfy $\text{fuproot}(S)(s) \subseteq^\text{yields} \text{fuproot}(S')(s)$ for all vertices $s$). We obtain:

$$ \begin{aligned} \text{RootYields}(\text{flatten}(S)) &= \text{InitYields}(\text{uproot}(\text{flatten}(S))) = \text{InitYields}(\text{flatten}(\text{fuproot}(S))) \\ &\subseteq \text{InitYields}(\text{flatten}(\text{fuproot}(S')))) = \text{InitYields}(\text{uproot}(\text{flatten}(S')) = \text{RootYields}(S'). \end{aligned} $$

Hence $\text{flatten}(S) \subseteq^\text{yields} \text{flatten}(S')$.

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

**Remark 48.** A consequence is that the endofunctor of ranked sets that builds yield-equivalence classes of set-systems, equipped with the flatten and unit natural transformations, is a monad.

Of course, since unfold-equivalence and yield-equivalence agree on systems, the monad of regular-trees is a submonad of this monad. However, it is not the case that it cannot be described using a distributive law with the powerset monad as shown in [4].

We conclude this section with a proof of a form of continuity result (the important version is Corollary 50).

**Lemma 49.** Let $R$ be a direct resolution of $C[S]$ for $C[\square_n]$ a set-context, and $S$ a set-system of rank $n$, then there exists a finite set $F$ of direct resolutions of $S$ such that $R$ unfolds to a direct resolution of $C[\sum_{R' \in F} R']$.

**Proof.** Let us show the more general version of the statement: let $S$ be a (set-system)-set-system, and $R$ be a direct resolution of $\text{flatten}(S)$, then there exists for all vertices $v$ of $S$ a finite set $F(v)$ of direct resolutions of $S(v)$, such that $R$ is a direct resolution of $\text{flatten}(S')$ defined to have the same shape as $S$, with $S'(v) = \sum_{R' \in F(v)} R'$.
XX:22 Tree algebras and bisimulation-invariant MSO on finite graphs

For this, let $T$ be the flatten-resolution of $S$ obtained by Lemma 46, witnessed by $(\delta, \sigma)$,
and such that flatten$(T)$ is an unfolding of $R$. For all vertices $v$ of $S$, let $F(v)$ be the set
of systems $\hat{\sigma}_t(T(t))$ for $t \in \delta^{-1}(v)$. Clearly, $F(v)$ is finite. Furthermore, for all $R' \in F(v)$,
$R' = \hat{\sigma}_t(T(t))$ for some $t \in \delta^{-1}(v)$ such that $(T(t), \sigma_t)$ is a resolution of $S(\delta(t))$. Hence $R'$ is a
direct resolution of $S(v)$. We also obviously have that $(T(t), \sigma_t)$ is a resolution of $\sum_{R' \in F(v)} R'$.
As a consequence, $T$ is a flatten-resolution of $S'$ as defined above (also witnessed by $(\delta, \sigma)$).
Now, using Lemma 45, we obtain that $R$ unfolds to flatten$(T)$ which is a direct resolution
of flatten$(S')$.

► **Corollary 50.** For all set-contexts $C[\square_n]$ and all set-systems $S$ of rank $n$,

$$
\text{Yields}(C[S]) = \bigcup_{\substack{F \subseteq \text{Yields}(S) \\ F \text{ finite}}} \text{Yields}\left(C\left[\sum_{R \in F} R\right]\right).
$$

3 Algebras

In this section, we introduce notions of algebras in Section 3.1, and how they can be used to
recognise languages of systems in Section 3.2. We then explain why MSO-definable languages
of systems are recognised by rankwise finite algebras in Section 3.3.

**3.1 Algebras**

The following definitions follow the standard approach via monads.

► **Definition 51 (algebras).** An algebra $\mathcal{A}$ is a ranked set $A$ together with a map of ranked sets eval (called the evaluation) from $\mathcal{A}$-systems to $A$, such that

■ eval(unit(a)) = a, for all a ∈ A,

■ eval(eval(S)) = eval(flatten(S)) for all (A-system)-systems S.

A morphism from the algebra $\mathcal{A} = (A, \text{eval})$ to the algebra $\mathcal{A}' = (A', \text{eval}')$ is a map $\rho$ from $A$
to $A'$ such that $\text{eval}'(\bar{\rho}(S)) = \rho(\text{eval}(S))$ for all $\mathcal{A}$-systems $S$.

An algebra is unfold-invariant if eval(S) = eval(S') for all unfold-equivalent A-systems S, S'.

Unfold-invariant algebras are called regular-tree algebras.

The ranked set of Σ-systems equipped with flatten as evaluation is an algebra called the free-algebra generated by Σ, or the Σ-free-algebra.

► **Example 52 (non-unfold-invariant algebra).** Consider $\mathcal{A} := (A, \text{eval})$ defined by $A_n = \{\top, \bot\}$ for all $n \in \mathbb{N}$, and for all $\mathcal{A}$-systems $S$, let $\text{eval}(S)$ be $\top$ if $S(s) = \top$ for some vertex $s \in V_S$, and $\bot$ otherwise. It is easy to show that $\mathcal{A}$ is an algebra. However, it is not a regular-tree algebra since it is not unfold-invariant, as shown now. Let $S_1$ be the closed $\mathcal{A}$-system with one vertex, which is initial and labelled $\bot \in A_0$; and let $S_2$ be $S_1$ augmented with a new vertex (not initial), labelled $\top \in A_0$. Since the new vertex is unreachable, $S_1$ and $S_2$ are unfold-equivalent (see Remark 18). We have $\text{eval}(S_1) = \bot \neq \top = \text{eval}(S_2)$, and hence $\mathcal{A}$ is not unfold-invariant.

► **Example 53 (unfold-invariant algebra).** Consider $\mathcal{A} = (A, \text{eval})$ defined by $A_n = \mathcal{P}([n]) \uplus \{\bot\}$, and eval to be mapping an $\mathcal{A}$-system $T$ of rank $n$ to eval($T$) = $\bot$ if there is a ‘$\bot$’ element reachable from the initial vertex. Otherwise eval($T$) is the set of $i \in [n]$ such that the variable $x_i$ is reachable in $T$ from the initial vertex. We leave to the reader to check that it satisfies the identities of algebras. This algebra is unfold-invariant, since a symbol $\bot$ (resp. a
variable $x_i$) is reachable in $T$ from the initial vertex or root vertex if and only if this is also the case in any unfolding of $T$.

► **Remark 54.** A consequence of Lemma 37 is that, in the definition of algebras, one could safely exchange the second identity for

eval($C[S]$) = eval eval($S$)) for all A-contexts $C[\square_m]$ and all A-systems $S$ of rank $m$.

## 3.2 Languages and their recognition by algebras

Call a language of systems (or simply a language) over an alphabet $\Sigma$ a set of closed $\Sigma$-systems. A language of $\Sigma$-regular-trees is a language of $\Sigma$-systems $L$ which is invariant under unfold-equivalence (ie such that if $T, T'$ are unfold-equivalent and $T \in L$, then $T' \in L$).

Let $\rho$ be a morphism (called the recognising morphism) from the $\Sigma$-free algebra to an algebra $\mathcal{A}$, and $P \subseteq A_0$ (called the accepting set), the language recognised by $(\mathcal{A}, \rho, P)$ is the set of closed $\Sigma$-systems defined as

$$ \mathrm{Rec}(\mathcal{A}, \rho, P) := \{T \mid T \text{ closed } \Sigma\text{-system such that } \rho(T) \in P\}. $$

We say that $L$ is recognised by $\mathcal{A}$ if it is recognised by $(\mathcal{A}, \rho, P)$ for some $\rho$ and $P$.

This is the standard definition of recognition, as for word languages. The only subtlety is that we focus on closed systems, which is reflected in the fact that $P \subseteq A_0$. Quite naturally, we shall be interested in languages that are recognisable by rankwise finite algebras, ie algebras $\mathcal{A} = (\mathcal{A}, \mathrm{eval})$ such that $A_n$ is finite for all $n \in \mathbb{N}$.

► **Example 55 (reachable symbol).** Consider some ranked alphabet $\Sigma$, and a set of letters $R \subseteq \Sigma$. Let also $\mathcal{A}$ be the algebra from Example 53, and define $\rho$ as the unique algebra morphism from the $\Sigma$-free algebra to $\mathcal{A}$ such that

$$ \rho(a(x_1, \dots, x_k)) = \begin{cases} \perp & \text{if } a \in R \\ \{1, \dots, k\} & \text{otherwise.} \end{cases} $$

Notice that thanks to Remark 54, this is enough to compute the value of e.g. $\rho(a(x_3, x_1, x_1))$, which is $\{1, 3\}$ if $a \notin R$. Then, the language recognised by $(\mathcal{A}, \rho, \{\perp\})$ is the set of closed $\Sigma$-systems that contain a symbol of $R$ reachable from the initial vertex. Since this language is preserved under unfold-equivalence, it is a language of regular-trees. Similarly, the language recognised by $(\mathcal{A}, \rho, \{\emptyset\})$ is the set of closed $\Sigma$-systems that contain no symbol of $R$ reachable from the initial vertex.

► **Lemma 56.** The language of systems recognised by unfold-invariant algebras are languages of regular-trees.

**Proof.** Let $T$ and $T'$ be unfold-equivalent $\Sigma$-systems. Then $\bar{\rho}(T)$ and $\bar{\rho}(T')$ are unfold-equivalent, and hence $\rho(T) = \mathrm{eval}(\bar{\rho}(T)) = \mathrm{eval}(\bar{\rho}(T')) = \rho(T')$. Thus $T \in L$ if and only if $T' \in L$, which means that $L$ is a language of regular-trees. $\blacksquare$

Let us now briefly recall the important closure operations enjoyed by the languages recognisable by rankwise finite algebras. These will be the justification of the translation from monadic second-order logic to recognisability by rankwise finite algebras (see Section 3.3).

For this, let $h$ be a map from the ranked set $\Sigma$ to the ranked set $\Gamma$. Then $\bar{h}$ is a morphism from $\Sigma$-systems to $\Gamma$-systems. We define the following operations:

For $L$ a language of $\Gamma$-systems, its cylindricification by $h$ is the language of $\Sigma$-systems $\bar{h}^{-1}(L)$.
For $L$ a language of $\Sigma$-systems, its projection by $h$ is the language of $\Gamma$-systems $\bar{h}(L)$.

► Remark 57. Note that languages of regular-trees are closed under boolean connectives and cylindrification. However, this is not the case for projection as illustrated now. Consider the ranked alphabet $\Sigma$ consisting of letters $a_2, b, c$ of respective ranks 2, 0, 0, and the language $L$ that contains, up to isomorphism, the sole $\Sigma$-system $a_2(b, c)$. It is a language of $\Sigma$-regular-trees. Consider now the map $h$ which maps $a_2$ to itself, and $b$ and $c$ to $b$. Then $a_2(b, b) \in \bar{h}(L)$. Notice now that $a_2(b, b)$ is unfold-equivalent to $S_1(b)$, in which $S_1 = \sigma_{2 \to 1}(a_2)$ where $\sigma_{2 \to 1}$ is the constant map from [2] to [1]. Informally, $S_1(b)$ is a version of $a_2(b, b)$ in which the two $b$-subtrees have been merged. Now $S_1(b)$ has only two antecedents by $\bar{h}$, namely $S_1(b)$ and $S_1(c)$, and none belongs to $L$, so $S_1(b) \notin \bar{h}(L)$. This means that $\bar{h}(L)$ is not a language of regular-trees, as it is not closed under unfold-equivalence.

In the above remark, the problem stems from the invariance under unfold-equivalence which is required for languages of regular trees. The following statement is not subject to this difficulty, since it considers languages of systems only.

**Lemma 58.** *Languages recognisable by rankwise finite algebras are closed under Boolean connectives, cylindrification, and projection.*

**Proof.** All the operations follow from generic algebraic arguments, that are independent of the specific algebraic theory, except for projection. For the projection it suffices to perform a rankwise powerset of the algebra recognising $L$. This is not problematic here since we do not consider systems modulo unfold-equivalence. However, it would not work modulo unfold-equivalence, for the reasons illustrated in the above remark. ◀

## 3.3 MSO over systems and the composition method

*Monadic second-order logic (MSO for short)* is the extension of first-order logic with *monadic second-order variables* (or simply *monadic variables*) $X, Y, \dots$, a membership relation $x \in Y$, and set quantifiers $\exists X$ and $\forall Y$. These constructions have their expected meaning.

Given a ranked set $\Sigma$, the signature $\mathit{Sig}(\Sigma)$ contains the relational symbol $R_a$ of arity $n+1$ for all $a \in \Sigma_n$, and a unary relational symbol $I$. It is natural to see a $\Sigma$-system $S$ as a relational structure $\mathit{Struct}(S)$ that has vertices of $S$ as universe, and such that

- The interpretation of $I$ is the singleton $\mathit{Vi}$.

- For all $a \in \Sigma_n$, the interpretation of $R_a$ is $\{(u, v_1, \dots, v_n) \in V^{n+1} \mid \mathit{label}(u) = a, (u, i, v_i) \in \mathit{Edges} \text{ for all } i \in [n]\}$.

Using this encoding gives a meaning to the statement $S \models \varphi$ in which $\varphi$ is an MSO-sentence over the signature $\mathit{Sig}(\Sigma)$: we simply interpret it as $\mathit{Struct}(S) \models \varphi$.

**Lemma 59.** *Given an MSO-sentence $\varphi$, the language $\{S \mid \Sigma\text{-system} \mid S \models \varphi\}$ is recognisable by a rankwise finite algebra.*

**Proof.** This follows the usual approach in which one interprets disjunctions as union, conjunction as intersection, negation as complement, adding of a free variable as cylindrification, and existential monadic quantifiers as projection. These operations indeed preserve recognisability by a rankwise finite algebra according to Lemma 58. ◀

# 4 Yield algebras

We introduce in Section 4.1 a richer notion of algebras, called *yield-algebras*. These are the algebras arising from *set-systems* considered modulo *yield-equivalence*. In particular, we
introduce the notion of syntactic yield-algebra of a language of regular-trees in Section 4.2, and
use it in Section 4.3 to establish that the syntactic yield-algebra of languages of regular-trees
recognised by rankwise finite algebra are also rankwise finite (see Lemma 70).

4.1 Yield-algebras

The definition of a yield-algebra corresponds to the notion of algebras naturally arising from set-systems, quotiented by yield-equivalence. Since set-systems are equipped with a form of non-determinism, yield-algebra are naturally endowed of an order $\sqsubseteq$ that provides an inf-semi-lattice structure (note that the non-deterministic sum will be noted $\sqcap$, ie as an infimum rather than a supremum; this is a design choice that corresponds to the fact that we see in this work this non-determinism as “demonic”, ie controlled by an opponent).

**Definition 60.** A yield-algebra $\mathcal{Y}$ is a ranked set $Y$ together with a map of ranked sets eval from $Y$-set-systems to $Y$, such that

- eval(unit($a$)) = $a$, for all $a \in Y$,

- eval($\overline{eval}(S)$) = eval(flatten($S$)) for all (Y-set-system)-set-systems $S$, and

- for all yield-equivalent $Y$-set-systems $S$, $S'$ of same rank $n$, eval($S$) = eval($S'$).

- for all $Y$-set-systems $S$ of rank $n$ and all $f \in Y_n$,

$f \sqsubseteq \text{eval}(T)$ for all yields $T$ of $S$ implies $f \sqsubseteq \text{eval}(S)$.

where for $a, b \in Y_n$, we note $a \sqcap b := \text{eval}(a + b)$, and $a \sqsubseteq b$ holds if $a \sqcap b = a$.

For $a \in Y_n$, let $a \upharpoonright$ be $\{b \in Y_n \mid a \sqsubseteq b\}$.

A morphism from the yield-algebra $\mathcal{Y} = (Y, \text{eval})$ to the yield-algebra $\mathcal{Y}' = (Y', \text{eval}')$ is a map of ranked sets $\rho$ from $Y$ to $Y'$ such that $\text{eval}'(\bar{\rho}(S)) = \rho(\text{eval}(S))$ for all $Y$-set-systems $S$.

The two first-items in Definition 60 state that yield-algebras are algebras for the monad of set-systems. The third one state that yield-algebras are invariant under yield-equivalence. The fourth one is a strengthening of it: it states that $\sqsubseteq$ admits some infinite infimums, namely the ones described by set-systems.

Some extra lemmas are required for making this definition fully operational.

As is classical with such a definition, $\sqsubseteq$ happens to be an order, and the operation $\sqcap$ is
in fact an infimum for it. This is the subject of the following statement.

**Lemma 61.** The operation $\sqcap$ is associative, commutative, and idempotent. The relation $\sqsubseteq$ is an order, and $\sqcap$ computes the infimum with respect to $\sqsubseteq$.

**Proof.** Since $a + b$ and $b + a$ are yield-equivalent, $a \sqcap b = b \sqcap a$. Similarly, $a + (b + c)$ being yield-equivalent to $(a + b) + c$, $\sqcap$ is associative. Finally, $a + a$ is yield-equivalent to $a$, and thus $\sqcap$ is idempotent. Transitivity of $\sqsubseteq$: Assume $a \sqsubseteq b$ and $b \sqsubseteq c$, then $a \sqcap c = (a \sqcap b) \sqcap c = a \sqcap (b \sqcap c) = a \sqcap b = a$. Hence $a \sqsubseteq c$. Reflexivity of $\sqsubseteq$: Since $a \sqcap a = a$, $a \sqsubseteq a$. Antisymmetry of $\sqsubseteq$: Assume $a \sqsubseteq b$ and $b \sqsubseteq a$, then $a = a \sqcap b = b \sqcap a = b$. Let us show that $a \sqcap b \sqsubseteq a$. This comes from the fact that $(a \sqcap b) \sqcap a = a \sqcap b$, and hence $a \sqcap b \sqsubseteq a$. Finally, let us assume that $c \sqsubseteq a$ and $c \sqsubseteq b$, then $c \sqcap (a \sqcap b) = (c \sqcap a) \sqcap (c \sqcap b) = c \sqcap c = c$. Hence $c \sqsubseteq a \sqcap b$. $\quad \blacksquare$

In fact, the way we will use yield-algebra is mainly via the following lemma which states
that the evaluation of a set-system is determined by the evaluation of its yields.

**Lemma 62.** Let $\mathcal{Y}$ be a yield-algebra, $f \in Y_n$, and $S$ a $Y$-set-systems of rank $n$,

$f \sqsubseteq \text{eval}(S)$ if and only if $f \sqsubseteq \text{eval}(T)$ for all yields $T$ of $S$.

See proof at page 26.
Proof of Lemma 62. Assume $f \subseteq \text{eval}(S)$ and let $T$ be some yield of $S$, then $S$ and $S+T$ are yield-equivalent. As a consequence, $f \subseteq \text{eval}(S) = \text{eval}(S+T) \subseteq \text{eval}(T)$. This proves the left to right implication. The right to left-implication is simply the fourth axiom in the definition of yield-algebras.

A direct consequence of the previous lemma is the following corollary.

*Corollary 63.* For all Y-set-systems $S, S'$ of same rank, $S \subseteq^{\text{yields}} S'$ implies $\text{eval}(S') \subseteq \text{eval}(S)$.

► **Corollary 63.** For all Y-set-systems $S, S'$ of same rank, $S \subseteq^{\text{yields}} S'$ implies $\text{eval}(S') \subseteq \text{eval}(S)$.

► Remark 64 (yield-algebras are regular-tree algebras). Since systems are particular cases of set-systems, a yield-algebra is in particular an algebra. Furthermore, since yield-equivalence coincide with unfold-equivalence over systems, we obtain that yield-algebras seen as algebras are unfold-invariant, and hence regular-tree algebras. This downgrading of yield-algebras to regular-tree algebras is made implicitly in the rest of this work.

## 4.2 Syntactic yield-algebra for a language of regular-trees

We now introduce the syntactic yield-congruence. This is a variation around the idea of syntactic algebra, tailored for yield-algebras, and giving a special role to the root vertices.

Here, we consider a language $L$ of regular-trees, and shall use the notation $\text{Plant}(L)$ for the set $\{\text{plant}(T) \mid T \in L\}$, ie the same elements but for the fact that initial vertices have been turned into root vertices. In the following definition we use properties of the form $\text{Yields}(S) \subseteq L \cup \text{Plant}(L)$. Unravelling the definitions, it means that all systems produced starting either from an initial vertex or a root vertex have to belong to $L$. It would be equivalent to state it as, for instance, $\text{Plant}(\text{Yields}(S)) \subseteq \text{Plant}(L)$.

► **Definition 65.** Let $\Sigma$ be a ranked set, and $L$ be a language of regular-trees. The yield-syntactic pre-order of $L$ holds between two $\Sigma$-set-systems $S$ and $S'$ of same rank $n$, denoted $S \subseteq^{\text{yield}}_L S'$ if for all closed $\Sigma$-set-contexts $C[\square_n]$,

$$ \text{Yields}(C[S]) \subseteq L \cup \text{Plant}(L) \text{ implies } \text{Yields}(C[S']) \subseteq L \cup \text{Plant}(L). $$

The L-yield-syntactic equivalence is defined as $S \equiv^{\text{yield}}_L S'$ if $S \subseteq^{\text{yield}}_L S'$ and $S' \subseteq^{\text{yield}}_L S$.

$[S]_L^{\text{yield}}$ denotes the L-yield-syntactic equivalence class of $S$. Let $\text{Synt}_L^{\text{yield}}$ be the set of $\equiv^{\text{yield}}_L$-classes of set-systems.

We need some preparatory lemmas. The first one states that $\subseteq_L^{\text{yield}}$ induces an inf-semi-lattice structure.

► **Lemma 66.** $S \subseteq_L^{\text{yield}} S' + S''$ holds if and only if both $S \subseteq_L^{\text{yield}} S'$ and $S \subseteq_L^{\text{yield}} S''$ hold.

► **Proof.** The direction from left to right is obvious.

For the other direction, we claim first that $S \subseteq_L^{\text{yield}} S'$ implies $S \subseteq_L^{\text{yield}} S + S'$. For this, consider some closed $\Sigma$-set-context $C[\square_n]$ such that $\text{Yields}(C[S]) \subseteq L \cup \text{Plant}(L)$. Define now $D[\square_n]$ to be $C[S + \square_n]$. Then we have $\text{Yields}(D[S]) = \text{Yields}(C[S]) \subseteq L \cup \text{Plant}(L)$, and thus by assumption applied on the closed $\Sigma$-set-context $D[\square_n]$, we obtain $\text{Yields}(C[S + S']) = \text{Yields}(D[S']) \subseteq L \cup \text{Plant}(L)$. The claim is proved.

We now have, assuming $S \subseteq_L^{\text{yield}} S'$ and $S \subseteq_L^{\text{yield}} S''$ and using twice the above claim:

$$ S \subseteq_L^{\text{yield}} S + S' \subseteq_L^{\text{yield}} S + S' + S'' \subseteq_L^{\text{yield}} S' + S'' . $$

◄
The second one states that $\equiv_L^{\text{yield}}$ is a congruence relation.

**Lemma 67.** For $S, S' \in \Sigma$-set-systems of same shape such that $S(v) \subseteq_L^{\text{yield}} S'(v)$ for all vertices $v$ of $S$, then $\text{flatten}(S) \subseteq_L^{\text{yield}} \text{flatten}(S')$.

*Proof.* By Lemma 37, we just have to show the result for set-contexts, ie to show that for all $\Sigma$-set-context $C[\Box_k]$ of rank $n$, and all $\Sigma$-set-systems $S \subseteq_L^{\text{yield}} S'$ of rank $k$, $C[S] \subseteq_L^{\text{yield}} C[S']$.

Indeed, let $C[\Box_k], S, S'$ be as above, and let $D[\Box_n]$ be some closed $\Sigma$-set-context. We define the set-context $D \circ C[\Box_k] := D[C[\Box_k]]$. Assuming Yields((D $\circ$ C)[S]) $\subseteq$ L $\cup$ Plant(L), and since $S \subseteq_L^{\text{yield}} S'$, we have Yields((D $\circ$ C)[S']) $\subseteq$ L $\cup$ Plant(L). This is true for all D, so this establishes $C[S] \subseteq_L^{\text{yield}} C[S']$. The lemma then follows from Lemma 37.

It follows that the operation *flatten* can be regarded as acting on $\equiv_L^{\text{yield}}$-equivalence classes. Let us denote $\text{flatten}_L$ the *flatten* operation applied to $\equiv_L^{\text{yield}}$-equivalence classes.

**Lemma 68.** *Given a language of $\Sigma$-regular-trees $L$, ($\text{Synt}_L^{\text{yield}}$, $\text{flatten}_L$) is a yield-algebra for which $\subseteq$ coincide with $\subseteq_L^{\text{yield}}$.*

*Proof.* Our first objective establish that $\subseteq$ and $\subseteq_L^{\text{yield}}$ coincide. Indeed, for all $\Sigma$-set-systems $S, S'$ of rank $n$,

$$[S]_L^{\text{yield}} \subseteq [S']_L^{\text{yield}}$$

if and only if $[S]_L^{\text{yield}} \sqcap [S']_L^{\text{yield}} = [S]_L^{\text{yield}}$, (definition of $\subseteq$)

if and only if $[S + S']_L^{\text{yield}} = [S]_L^{\text{yield}}$, (definition of $\sqcap$)

if and only if $S + S' \equiv_L^{\text{yield}} S$, (definition of $[-]_L^{\text{yield}}$)

if and only if $S \subseteq_L^{\text{yield}} S + S'$, (since $S + S' \subseteq_L^{\text{yield}} S$)

if and only if $S \subseteq_L^{\text{yield}} S'$. (using Lemma 66)

We can now complete the proof that ($\text{Synt}_L^{\text{yield}}$, $\text{flatten}_L$) is a yield-algebra. Only the fourth item needs to be proved, the other following from the fact that $\equiv_L^{\text{yield}}$ is a congruence. Hence, let $f \in \text{Synt}_L^{\text{yield}}$ of rank $n$, and $S$ be a $\text{Synt}_L^{\text{yield}}$-set-system such that $f \subseteq \text{flatten}_L(T)$ for all yields $T$ of $S$. We have to show that $f \subseteq \text{flatten}_L(S)$.

Let $S'$ be a $\Sigma$-set-system such that $f = [S']_L^{\text{yield}}$ and $C[\Box_n]$ be a set-context such that Yields($C[S']$) $\subseteq$ L $\cup$ Plant(L). We know by assumption that $S' \subseteq_L^{\text{yield}} T$ for all yields $T$ of $S$. By Lemma 66, this means that $S' \subseteq_L^{\text{yield}} \sum_{T \in F} T$ for all finite sets $F \subseteq \text{Yields}(S)$. Hence for all such $F$, we have Yields($C[\sum_{T \in F} T]$) $\subseteq$ L $\cup$ Plant(L). Putting it in combination with Corollary 50, we get

$$\text{Yields}(C[S]) = \bigcup_{\substack{F \subseteq \text{Yields}(S) \\ F \text{ finite}}} \text{Yields}\left(C\left[\sum_{T \in F} T\right]\right) \subseteq L \cup \text{Plant}(L).$$

Since this holds for all choice of $C[\Box_n]$, this means $S' \subseteq_L^{\text{yield}} S$, ie $f \subseteq \text{flatten}_L(S)$. $\blacksquare$

Let us call the yield-algebra ($\text{Synt}_L^{\text{yield}}$, $\text{flatten}_L$) the syntactic yield-algebra of $L$, denoted $\mathcal{Y}_L^{\text{Synt}}$.

**Lemma 69.** For $L$ a language of $\Sigma$-regular-trees, the algebra $\mathcal{Y}_L^{\text{Synt}}$ recognises $L$. Moreover, the corresponding accepting set $P \subseteq \text{Synt}_L^{\text{yield}}$ is $\sqsubseteq$-upward closed and closed under $\sqcap$.
**Proof.** Let $P = \{[S]_L^{\text{yield}} | \text{Yields}(S) \subseteq L \cup \text{Plant}(L)\}$. Following the proof of the previous lemma, we obtain that for any $\Sigma$-set-system $S$, we have $[S]_L^{\text{yield}} \in P$ if and only if $\text{Yields}(S) \subseteq L \cup \text{Plant}(L)$, as the yields of $S$ uniquely define the $\equiv_L^{\text{yield}}$-equivalence class of $S$. Accordingly, $P$ is closed under $\sqcap$, and $\sqsubseteq$ upwards.

Moreover, for a regular tree $T$, we have $T \in L$ if and only if $[T]_L^{\text{yield}} \in P$ if and only if $[\text{plant}(T)]_L^{\text{yield}} \in P$. This means that $(\text{Synt}_L^{\text{yield}}, \text{flatten}_L, P)$ recognises $L$ among regular trees. $\blacksquare$

## 4.3 Rankwise finite yield-algebras

The goal of this section is to establish the following lemma.

**Lemma 70.** If a language of regular-trees $L$ is recognised by a rankwise finite algebra, then its syntactic yield-algebra is also rankwise finite.

We fix from now a rankwise finite algebra $A$ that recognises a language of $\Sigma$-regular-trees $L$. Let $\rho$ be the recognising morphism.

The proof of Lemma 70 consists in defining an equivalence relation over $A$-set-systems for each rank, called the *small-$A$-profile-equivalence*. It happens to be of finite index for each sort (this is straightforward) and at the same time to refine the yield-syntactic congruence for $L$ (this is the more involved part proved in Corollary 79). Lemma 70 immediately follows. Let us begin with introducing this notion.

* Given a map $\sigma: [m] \to [n]$, call it *A-small*, or simply *small*, if $|\sigma^{-1}(i)| \le |A_1|$ for all $i \in [n]$. Call a resolution $(T, \sigma)$ *small* if $\sigma$ is small. Given an $\Sigma$-set-system $S$ of rank $n$, its *profile*, its *root-profile*, its *small-profile* and its *small-root-profile* are the sets

$$ 
\begin{align*}
\text{profile}(S) &:= \{(\rho(T), \sigma) \mid (T, \sigma) \text{ is a resolution of } S\}, \\
\text{root-profile}(S) &:= \text{profile}(\text{uproot}(S)), \\
\text{small-profile}(S) &:= \{(\rho(T), \sigma) \mid (T, \sigma) \text{ is a small resolution of } S\}, \\
\text{and } \text{small-root-profile}(S) &:= \text{small-profile}(\text{uproot}(S)).
\end{align*}
$$

Two $\Sigma$-set-systems of rank $n$ are *profile-equivalent* if they share the same profile and the same *root-profile*, and are *small-profile-equivalent* if they share the same *small-profile* and the same *small-root-profile*.

* **Remark 71 (profiles and small-profiles coincide on closed set-systems).** For a closed $\Sigma$-set-system $S$, all resolutions $(T, \sigma)$ are such that $\sigma$ is the empty map $\emptyset$, which is small. Hence small-profile-equivalence and profile-equivalence coincide over closed $\Sigma$-set-systems.

* **Remark 72.** For $S$ and $S'$ *profile-equivalent* closed $\Sigma$-set-systems, $\text{InitYields}(S) \subseteq L$ if and only if $\text{InitYields}(S') \subseteq L$, and $\text{RootYields}(S) \subseteq L$ if and only if $\text{RootYields}(S') \subseteq L$.

We begin with proving that *profile-equivalence* is a congruence. This statement is not strictly speaking useful for our goal, but it helps understanding the need for *small-profiles*, and illustrates perfectly the key arguments that we shall then refine. However it is important to note that we never prove that *small-profile-equivalence* is a congruence.

**Lemma 73 (profile-equivalence is a congruence).** If $S$ and $S'$ are $(\Sigma$-set-system)-set-systems of same shape and such that $S(s)$ and $S'(s)$ are *profile-equivalent* for all vertices $s \in V_S$, then *flatten*($S$) and *flatten*($S'$) are *profile-equivalent*.

* **Proof.** We claim first that $\text{profile}(\text{flatten}(S)) = \text{profile}(\text{flatten}(S'))$. Let $(a, \tau) \in \text{profile}(\text{flatten}(S))$. This means that there is a resolution $(R, \tau)$ of $\text{flatten}(S)$ with $\rho(R) = a$. Hence $\hat{\tau}(R)$ is a
direct resolution of flatten(S), or equivalently R is a direct resolution of $\tau^{-1}(flatten(S)) = flatten(\tau^{-1}(S))$.

By Lemma 46, there exists a flatten-resolution $T$ of $\tau^{-1}(S)$ such that $R$ unfolds to flatten($T$) (and in particular $\rho(flatten(T)) = \rho(R) = a$). Let $(\delta, \sigma)$ be witnessing the flatten-resolution. For all vertices $t$ of $T$, $(T(t), \sigma_t)$ is a resolution of $S(\delta(t))$. Since by assumption $S(\delta(t))$ and $S'(\delta(t))$ are profile-equivalent, there exists $R_t$ such that $(R_t, \sigma_t)$ is a resolution of $S'(\delta(t))$ and $\rho(R(t)) = \rho(T(t))$. Let us define the $(\Sigma$-system)-system $T'$ to be identical to $T$ but for its labelling, for which we set $T'(t) = R_t$. It is clear that $T'$ is a flatten-resolution of $\tau^{-1}(S')$. Furthermore,

$$ \rho(flatten(T')) = \text{eval}(flatten(\bar{\rho}(T'))) = \text{eval}(flatten(\bar{\rho}(T))) = \rho(flatten(T)) = a, $$

and hence $(a, \tau) \in \text{profile}(flatten(S'))$. Since this holds for all $a$, and by symmetry, we get $\text{profile}(flatten(S)) = \text{profile}(flatten(S'))$ as claimed.

Note that the above claim also applies to fuproot($S$) and fuproot($S'$), thus we obtain:

$$ \begin{aligned} \text{root-profile}(flatten(S)) &= \text{profile}(\text{uproot}(flatten(S))) = \text{profile}(flatten(\text{fuproot}(S))) \\ &= \text{profile}(flatten(\text{fuproot}(S')) = \text{profile}(\text{uproot}(flatten(S')) = \text{root-profile}(flatten(S')). \end{aligned} $$

In the end, we have shown that $S$ and $S'$ are profile-equivalent.

By combining Lemma 73 with Remark 72 we immediately obtain the following corollary.

**Corollary 74.** *The profile-equivalence refines the yield-syntactic equivalence.*

So far, it looks almost like a proof of Lemma 70: since the profile-equivalence is a congruence that refines the yield-syntactic congruence for $L$, one would just have to show that it is of rankwise finite index. However, the next example shows that this is not true.

**Example 75 (profile-equivalence is not of rankwise finite index).** Consider the rankwise finite algebra from Example 53, and the morphism used in Example 55 for recognising the language of regular-trees that contain the symbol $b$. Let $T_n$ be some finite regular-tree of rank 1 which has exactly $n$ occurrences of the variable $x_1$ (for instance, set $T_0 := a$, and $T_{n+1} := a_2(T_n, x_1)$). Let us show now that all the $T_n$'s are non-profile-equivalent systems, thus witnessing that profile-equivalence is not of rankwise finite index.

For this, let us denote $1_m$ the constant map from $[m]$ to $[1]$. A resolution of $T_n$ has the form $(R, 1_m)$, in which $R$ is a system of rank $m$ of same shape as $T_n$, but for the fact that the variables $x_1, \dots, x_m$ can be used in place of the $n$ occurrences of $x_1$ in $T_n$. Then, by definition of $\rho$, $\rho(R)$ is the set of variables that occur in at least one place in $R$. Hence when $(R, 1_m)$ ranges over all the resolutions of $T_n$, $\rho(R)$ ranges over all non-empty subsets of $[m]$ of size at most $n$. Ie:

$$ \text{profile}(T_n) = \{(X, 1_m) \mid X \in A_m, 1 \le |X| \le n\}. $$

Hence, for all $m > n > 0$, we have that $([m], 1_m) \in \text{profile}(T_m)$, but $([m], 1_m) \notin \text{profile}(T_n)$, witnessing that $T_m$ and $T_n$ are not profile-equivalent. This shows that profile-equivalence is not of rankwise finite index, since there are infinitely many profiles for rank 1 systems.

In the above example, one sees that there are many profiles, but clearly the yield-syntactic congruence for $L$ is much coarser (it has 3 classes among set-systems of rank 1).

The core of the proof of Lemma 70 consists in showing that if we have a flatten-resolution $T$ of a closed $(\Sigma$-set-system)-set-system $S$, then it can be transformed into another flatten-resolution $T'$ of $S$ that involves only small resolutions in all its subsystems. This is established
XX:30 Tree algebras and bisimulation-invariant MSO on finite graphs

in Lemma 77. We begin with a more local version of the statement, in which the bound $|A_1|$ shows up, namely Lemma 76.

**Lemma 76.** Let $T$ be a $\Sigma$-system of rank $m$, $C[\square_m]$ be a closed $\Sigma$-context, and $\sigma: [m] \to [n]$. Then there exist $m'$ and two maps $\tau: [m] \to [m']$ and $\tau': [m'] \to [m]$ such that

- $\sigma \circ \tau' \circ \tau = \sigma$,

- $\sigma \circ \tau'$ is small, and

- $\rho(C[T]) = \rho(C[\tau' \circ \tau(T)])$.

**Proof.** Let $P, P_1, \dots, P_m$ be the pieces of $C[\square_m]$. For $i, j \in [m]$, let $i \sim j$ hold if $\sigma(i) = \sigma(j)$, and $\rho(P_i) = \rho(P_j)$. Let $X_1, \dots, X_{m'}$ be an enumeration of the $\sim$-equivalence classes, and let $\tau$ be the map which sends each $i \in [m]$ to the index of its $\sim$-equivalence classes, ie it maps $i$ to $k$ for $k$ such that $i \in X_k$. In other words, $\tau: [m] \to [m']$ is defined to be a surjection with the property that $\tau(i) = \tau(j)$ if and only if $i \sim j$. $\tau$ being surjective, one can choose a section $\tau'$ of $\tau$, ie a map $\tau': [m'] \to [m]$ such that $\tau \circ \tau' = \text{Id}_{[m']}$.

For all $i \in [m]$, we have $\tau' \circ \tau(i) \sim i$, and thus by definition of $\sim$, $\sigma(i) = \sigma(\tau' \circ \tau(i))$. Hence $\sigma \circ \tau' \circ \tau = \sigma$.

Let $j \in [n]$ and $i, i' \in (\sigma \circ \tau')^{-1}(j)$. Then $i = i'$ is and only if $\rho(P_{\tau'(i)}) = \rho(P_{\tau'(i')})$. Hence $|(\sigma \circ \tau')^{-1}(j)| \le |A_1|$. We have shown that $\sigma \circ \tau'$ is small.

Furthermore, $\tau' \circ \tau$ is by construction such that $\rho(P_i) = \rho(P_{\tau' \circ \tau(i)})$ for all $i$. Thus we get

$$ \begin{align*} \rho(C[T]) &= \rho(\text{Context}(P, P_1, \dots, P_n)[T]) & \text{by Lemma 38 and Definition 60} \\ &= \text{eval}(\text{Context}(\rho(P), \rho(P_1), \dots, \rho(P_n))[\rho(T)]) & \text{since } \rho \text{ is a morphism} \\ &= \text{eval}(\text{Context}(\rho(P), \rho(P_{\tau' \circ \tau(1)}), \dots, \rho(P_{\tau' \circ \tau(n)}))[\rho(T)]) & \text{from } \rho(P_i) = \rho(P_{\tau' \circ \tau(i)}) \\ &= \text{eval}(\text{Context}(\rho(P), \rho(P_1), \dots, \rho(P_n))[\widehat{\tau' \circ \tau}(\rho(T))]) & \text{by Lemma 39} \\ &= \rho(C[\widehat{\tau' \circ \tau}(T)]) & \text{by Lemma 38.} \end{align*} $$

◀

Let us call a flatten-resolution $T$ of some $(\Sigma$-set-system)-set-system $S$ small if it is witnessed by $(\delta, \sigma)$ with $\sigma_t$ small for all vertices $t$ of $T$.

**Lemma 77.** Let $T$ be a flatten-resolution of a closed $(\Sigma$-set-system)-set-system $S$. There exists a small flatten-resolution $T'$ of $S$ such that

$$ \rho(\text{flatten}(T)) = \rho(\text{flatten}(T')) . $$

**Proof.** Let $T$ be a flatten-resolution of $S$ witnessed by $(\delta, \sigma, \gamma)$. The proof is by downward induction on the number of vertices $t$ of $T$ such that $\sigma_t$ is not small. If this quantity is null, then $T$ is a small flatten-resolution, and the statement is proved.

Otherwise, let $u$ be such that $\sigma_u$ is not small. We can decompose flatten($T$) as $C[T(u)]$ in which $C$ is obtained from $T$ by substituting a hole for $T(u)$, and then flattening. Formally, let $m = \text{rk}(T(u))$, $C$ is obtained from $T$ by first changing $T(u)$ into unit($\square_m$), and then flattening the obtained system-system.

Let us apply Lemma 76 to $T(u)$, $C[\square_m]$ and $\sigma_u$, and get the maps $\tau: [m] \to [m']$ and $\tau': [m'] \to [m]$, satisfying the conclusions of the statement.

We now construct $T'$ to be identical to $T$, but for the following changes:

- $T'(u)$ is $\hat{\tau}(T(u))$ (hence it is of rank $m'$), and

- there is a transition edge of the form $(u, i, t)$ in $T'$ if and only if $(u, \tau'(i), t) \in E_T$ (the transition edges of source different from $u$ are kept unchanged).
Let us show that $\rho(\text{flatten}(T')) = \rho(\text{flatten}(T))$. For this, consider $C'$ defined from $T'$ as $C$ was defined from $T$. We then have

$$ 
\begin{align*}
\rho(\text{flatten}(T)) &= \rho(C[T(u)]) \\
&= \rho(C[\widehat{\tau' \circ \tau}(T(u))]) & \text{by Lemma 76} \\
&= \rho(C'[\hat{\tau}(T(u))]) & \text{by definition of } T' \text{ and thus } C' \\
&= \rho(C'[T'(u)]) & \text{by definition of } T'(u) \\
&= \rho(\text{flatten}(T')) .
\end{align*}
$$

Let us now prove that $(\delta, \sigma', \gamma)$ witnesses that $T'$ is a flatten-resolution of $S$, in which $\sigma'$ is identical to $\sigma$, but for $\sigma'_u = \sigma_u \circ \tau'$. Since $T'$ and $\sigma'$ differ from $T$ and $\sigma$ only at $u$, and $T$ is closed, only two things remain to be checked:

- Since $\gamma_u$ witnesses that $(T(u), \sigma_u)$ is a resolution of $S(\delta(u))$, it is a morphism from $\widehat{\sigma}_u(T(u))$ to $S(\delta(u))$. We have by Lemma 76 that $\sigma_u = \sigma_u \circ \tau' \circ \tau = \sigma'_u \circ \tau$. Thus $\gamma_u$ is also a morphism from $\widehat{\sigma}'_u(\hat{\tau}(T(u))) = \widehat{\sigma}'_u(T'(u))$ to $S(\delta(u))$. Hence $\gamma_u$ is a witness that $(T'(u), \sigma'_u)$ is a resolution of $S(\delta(u))$.

- For all transition edges $(u, i, t) \in E_{T'}$, we have by definition of $E_{T'}$ that $(u, \tau'(i), t) \in E_{T}$. Since $T$ is a flatten-resolution witnessed by $(\delta, \sigma, \gamma)$, we obtain $(\delta(u), \sigma'_u(i), \delta(t)) = (\delta(u), \sigma_u(\tau'(i)), \delta(t)) \in E_S$.

Finally, still by Lemma 76, $\sigma'_t = \sigma_t \circ \tau'$ is small. Hence, the number of vertices $t$ such that $\sigma'_t$ is not small is one less than for $\sigma$. The induction step has been proved. ◀

We can finally establish the key statement of this section, Lemma 70.

**Lemma 78.** For closed $(\Sigma$-set-system)-set-systems $S$ and $S'$ of same shape such that $S(s)$ and $S'(s)$ are small-profile-equivalent for all vertices $s$, then flatten($S$) and flatten($S'$) are profile-equivalent.

**Proof.** We claim first that $\text{profile}(\text{flatten}(S)) = \text{profile}(\text{flatten}(S'))$. Indeed, let $(a, \emptyset) \in \text{profile}(\text{flatten}(S))$, this means that there is a direct resolution $R$ of $S$ with $\rho(R) = a$. By Lemma 46, there exists a flatten-resolution $T$ of $S$ such that $R$ unfolds to flatten($T$). In particular, this means that $\rho(\text{flatten}(T)) = a$. By Lemma 77, there is a small flatten-resolution $T'$ of $S$ such that $\rho(\text{flatten}(T')) = \rho(\text{flatten}(T)) = a$, witnessed by $(\delta, \sigma)$.

By definition of small flatten-resolutions, for all vertices $t$ of $T'$, $(T'(t), \sigma_t)$ is a small resolution of $S(\delta(t))$. Since $S(\delta(t))$ and $S'(\delta(t))$ are small-profile-equivalent by hypothesis, there exists $R_t$ such that $(R_t, \sigma_t)$ a small resolution of $S'(\delta(t))$ and $\rho(R(t)) = \rho(T'(t))$. Let us define the $(\Sigma$-system)-system $T''$ to be identical to $T'$ but for its labelling, for which we set $T''(t) = R_t$.

It is clear that $T''$ is a flatten-resolution of $S'$. Furthermore,

$$ \rho(\text{flatten}(T'')) = \text{eval}(\text{flatten}(\bar{\rho}(T''))) = \text{eval}(\text{flatten}(\bar{\rho}(T'))) = \rho(\text{flatten}(T')) = a . $$

This witnesses that $(a, \emptyset) \in \text{profile}(\text{flatten}(S'))$.

Overall, since this holds for all $a$, and by symmetry, we have proved that $\text{profile}(\text{flatten}(S)) = \text{profile}(\text{flatten}(S'))$.

Note that the above claim also applies to fuproot($S$) and fuproot($S'$), thus we obtain:

$$ 
\begin{align*}
\text{root-profile}(\text{flatten}(S)) &= \text{profile}(\text{uproot}(\text{flatten}(S))) = \text{profile}(\text{flatten}(\text{fuproot}(S))) \\
&= \text{profile}(\text{flatten}(\text{fuproot}(S')))) = \text{profile}(\text{uproot}(\text{flatten}(S')))) = \text{root-profile}(\text{flatten}(S'))).
\end{align*}
$$

In the end, we have shown that $S$ and $S'$ are profile-equivalent. ◀
We are now ready to conclude the proof of Lemma 70.

► **Corollary 79.** *The small-profile-equivalence refines $\equiv_L^{\text{yield}}$.*

Proof. Let $S$ and $S'$ be two small-profile-equivalent Σ-set-systems of rank $k$, and $C[\square_k]$ be a closed Σ-set-context. From Lemma 78, $C[S]$ and $C[S']$ are profile-equivalent. Hence for all $T \in \text{Yields}(C[S])$, there exists $T' \in \text{Yields}(C[S'])$ such that $\rho(T) = \rho(T')$. Since $\rho$ recognises $L$, this means that $\text{Yields}(C[S']) \subseteq L$ implies $\text{Yields}(C[S]) \subseteq L$. Since this holds for all $C$, we have $S \subseteq^{\text{yield}} S'$, and by symmetry also $S' \subseteq^{\text{yield}} S$. ◀

This achieves the proof of Lemma 70, since it is clear that small-profile-equivalence is of rankwise finite index.

**5 The automaton property**

In Section 5.1, we define deterministic elements and deterministic yield-algebras. The crux of our construction lies in Section 5.2, in which we define the automaton property, and we show that syntactic yield algebras have the automaton property. This will be the key to the proof of Theorem 93 translating rankwise finite algebras to automata in Section 6.

**5.1 Deterministic elements and deterministic yield-algebras**

For a yield-algebra $\mathcal{Y} = (Y, \text{eval})$, denote $Y_{\le 1}$ the ranked alphabet $Y$ from which all symbols

of rank 2 or above are removed. We define now the *deterministic elements* of the algebra as the *ranked set Det($\mathcal{Y}$)*, where, for all natural numbers $k$:

$$ \text{Det}(\mathcal{Y})_k := \{\text{eval}(S) \mid S \text{ is a } Y_{\le 1}\text{-set-system of rank } k\}. $$

► **Remark 80.** $\text{Det}(\mathcal{Y})$ is a sub-yield-algebra of $\mathcal{Y}$. Indeed, since flattening a $(Y_{\le 1}\text{-set-system})$-set-system yields a $Y_{\le 1}\text{-set-system}$, we immediately have that $\text{eval}(S)$ for $S$ a $\text{Det}(\mathcal{Y})$-set-system belongs to $\text{Det}(\mathcal{Y})$. In other words, *deterministic elements* form a sub-yield-algebra of $\mathcal{Y}$.

The next lemma provides a normalised presentation for deterministic elements:

► **Lemma 81.** *Elements of rank 0 and 1 are deterministic. An element $a \in Y_k$ of rank $k \ge 1$ is deterministic if and only if there exists $(a_1, \dots, a_k) \in Y_1^k$ such that:*

$$ a = \text{eval} \left( \sum_{i=1}^{k} a_i(x_i) \right). $$

Proof. *From left to right.* Let $a$ be a deterministic element of rank $k \ge 1$. This means that there exists a $Y_{\le 1}\text{-set-system } S$ of rank $k$ such that $a = \text{eval}(S)$. For all $i \in [k]$, let $S_i$ be the rank 1 set-system $\hat{\sigma}_i^{-1}(S)$ in which $\sigma_i: [1] \to [k]$ is the constant map equal to $i$. In other words, the variable $x_i$ becomes $x_1$, and all the others are removed. Since $\sigma_i \circ \sigma_i^{-1} \subseteq \text{Id}_{[k]}$, all yields (resp. root yields) of $\hat{\sigma}_i(S_i)$ are also yields (resp. root yields) of $S$. Hence $a = \text{eval}(S) \subseteq \hat{\sigma}_i(S_i) = a_i(x_i)$. Hence, $a \subseteq \text{eval}(\sum_{i=1}^k a_i(x_i))$ follows.

For the other inequality, let $T$ be some yield of $S$. Up to *unfold-equivalence*, we can assume $T$ to be restricted to its vertices reachable from the initial vertex (see Remark 18). Since $S$ is a $Y_{\le 1}\text{-set-system}$, all symbols appearing in $S$ are of rank 0 or 1, and hence, there is at most one *variable edge* in $T$, let us say corresponding to *variable $x_i$*. In this case, $T$ is also a yield of $S_i$. If there is no *variable edge*, then $T$ is also a yield of $S_1$ (this is why we need $k \ge 1$). The same holds for *root yields*. Hence $\text{eval}(\sum_{i=1}^k a_i(x_i)) \subseteq a$.
From right to left. Conversely, $\mathrm{eval}(\sum_{i=1}^k a_i(x_i))$ is by definition $\mathrm{eval}(a_1(x_1)+\dots+a_k(x_k))$, ie the value of a $Y_{\le 1}$-set-system. Hence it is deterministic. ◀

A yield-algebra is *deterministic* if all its elements are deterministic, ie $\mathcal{Y} = \mathrm{Det}(\mathcal{Y})$. Note that a deterministic yield-algebra is entirely generated by its ranks 0 and 1.

## 5.2 Rankwise finite syntactic yield-algebras have the automaton property

In this section, we define what it means for a rankwise finite yield-algebra and a suitable subset $f \uparrow$ to have the automaton property (Definition 82). This will in turn be used in Section 6 to prove that languages recognised by such objects are accepted by automata (Theorem 93).

**Definition 82.** Let $\mathcal{Y} = (Y, \mathrm{eval})$ be rankwise finite yield-algebra and $f \in Y_0$. The pair $(\mathcal{Y}, f \uparrow)$ has the automaton property if for all closed $Y$-set-contexts $C[\square_n]$ and all $a \in Y_n$ such that $f \subseteq \mathrm{eval}(C[a])$, there exists $\delta \in \mathrm{Det}(\mathcal{Y})_n$ such that:

- $\delta \subseteq a$, and

- $f \subseteq \mathrm{eval}(C[\delta])$.

We establish now a sufficient condition for a yield-algebra $\mathcal{Y}$ and a subset $f \uparrow$ to have the automaton property. This sufficient condition in particular applies to rankwise finite syntactic yield-algebras as seen above. The core result is as follows.

**Lemma 83.** Let $\mathcal{Y} = (Y, \mathrm{eval})$ be a rankwise finite yield-algebra and $f \in Y_0$ such that:

1. $f \subseteq \mathrm{eval}(S)$ if and only if $f \subseteq \mathrm{eval}(\mathrm{plant}(S))$, for all $Y$-set-systems $S$, and

2. For all $a, b \in Y_k$, if for all closed $Y$-set-context $C[\square_k]$, $f \subseteq \mathrm{eval}(C[a])$ implies $f \subseteq \mathrm{eval}(C[b])$, then $a \sqsubseteq b$, then $(\mathcal{Y}, f \uparrow)$ has the automaton property.

The rest of the section is devoted to proving Lemma 83. From now, we assume that $\mathcal{Y}$ and $f \in Y_0$ satisfy the hypotheses of Lemma 83, and we aim at showing that $(\mathcal{Y}, f \uparrow)$ has the automaton property.

For establishing the automaton property (Definition 82), we consider some closed $Y$-set-context $C[\square_k]$ and $a \in Y_k$ such that $f \subseteq C[a]$, and have to construct a deterministic element $\delta \in \mathrm{Det}(\mathcal{Y})_k$ such that $\delta \subseteq a$ and $f \subseteq C[\delta]$.

Note first that when $k \le 1$, $a$ belongs to $\mathrm{Det}(\mathcal{Y})_k$, and hence $\delta := a$ does satisfy the expectation. Hence, from now, we assume without loss of generality that $k \ge 2$.

The proof now proceeds as follows. (a) We first construct a closed $Y$-set-context $M[\square_k]$ which is “more difficult” than $C[\square_k]$ and “maximally difficult” while still having $f \subseteq M[a]$. Then (b) we combine the pieces of $M$ with $a$ for constructing a set-system $\Delta$ of value $\delta := \mathrm{eval}(\Delta)$. Then, we successively prove that $\delta$ is deterministic (Lemma 85), $f \subseteq C[\delta]$ (Lemma 86), and $\delta \subseteq a$ (Lemma 87). From this, it directly follows that $(\mathcal{Y}, f \uparrow)$ has the automaton property.

### Choice of an extremal context.

The next lemma shows the existence of a context of the form $\mathrm{Context}(m_0, \dots, m_k)$ which is “more difficult than $C$” (first item), “compatible with $C$ for accepting $a$” (second item), and “minimal with this property” (third item).

**Lemma 84.** There exist $m_0, \dots, m_k \in Y_1$ such that:

See proof at page 34.
XX:34 Tree algebras and bisimulation-invariant MSO on finite graphs

- eval(Context($m_0, \dots, m_k$))[b] ⊑ eval(C[b]) for all $b \in Y_k$,

- $f \subseteq eval(Context(m_0, \dots, m_k)[a])$, and

- for all $t \in Y_1$ and $i \in \{0, \dots, k\}$ such that

$$f \subseteq eval(Context(m_0, \dots, m_{i-1}, m_i + t, m_{i+1}, \dots, m_k)[a]),$$

we have $m_i \subseteq t$.

Proof of Lemma 84. Let $P_0, \dots, P_k$ be the pieces of $C$, and $p_i = eval(P_i)$ for all $i \in \{0, \dots, k\}$. We know that $eval(Context(p_0, \dots, p_k)[b]) = eval(Context(P_0, \dots, P_k)[a]) = eval(C[b])$ for all $b \in Y_k$. In particular $f \subseteq eval(context(p_0, \dots, p_k)[a])$.

Let $Z \subseteq (Y_{\le 1})^{k+1}$ be the set of tuples $(t_0, \dots, t_k)$ such that (a) $t_i \subseteq p_i$ for all $i \in \{0, \dots, k\}$, and (b) $f \subseteq eval(context(t_0, \dots, t_k)[b])$.

This set $Z$ is non-empty, since it contains $(p_0, \dots, p_k)$. It is also finite since $Y$ is rankwise finite. Hence, one can choose $(m_0, \dots, m_k) \in Z$ componentwise minimal with respect to $\subseteq$. Clearly this choice of $m_0, \dots, m_k$ satisfies the two first items of the conclusion of the lemma. For the third item, let us consider some $t \in Y_1$ and $i \in \{0, \dots, k\}$ such that $f \subseteq eval(context(m_0, \dots, m_{i-1}, m_i + t, m_{i+1}, \dots, m_k))$. This means that $f \subseteq eval(context(m_0, \dots, m_{i-1}, m_i \sqcap t, m_{i+1}, \dots, m_k))$. Since furthermore $m_i \sqcap t \subseteq m_i \subseteq p_i$, we have $(m_0, \dots, m_{i-1}, m_i \sqcap t, m_{i+1}, \dots, m_k) \in Z$. By minimality in the choice of $(m_0, \dots, m_k)$, in combination with $m_i \sqcap t \subseteq m_i$, we obtain $m_i \sqcap t = m_i$. Hence $m_i \subseteq t$. ◀

From now on, we assume $m_0, \dots, m_k$ chosen according to Lemma 84, and we define:

$$M[\square_k] := \text{plant}(Context(m_0, \dots, m_k)[\square_k]).$$

Note in particular, from the assumptions of Lemma 83 that $f \subseteq eval(M[a])$.

**Construction of** $\delta := eval(\Delta)$

For all $i \in [k]$ we define $Y$-set-systems $U_i$ of rank 1 and a $Y$-set-system $\Delta$ of rank $k$ as depicted below:

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

We also set $\delta$ to be eval($\Delta$).

**Lemma 85.** $\delta \in \text{Det}(\mathcal{Y})_k$.

Proof. Since the $U_i$'s are of rank 1, their evaluation belongs to $Y_{\le 1}$, hence $\delta$ can be written as the evaluation of a $Y_{\le 1}$-set-system, and as consequence $\delta$ is deterministic. ◀

**Lemma 86.** $f \subseteq eval(C[\delta])$.

Proof. Below are depicted the closed $Y$-set-systems $M[\Delta]$ and $M[a]$:
<figure><img src="image_16.png" /></figure>

There is a straightforward morphism from $M[\Delta]$ to $M[a]$: it consists in sending each $m_i$'s in $M[\Delta]$ to its unique occurrence in $M[a]$, and similarly for $a$. Hence, $M[\Delta] \subseteq^yields M[a]$, which by Corollary 63 implies $\mathrm{eval}(M[a]) \subseteq \mathrm{eval}(M[\Delta])$. By Lemma 84 we also have $\mathrm{eval}(M[\Delta]) \subseteq \mathrm{eval}(C[\Delta])$. Hence $f \subseteq \mathrm{eval}(M[a]) \subseteq \mathrm{eval}(M[\Delta])$. By Item 1 of Lemma 83, we obtain $f \subseteq \mathrm{eval}(\mathrm{Context}(m_0, \dots, m_k)[\Delta]) \subseteq \mathrm{eval}(C[\Delta]) = \mathrm{eval}(C[\delta])$. $\blacksquare$

► Lemma 87. $\delta \subseteq a$.

► Proof. Using the assumptions of Lemma 83, it is sufficient to prove that for all closed Y-set-contexts $D[\square_k]$, $f \subseteq \mathrm{eval}(\mathrm{plant}(D[\delta]))$ implies $f \subseteq \mathrm{eval}(\mathrm{plant}(D[a]))$.

Without loss of generality, we assume $D$ of the form $D[\square_k] = \mathrm{Context}(t_0, t_1, \dots, t_k)$. We assume that $f \subseteq \mathrm{eval}(\mathrm{plant}(D[\delta]))$, and aim at showing that $f \subseteq \mathrm{eval}(\mathrm{plant}(D[a]))$. Let us depict first the closed set-context plant($D[\square_k]$), and plant($D[\Delta]$):

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

We claim that $m_i \subseteq t_i$ for all $i \in [k]$. Let us fix $i \in [k]$, and define:

$$T_i := \mathrm{plant}(\mathrm{Context}(m_0, \dots, m_{i-1}, m_i + t_i, m_{i+1}, \dots, m_k))[a].$$

In picture, we get:

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

Note that, starting from plant($D[\Delta]$), after removing the $t_0$-vertex, removing the $U_j$'s with $j \neq i$ as well as all the $t_i$-vertices' for $j \neq i$, we obtain $T_i$. This means that there is an (injective) morphism from $T_i$ to plant($D[\Delta]$). This implies $T_i \subseteq^yields \mathrm{plant}(D[\Delta])$ and thus, by Corollary 63, $f \subseteq \mathrm{eval}(\mathrm{plant}(D[\Delta])) \subseteq \mathrm{eval}(T_i)$. By Lemma 84, we obtain $m_i \subseteq t_i$.

We claim now that $m_0 \subseteq t_0$. The proof is similar. Let us consider the closed set-system

$$S := \mathrm{plant}(\mathrm{Context}(m_0 + t_0, m_1, \dots, m_k))[a]$$

depicted below:
XX:36 Tree algebras and bisimulation-invariant MSO on finite graphs

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

Note that, starting from plant(D[Δ]) and removing all the vertices of the $t_i$'s (recall that the variable $x$ of $U_i$ appears just after a nondeterministic choice, so this is a valid partial resolution of nondeterminism) as well as all the vertices of the $U_i$'s for $i \ge 2$, the resulting set-system is isomorphic to $S$. This means that there is an (injective) morphism from $S$ to plant(D[Δ]) witnessing that $S \subseteq^y \text{plant}(D[Δ])$. Hence, using Corollary 63, $f \subseteq \text{eval}(\text{plant}(D[Δ])) \subseteq \text{eval}(S)$. By Lemma 84, we get $m_0 \subseteq t_0$.

**Conclusion:** Overall, we obtain that

$$ 
\begin{align*}
f \subseteq \text{eval}(M[a]) \\
&= \text{eval}(\text{plant}(\text{Context}(m_0, \dots, m_k)[a])) \tag{by definition of $M$} \\
&\subseteq \text{eval}(\text{plant}(\text{Context}(t_0, \dots, t_k)[a])) \tag{since $m_i \subseteq t_i$ for all $i$} \\
&= \text{eval}(\text{plant}(D[a])) .
\end{align*}
$$

From the assumptions of Lemma 83, this means $f \subseteq \text{eval}(D[a])$. Since furthermore this holds for all choices of $D$, this means $\delta \subseteq a$. $\blacksquare$

**Corollary 88.** Let $L$ be a language of $\Sigma$-regular-trees recognised by a rankwise finite algebra. Then the syntactic yield-algebra of $L$ has the automaton property.

**Proof.** By Lemma 69, the syntactic yield-algebra $\mathcal{Y}$ of $L$ has elements of the form $[S]^y_L$ for $S$ $\Sigma$-set-systems. The accepting set $P$ verifies $[S]^y_L \in P$ if and only if $\text{Yields}(S) \subseteq L \cup \text{Plant}(L)$, and $P$ is closed under $\sqcap$ and $\upharpoonright$. Since $\mathcal{Y}$ is rankwise finite by Lemma 70, $P$ is finite as a subset of $\mathcal{Y}_0$. This means that if we take $f = \bigcap_{x \in P} x$, we have $f \upharpoonright = P$.

The first hypothesis of Lemma 83 amounts to showing that for all $\Sigma$-set-systems $S$, $\text{Yields}(S) \subseteq L \cup \text{Plant}(L)$ if and only if $\text{Yields}(\text{plant}(S)) \subseteq L \cup \text{Plant}(L)$. This follows from the fact that by definition of Yields, for any $\Sigma$-set-system $S, T$, we have

- $T \in \text{Yields}(S)$ if and only if $\text{plant}(T) \in \text{Yields}(\text{plant}(S))$,

- $T \in \text{Yields}(\text{plant}(S))$ if and only either $T \in \text{Yields}(S)$ or $\text{plant}(T) \in \text{Yields}(S)$.

For the second hypothesis of Lemma 83, let $a, b \in \mathcal{Y}_k$ such that for all closed $Y$-set-context $C[\square_k]$, $\text{eval}(C[a]) \in P$ implies $\text{eval}(C[b]) \in P$. Let $D[\square_k], A, B$ be $\Sigma$-set-systems evaluating to $C[\square_k], a, b$ respectively. We have to show that $a \subseteq b$. This means that $\text{Yields}(D[A]) \subseteq L \cup \text{Plant}(L)$ implies $\text{Yields}(D[B]) \subseteq L \cup \text{Plant}(L)$. This is the definition of $A \subseteq^y B$, and Lemma 68 states that this implies $a \subseteq b$. $\blacksquare$

# 6 MSO, automata, bisimulation and $\mu$-calculus

In this section, we combine the different tools seen so far, and complete the proof of our main theorems.

We use standard definitions of the Monadic Second-Order logic (MSO) and $\mu$-calculus. We assume the reader has a good familiarity with MSO. Further definitions and notations can be found in [21]. We shall use finite signatures containing relational symbols only (ie no functional symbols). The notion of a structure over a given signature is the usual one. Given a formula in some logic $\varphi$, and a structure $S$, we say that $S$ models $\varphi$, noted $S \models \varphi$, if the sentence $\varphi$ is true when evaluated in the structure $S$.
In Section 6.1, we define transition systems, and in Section 6.2 we see how MSO and μ-calculus can express properties about them.

We show in Section 6.3 that MSO and finite rank algebras are equi-expressive for defining languages of regular-trees. Finally, in Section 6.4, we use this result in the fragment of bisimulation-invariant languages to show that bisimulation-invariant MSO and μ-calculus are equi-expressive.

## 6.1 Transition systems as systems, and bisimulation

In this section, we define the notion of transition systems, which is the classical one, and state how these objects can be encoded in Tr-systems, where Tr is a suitably defined ranked alphabet. We shall also see how to define a notion of “bisimulation” over Tr-systems that corresponds to the usual definition of bisimilarity (see Lemma 89).

Let us fix a finite set $\mathcal{P}$ of unary predicates.

A transition system $(V, i, T, \gamma)$ consists$^8$ of a finite set of vertices $V$, an initial vertex $i$, a binary relation $T$ called the transition relation, and a labelling function $\gamma : V \to 2^P$.

We now explain how to encode transition systems as systems as defined in this document.

Let Tr be the ranked alphabet which has an element $\nu_n$ of rank $n$ for all P-valuation $\nu \in 2^P$, and all $n \in \mathbb{N}$. A transition system is a Tr-system. Given a closed Tr-system $S$, its decoding is the transition system $decode(S)$ that has the same set of vertices with same labelling, the same initial vertex, and $T(u, v)$ holds if $(u, d, v)$ is an edge for some $d$. Conversely, $S$ is called an encoding of $decode(S)$. Note that the decoding is unique, while several non-isomorphic Tr-systems may encode the same transition system. Note also that all transition systems admit at least one encoding (we use here the assumption that transition systems are finite).

In this work, we define the *bisimilarity* relation as the least equivalence relation over closed Tr-systems that contains unfold-equivalence and the relation “encoding the same transition system”. The following lemma states why this is consistent with the standard terminology.

**Lemma 89.** Two Tr-systems are bisimilar if and only if their decodings are “bisimilar in the usual sense”.

*Proof.* Let us recall the following definition of “usual bisimulation”. Two transition systems $(V, i, T, \gamma)$ and $(V', i', T', \gamma')$ of respective vertices sets $V, V'$ are “usual-bisimilar” if there exists a relation $R \subseteq V \times V'$ such that $R(i, i')$, and for all $R(x, x')$:

- $\gamma(x) = \gamma'(x')$,

- For all $y$ such that $T(x, y)$ there exists $y' \in V'$ such that $T'(x', y')$ and $R(y, y')$.

- For all $y'$ such that $T'(x', y')$ there exists $y \in V$ such that $T(x, y)$ and $R(y, y')$.

Let now $S, S'$ be Tr-systems. we have to show that $decode(S)$ and $decode(S')$ are usual-bisimilar if and only if $S$ and $S'$ are bisimilar according to our definition.

*First direction.* Assume that $decode(S) = decode(S')$, then clearly $decode(S)$ and $decode(S')$ are usual-bisimilar, witnessed by the identity relation. Assume now that $S$ unfolds to $S'$, ie that there is a morphism $\eta$ from $S'$ to $S$, then the graph of $\eta$ is a witness of usual-bisimilarity between $decode(S)$ and $decode(S')$. Hence, by transitivity, if $S$ and $S'$ are bisimilar, then $decode(S)$ and $decode(S')$ are usual-bisimilar.

<footnote>$^8$ In this work, as for systems, transition systems are finite, unless explicitly stated otherwise. We chose here to label only vertices and not transitions for simplicity, as opposed, say, to [14]. This choice is purely for simplifying the presentation, and its adaptation to richer models is straightforward.</footnote>
Converse direction. It is sufficient to show, given two usual-bisimilar transition systems $\mathcal{T} = (V, i, T, \gamma)$ and $\mathcal{T}' = (V', i', T', \gamma')$, that there exist two bisimilar Tr-systems $S$ and $S'$ that respectively encode $\mathcal{T}$ and $\mathcal{T}'$.

We first claim that the result holds when the relation $R \subseteq V \times V'$ that witnesses that $\mathcal{T}$ and $\mathcal{T}'$ are usual-bisimilar is the graph of a map $\eta$ from $V$ to $V'$. Let $n$ be the maximal out-degree of a vertex $v \in V$. We define $S'$ to have the same vertices, and initial vertex as $\mathcal{T}'$. For all vertices $v' \in V'$ of label $\nu$ and successors $v'_1, \dots, v'_{n'}$ in $\mathcal{T}'$ (chosen in some fixed order), we set $\text{label}_S(v') := \nu_{nn'}$ and for $i \in [n']$, and $j = 0 \dots n-1$, the $(i+n'j)$-th-successor of $v'$ (in $S'$) to be $v'_i$. Clearly, $\text{decode}(S') = \mathcal{T}'$. We now define $S$ to have the same vertices and initial vertex as $\mathcal{T}$. For all vertices $v \in V$ we set $\text{label}_S(v) := \text{label}_{S'}(\eta(v))$. Now, let $v'_1, \dots, v'_{n'}$ (chosen in the same order as above) be the successors vertices of $\eta(v)$, and for each $i \in [n']$, let $v_{i,0}, \dots, v_{i,k_{i}-1}$ be the successors of $v$ that are mapped by $\eta$ to $v'_i$. By definition of bisimulation, $1 \le k_i$, and hence $v_{i,0}$ is well defined. We define the $(i+nj)$th-successor of $v$ in $S$ to be $v_{i,j}$ if $j < k_i$, and $v_{i,0}$ otherwise. Note that by choice of $n$, $k_i \le n$, and as a consequence, all successors of $v$ in $\mathcal{T}$ are also successors of $v$ in $S$. It is also easy to check that the image of $(i+nj)$th-successor of $v$ by $\eta$ is $v'_i$. As a consequence, $S$ is such that $\text{decode}(S) = \mathcal{T}$, and $\eta$ is a morphism from $S$ to $S'$. This concludes the proof of the claim.

Let us assume now that $R \subseteq V \times V'$ is a witness that $\mathcal{T} = (V, i, T, \gamma)$ and $\mathcal{T}' = (V', i', T', \gamma')$ are usual-bisimilar. We construct the new transition system $\mathcal{T}_R = (R, (i, i'), T_R, \gamma_R)$, where $T_R = \{( (x, x'), (y, y') ) \in R^2 \mid T(x, y), T(x', y') \} \text{ and } \gamma_R(x, x') = \gamma(x) = \gamma'(x')$. It is easy to check that the projection on the first component is a map from $R$ to $V$ that witnesses that $\mathcal{T}$ and $\mathcal{T}_R$ are usual-bisimilar. The same holds for $\mathcal{T}'$ and $\mathcal{T}_R$. It follows from the above claim that there exist Tr-systems $S, S'_R, S'_R$, such that $\text{decode}(S) = \mathcal{T}$, $\text{decode}(S_R) = \mathcal{T}_R$, $\text{decode}(S'_R) = \mathcal{T}_R$, $\text{decode}(S') = \mathcal{T}'$, $S$ unfolds to $S_R$, and $S'$ unfolds to $S'_R$. As a consequence $S$ and $S'$ are bisimilar. $\quad \blacksquare$

## 6.2 Monadic second-order logic, and the composition method

<footnote>Monadic second-order logic (or simply MSO) is the extension of first-order logic with set variables $X, Y, Z, \dots$, the possibility to write existential and universal set quantifiers, and a membership predicate $x \in Y$ expressing that an element belongs to a set.</footnote>

<footnote>The sentence $\psi$ is bisimulation-invariant if for all bisimilar transition systems $S, S'$, we have $S \models \psi$ if and only if $S' \models \psi$. Note that in the context of this work, systems are assumed finite, hence unless explicitly stated, or in the introduction, bisimulation-invariant implicitly means “over finite transition systems”.</footnote>

<footnote>The argument used for translating MSO to algebra is a mere use of the “composition method” which consists in using the fact that for suitable logics, and suitable operations allowing to build structures from simpler ones, then the set of sentences of a structure satisfied by the result can be deduced from the sentences satisfied by the components. We shall use this principle for MSO logic under quantifier depth⁹ bound. Essentially, it uses the fact (1) that if the signature is relational and finite, then there are finitely many semantically distinct MSO-sentences of quantifier depth at most $d$, and (2) when composing several structures (in particular using the flatten operation), the MSO-sentences of quantifier at most $d$ that hold on the result can be deduced from the MSO-sentences of quantifier at most $d$ that hold on the substructures. This is sufficient for showing that the syntactic congruence is finite:</footnote>

<footnote>With the same argument as Lemma 59, we get:</footnote>

<footnote n="9">⁹ The quantifier depth of a sentence is the maximal number of nested quantifiers.</footnote>
**Lemma 90.** Given an MSO-sentence $\varphi$, the set $\{S \text{ Tr-system} \mid \text{decode}(S) \models \varphi\}$ is recognisable by a rankwise finite algebra.

We obtain in turn:

**Lemma 91.** Let $\varphi$ be an MSO-sentence such that for all bisimulation-equivalent closed transition systems $S, S'$, we have $S \models \varphi$ if and only if $S' \models \varphi$. Then the set $\{S \text{ closed transition system} \mid S \models \varphi\}$ is recognised by a rankwise finite algebra.

## 6.3 From algebra to automata in the unfold-invariant setting

As in the previous section, we will consider that the alphabet $\Sigma$ labelling the nodes of transition systems is Tr, i.e. based on a finite set $\mathcal{P}$ of predicates, and containing for each $n \in \mathbb{N}$ and $\nu \in 2^\mathbb{P}$ an element $\nu_n$. We note $\Sigma_n$ the set of elements of rank $n$ of $\Sigma$, and $\Sigma_{>0} = \bigcup_{n>0} \Sigma_n$.

Before considering bisimulation-invariant language, let us consider the more general unfold-invariant case. We will show that already in this case, we can go from rankwise finite algebra to automata, which is a result that we think is interesting in its own right.

Let us start by defining an appropriate notion of automaton for this setting. These automata will process $\Sigma$-systems in a way that is insensitive to unfolding, so they can actually be seen as recognising regular-trees:

**Definition 92.** An unfold-automaton is a tuple $\mathcal{B} = (X, \Sigma, \Delta, \Omega)$ where

- $X = X_1 \oplus X_0$ is a finite set of unary and nullary types,

- $\Sigma$ is the ranked alphabet of the automaton,

- $\Delta = (\Delta_+, \Delta_0)$ is the transition relation, with $\Delta_+ : \Sigma_{>0} \to \mathcal{P}(X_1^+)$ where for each $a \in \Sigma_{>0}$, we have $\Delta_+(a) \subseteq X_1^{\text{rk}(a)}$, and $\Delta_0 : \Sigma_0 \to \mathcal{P}(X_0)$

- $\Omega \subseteq X_1^* X_0 \cup X_1^\omega$ is an $\omega$-regular acceptance condition.

We will simply note $\Delta(a)$ for either $\Delta_+(a)$ or $\Delta_0(a)$ depending on the rank of $a$.

Such automata will be used to recognise a set of regular-trees in the following way. Recall that a regular-tree is an equivalence class of finite transition systems under unfold-equivalence, and that each regular-tree $r$ can be canonically represented by an infinite regular tree $T_r$ in the usual sense. Such a tree $T_r$ is a pair $(D, t)$ where $D \subseteq \mathbb{N}^*$ is the prefix-closed domain, and $t: D \to \Sigma$ is the labelling function consistent with the arities, i.e. for all $d \in D$, the symbol arity $\text{rk}(t(d))$ must correspond to the number of children of $d$ in $D$.

A run of an unfold-automaton $\mathcal{B}$ on a regular-tree $r$ is a labelling of the edges and leaves of $T_r = (D, t)$ by elements of $X_1$ and $X_0$ respectively, consistent with the transition function $\Delta$:

- for all internal node $d \in D$, if $e_1, \dots, e_k$ are the edges from $d$ to its children $d \cdot 1, \dots, d \cdot k$ respectively, we have $(\rho(e_1), \dots, \rho(e_k)) \in \Delta_+(t(d))$.

- for all leaf $d \in D$, we have $\rho(d) \in \Delta_0(t(d))$.

- $\rho$ is accepting if for all (finite or infinite) branch $b$ of $T_r$, we have $\rho(b) \in \Omega$, where $\rho$ is applied componentwise on $b$.

Notice that choosing a run amounts to choosing for each node labelled $a$ an element of $\Delta(a)$. The formalism of unfold-automaton is stateless, because states are abstracted away in the acceptance condition $\Omega$, that is allowed to be an arbitrary $\omega$-regular language. We chose here to describe the automaton as running on the unfolded tree, but it is equivalent to consider that a regular-tree $r$ is accepted if there is run labelling a finite system in the class
XX:40 Tree algebras and bisimulation-invariant MSO on finite graphs

r. This is because the existence of a run of an automaton on an infinite tree is equivalent to
the existence of a regular run, by Rabin's theorem.

We are now ready to state the main result of this section:

**► Theorem 93.** Let $L$ be a language of regular-trees recognised by a rankwise finite algebra. Then $L$ can be recognised by an unfold-automaton.

The rest of this section is devoted to the proof of this theorem. Using Corollary 88, we can assume that the syntactic set-algebra ($\mathcal{Y}$, eval, $f^\uparrow$) has the automaton property. As the name of this property suggests, we shall use this to build an unfold-automaton $\mathcal{B} = (X, \Sigma, \Delta, \Omega)$.

We choose as set of types $X_1 = Y_1$ and $X_0 = Y_0$, i.e. the elements of sort 1 and 0 of $\mathcal{Y}$ respectively.

Let us define the acceptance condition $\Omega \subseteq Y_1^\omega \cup Y_1^*Y_0$. First of all, elements of $Y_1^*Y_0$ are in $\Omega$ if they evaluate to an element of the accepting set $P$ of the algebra: they can simply be viewed as finite systems, and evaluated accordingly. See the left of Figure 4 for an example.

In order to define the acceptance of infinite branches, we need to consider the evaluation of arbitrary elements $\vec{u} = u_0u_1u_2u_3...$ of $Y_1^\omega$ (the subscript of $u_i$ is not its rank here). According to Ramsey's theorem, there exists elements, $a_1, e_1 \in Y_1$ such that $\vec{u}$ can be factorized as $\vec{u} = \vec{v}_0\vec{v}_1\vec{v}_2...$ where $\vec{v}_i$ is a finite sequence of elements of $Y_1$ evaluating to $a_1$ for $i=0$ and $e_1$ for $i>0$. We can then define $\vec{u}$ to be in $\Omega$ if and only if the system depicted on the right of Figure 4 evaluates to an element of $P$.

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

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

Finally, the transition table $\Delta$ is given by $\Delta_0(a) = \{\text{eval}(a)\}$ for all $a \in \Sigma_0$, and for all $n \in \mathbb{N}$ and $a \in \Sigma_n$, we have

$$
\Delta_+(a) = \{(b_1, \dots, b_n) \in (Y_1)^n \mid \bigcap_{i=1}^n b_i(x_i) \subseteq a\}.
$$

Intuitively, this means that choosing a run will amount to choosing a deterministic below
$a$ for each node labelled $a$.

We have to show that a regular-tree is accepted by $\mathcal{B}$ if and only if it belongs to $L$

**► Lemma 94.** If a $\Sigma$-labelled regular-tree $r$ is accepted by $\mathcal{B}$, then $r$ belongs to $L$.

**Proof.** Let $r$ be a regular-tree accepted by $\mathcal{B}$, i.e. the infinite tree $T_r$ is accepted by $\mathcal{B}$. Since $T_r$ is a regular tree, we can choose a regular accepting run $\rho$ of $\mathcal{B}$ on $T_r$. We view here $\rho$ as a labelling of the nodes of $T_r$ by transitions in $Y_1^+$ (for internal nodes) or $Y_0$ (for leaves). Let $T_\rho$ be the regular tree obtained by replacing for each node $d$ its labelling $a$ by $(a, \rho(d))$. We can fold the tree $T_\rho$ into a finite transition system $S$.

Let $\pi : Y_1^+ \to \text{Det}(\mathcal{Y})$ mapping $\vec{b}$ to $\bigcap_{i=1}^n b_i(x_i)$, and $\pi(a_0) = a_0$ if $a_0 \in Y_0$. Let $\pi(S)$ be the $\mathcal{Y}$-system obtained from $S$ by replacing each label $(a, \vec{b})$ of $S$ by $\pi(\vec{b})$.

We claim that $\pi(S)$ is accepted by the algebra $(\mathcal{Y}, \text{eval}, P)$. This amounts to show that all yields of $\pi(S)$ are in $P$. Yields of $\pi(S)$ directly correspond to branches of $T_r$, labelled by the elements $b_i$ chosen in the run $\rho$. Since $\rho$ is an accepting run, all such branches are in $\Omega$, which is defined to be the set of elements of $Y_1^\omega$ and $Y_1^*Y_0$ evaluating to an element in $P$. Therefore, $\pi(S)$ is indeed accepted by the algebra $\mathcal{Y}$. Finally, for each $a \in \Sigma$ and $\vec{b} \in \Delta(a)$, we have $\pi(\vec{b}) \subseteq \text{eval}(a)$. This implies that the $\Sigma$-system $s$ obtained by projecting each label $(a, \vec{b})$ of $S$ onto their first component $a$ is accepted by $(\mathcal{Y}, \text{eval}, P)$, since $\text{eval}(\pi(S)) \subseteq \text{eval}(s)$
and eval($\pi(S)$) ∈ P. By Lemma 69, since s is a Σ-system, this means that s ∈ L. Moreover, s is in the unfold-equivalence class of r, since it has been obtained by unfolding r into an infinite tree T<sub>r</sub> then folding T<sub>r</sub> into the finite system s. Since L is unfold-equivalent, we can conclude that the regular-tree r is in L.

► **Lemma 95.** If a Σ-labelled regular-tree r belongs to L, then it is accepted by B.

**Proof.** Let $r$ be a regular-tree in $L$, and $s$ a $\Sigma$-system in the unfold-equivalence class of $r$. Given a node $v$ of $s$ labelled with $a \in \Sigma$, we can use Lemma 81 to choose a deterministic element $\delta = a_0 \sqcap \sqcup_{i=1}^n b_i(x_i)$ such that $\delta \subseteq a$ (so $\delta \in \Delta(a)$), and that preserves acceptance in the context of $s$. Proceeding iteratively, we build a system $s'$ by labelling $s$ with elements according to $\Delta$, such that, in the previous notations, $\pi(S)$ is accepted by the algebra. As before, this means that all branches of $\pi(S)$ are accepted, which means that unfolding $s$ into an infinite tree gives an accepting run of $B$ on $T_r$. We can conclude that $r$ is accepted by $B$.

## 6.4 The bisimulation-invariant case

Let us now treat the case where the language of regular-trees $L$ is not only unfold-invariant, but also bisimulation-invariant. We will show that in this case, we can obtain a $\mu$-calculus formula for $L$. Recall that in this setting, for each P-valuation $\nu: P \to 2$, and $n \in \mathbb{N}$, there is a symbol $\nu_n \in \text{Tr}$. We take as alphabet $\Sigma = \text{Tr}$.

By Theorem 93, we obtain an unfold-automaton $\mathcal{B}$ recognising the language $L$ of regular-trees. Let us build an automaton $\mathcal{B}'$ based on $\mathcal{B}$, making explicit the bisimulation invariance in the transition table. The components $X, \Sigma, \Omega$ of $\mathcal{B}'$ are the same as those of $\mathcal{B}$, and its transition table $\Delta'$ is defined from the table $\Delta$ of $\mathcal{B}$ as follows:

- for all $a \in \Sigma_0$, we have $\Delta'_0(a) = \Delta_0(a)$,

- for all $n > 0$ and $\nu_n \in \Sigma$, we define

$$ \Delta'_{+}(\nu_n) = \{(b'_1, \dots, b'_n) \in Y_1^n \mid \begin{array}{l} \exists m \le n, (b_1, \dots, b_m) \in \Delta(\nu_m), \\ \exists \sigma \text{ surjection } [n] \to [m] \text{ such that } \forall i \in [n], b'_i = b_{\sigma(i)} \end{array} \} $$

Intuitively, this means that $\mathcal{B}'$ behaves on a tree $r'$ similarly as $\mathcal{B}$ would behave on a tree $r$, where $r'$ is obtained from $r$ by reordering and duplicating children. Since these operations preserve the bisimilarity class, such a tree $r'$ belongs to $L$ if and only if $r$ does.

► **Lemma 96.** The automaton $\mathcal{B}'$ recognises the bisimulation-invariant language $L$.

**Proof.** Let $r'$ be a regular-tree accepted by $\mathcal{B}'$, via a run $\rho'$. We build a tree $r \in L$ that is bisimilar to $r'$, by induction on the structure of $r'$. We will also build a function $f$ from the nodes of $r$ to the nodes of $r'$, witnessing the bisimulation between $r$ and $r'$. We describe here the construction of $r$ and $f$ for the root of $r'$, starting at the root $v'$ of $r'$:

1. Create a node $v = f(v')$ as the root of $r$.

2. Let $\nu_n$ be the label of $v'$ in $r'$.

3. If $n = 0$, define the label of $v$ in $r$ to be $\nu_0$ and $\rho(v) = \rho'(v')$, and stop.

4. Otherwise, by definition of $\Delta'$, there exists $m \le n$, $(b_1, \dots, b_m) \in \Delta(\nu_m)$, and a surjection $\sigma: [n] \to [m]$ such that for all $i \in [n]$, $\rho'(v)_i = b'_{\sigma(i)}$. Define $\rho(v) = (b_1, \dots, b_m)$.

5. Define the label of $v$ to be $\nu_m$.

6. Define the children of $v$ to be $v_1, \dots, v_m$, and for each $i \in [n]$, $f(v'_i) = v_{\sigma(i)}$.

7. For each $i \in [m]$, go to step 2 with $v'_i$ and $fv_i$ playing the role of $v'$ and $v$.
XX:42 Tree algebras and bisimulation-invariant MSO on finite graphs

The tree $r$ is thus built, together with the function $f$ from $r$ to $r'$ and run $\rho$ on $r'$. The function $f$ witnesses the bisimulation between $r$ and $r'$. Recall that $\nu_n$ and $\nu_m$ define the same set of predicates and are therefore considered identical from the point of view of the bisimulation relation. Moreover, any branch of $\rho$ is a branch of $\rho'$, so the run $\rho$ is accepting. We obtain that $r \in L$, so by bisimulation-invariance of $L$, $r' \in L$.

Conversely, let $r$ be a regular-tree in $L$, witnessed by an accepting run $\rho$ of $B$. Using the identity function for $\sigma$ on every node, we directly obtain that $\rho$ is also an accepting run of $B'$ on $r$, so $r$ is accepted by $B'$.

Moreover, the automaton $B'$ can be turned into an automaton of the form described in [14, Thm 7]. The transition table $\Delta'$ of $B'$ is such that for all valuation $\nu: P \to 2$, the set of transitions from a node labelled $\nu$ only imposes a certain set of unary transitions to be taken at least once, among a certain set of possible unary transitions. Up to encoding choices, this corresponds to the constraint given in [14, Thm 7]. Indeed, up to the incorporation of states $Q$ and labels $\Sigma_r$ in the elements $b_i$, and in the acceptance condition $\Omega$, we can express the automaton $B'$ as an instance of [14, Thm 7] in the following way:

$$ \delta(\nu) = \bigvee_{\substack{m \le n, \\ (b_1, \dots, b_m) \in \Delta(\nu_m)}} \exists x_1, \dots, x_m. (b_1(x_1) \wedge \dots \wedge b_m(x_m) \wedge \forall z. (b_1(z) \vee \dots \vee b_m(z))). $$

Thus, by [14, Thm 7], the automaton $B'$ can be turned into an equivalent $\mu$-calculus formula. We can finally conclude with the following theorem:

**Theorem 97.** Let $L$ be a bisimulation-invariant language of regular-trees recognised by a rankwise finite algebra. Then $L$ can be recognised by a $\mu$-calculus formula.

## Comments on effectivity

The well-known upward direction of Theorem 1, and Theorem 2, which consists in translating a $\mu$-calculus sentence into an equivalent MSO-sentence is purely syntactic, and effective.

For the other direction, let us first note that, given an MSO-sentence, it is undecidable whether it is bisimulation-invariant (over all transition systems, or over finite transition systems), as observed in [9] already for First-Order Logic.

Consequently, the algorithm that we provide has the following characteristics:

**Input** An MSO-sentence $\Phi$.

**Output** A $\mu$-calculus sentence $\Psi$ such that, if $\Phi$ is bisimulation-invariant over finite transition systems, then $\Psi$ and $\Phi$ coincide on all finite transition systems.

**Proof (Sketch).** Let $\Phi$ be the input MSO formula. Let $d$ be the quantifier depth of $\Phi$. Let us assume $\Phi$ to be bisimulation-invariant over finite transition systems. Then the property it defines is recognised by a rankwise finite algebra by Lemma 91. But our proof gives slightly more: there exists an effective bound $N(d)$ on the size of sort $X$ for all $X$, and in particular for sorts 0 and 1. As a consequence, there exists an effective bound $N'(d)$ on the size of a $\mu$-calculus formula for the property. Pushing further, it follows that there exists an effective bound $N''(d)$ such that two $\mu$-calculus sentences of size at most $N'(d)$ are equivalent if and only if they are equivalent over all transition systems of size at most $N''(d)$. Hence, a possible algorithm is as follows: try all $\mu$-calculus sentences of size at most $N'(d)$, and for each of them, check whether it is equivalent to $\Phi$ on all transition systems of size at most $N''(d)$. If yes, choose $\Psi$ to be this $\mu$-calculus sentence. If no such $\mu$-calculus sentence is discovered, output any sentence. The validity of this approach is straightforward.
# 7 Conclusion

Our notion of systems is equivalent to notions of tree algebras developed elsewhere in the literature. The notion of set-systems is a kind of extended powerset construction on it, expanded with root vertices, something that is new to the best of our knowledge, though close to more classical powerset constructions. One originality here is mainly that all operations are performed while keeping the structures folded, and only finitely unfolding it when necessary. More crucial is the argument that transforms algebras to yield-algebras, which circumvent the impossibility to have the powerset distribute over the monad of an algebraic theory that has non-linear identities. We are studying further this categorical aspect. Another interesting direction is to see to which extent an algebraic approach can be used to bypass automata for deciding the MSO-theory of infinite trees, ie a purely algebraic proof or Rabin's theorem.

**Acknowledgements.** We thank Achim Blumensath for helpful discussions, proofreading this work, and finding a major mistake in a previous version of this paper (now solved).

## References

1. Peter Aczel, Jiří Adámek, and Jiří Velebil. A coalgebraic view of infinite trees and iteration. *Electronic Notes in Theoretical Computer Science*, 44(1):1–26, 2001. CMCS 2001, Coalgebraic Methods in Computer Science (a Satellite Event of ETAPS 2001). doi:https://doi.org/10.1016/S1571-0661(04)80900-9.

2. Achim Blumensath. Recognisability for algebras of infinite trees. *Theor. Comput. Sci.*, 412(29):3463-3486, 2011. doi:10.1016/J.TCS.2011.02.037.

3. Achim Blumensath. An algebraic proof of rabin's tree theorem. *Theor. Comput. Sci.*, 478:1–21, 2013. doi:10.1016/J.TCS.2013.01.026.

4. Achim Blumensath. The Power-Set Construction for Tree Algebras. *Logical Methods in Computer Science*, Volume 19, Issue 4, November 2023. URL: https://lmcs.episciences.org/12507, doi:10.46298/lmcs-19(4:9)2023.

5. Achim Blumensath and Felix Wolf. Bisimulation invariant monadic-second order logic in the finite. *Theoretical Computer Science*, 823:26–43, 2020. doi:https://doi.org/10.1016/j.tcs.2020.03.001.

6. Mikolaj Bojanczyk and Tomasz Idziaszek. Algebra for infinite forests with an application to the temporal logic EF. In Mario Bravetti and Gianluigi Zavattaro, editors, *CONCUR 2009 - Concurrency Theory, 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings*, volume 5710 of *Lecture Notes in Computer Science*, pages 131–145. Springer, 2009.

7. Mikolaj Bojanczyk and Igor Walukiewicz. Forest algebras. In Jörg Flum, Erich Grädel, and Thomas Wilke, editors, *Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas]*, volume 2 of *Texts in Logic and Games*, pages 107–132. Amsterdam University Press, 2008.

8. Mikołaj Bojańczyk and Bartek Klin. A non-regular language of infinite trees that is recognizable by a sort-wise finite algebra. *Logical Methods in Computer Science*, Volume 15, Issue 4, November 2019. URL: https://lmcs.episciences.org/5927, doi:10.23638/LMCS-15(4:11) 2019.

9. Ivano Ciardelli and Martin Otto. Inquisitive bisimulation. *The Journal of Symbolic Logic*, 86(1):77–109, October 2020. URL: http://dx.doi.org/10.1017/jsl.2020.77, doi:10.1017/jsl.2020.77.

10. Anuj Dawar and Martin Otto. Modal characterisation theorems over special classes of frames. *Ann. Pure Appl. Log.*, 161(1):1–42, 2009. doi:10.1016/J.APAL.2009.04.002.

11. S. Feferman and R. Vaught. The first order properties of products of algebraic systems. *Fundamenta Mathematicae*, 47(1):57–103, 1959. URL: http://eudml.org/doc/213526.
12 Helle Hvid Hansen, Clemens Kupke, and Eric Pacuit. Neighbourhood structures: Bisimilarity and basic model theory. *Log. Methods Comput. Sci.*, 5(2), 2009.

13 Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In J. W. de Bakker and Jan van Leeuwen, editors, *Automata, Languages and Programming, 7th Colloquium, Noordweijkerhout, The Netherlands, July 14-18, 1980, Proceedings*, volume 85 of *Lecture Notes in Computer Science*, pages 299-309. Springer, 1980.
doi:10.1007/3-540-10003-2\_79.

14 David Janin and Igor Walukiewicz. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In Ugo Montanari and Vladimiro Sassone, editors, *CONCUR '96, Concurrency Theory, 7th International Conference, Pisa, Italy, August 26-29, 1996, Proceedings*, volume 1119 of *Lecture Notes in Computer Science*, pages 263-277. Springer, 1996.
doi:10.1007/3-540-61604-7\_60.

15 Damian Niwiński. Fixed point characterization of infinite behavior of finite-state systems. *Theoretical Computer Science*, 189(1):1-69, 1997.
doi:https://doi.org/10.1016/S0304-3975(97)00039-X.

16 Maximilian Pflueger, Johannes Marti, and Egor V. Kostylev. A characterisation theorem for two-way bisimulation-invariant monadic least fixpoint logic over finite structures. In *Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024*, pages 63:1-63:14. ACM, 2024.
doi:10.1145/3661814.3662107.

17 Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. *Bulletin of the American Mathematical Society*, 74(5):1025-1029, 1968.

18 Alexander Rabinovich. On compositionality and its limitations. *ACM Trans. Comput. Log.*, 8(1):4, 2007.
doi:10.1145/1182613.1182617.

19 Eric Rosen. Modal logic over finite structures. *J. Log. Lang. Inf.*, 6(4):427-439, 1997.
doi:10.1023/A:1008275906015.

20 Saharon Shelah. The monadic theory of order. *Annals of Mathematics*, 102(3):379-419, 1975.

21 Wolfgang Thomas. Languages, automata, and logic. In Grzegorz Rozenberg and Arto Salomaa, editors, *Handbook of Formal Languages, Volume 3: Beyond Words*, pages 389-455. Springer, 1997.
doi:10.1007/978-3-642-59126-6\_7.

22 Johan Van Benthem. Correspondence theory. In D. Gabbay and F. Guenthner, editors, *Handbook of Philosophical Logic: Volume II: Extensions of Classical Logic*, pages 167-247. Springer Netherlands, Dordrecht, 1984.
doi:10.1007/978-94-009-6259-0\_4.

23 Thomas Wilke. Algebras for classifying regular tree languages and an application to frontier testability. In Andrzej Lingas, Rolf Karlsson, and Svante Carlsson, editors, *Automata, Languages and Programming*, pages 347-358, Berlin, Heidelberg, 1993. Springer Berlin Heidelberg.