Tree Algebras and Bisimulation-Invariant MSO on Finite Graphs

We present here a high-level overview of the sequence of arguments used in our proof, putting an emphasis on lemmas that involve entirely new arguments. Due to lack of space, only subsets of these arguments will be covered in this extended abstract.

We roughly decompose the arguments in three main parts: from MSO to algebras, from algebras to yield-algebras, and from yield-algebras to $\mu$-calculus.

A >ranked set $\mathrm{\Sigma }$ (or >alphabet) is a family of sets ${\mathrm{\Sigma }}_n$ indexed by natural numbers. We write $a\in \mathrm{\Sigma }$ for $a\in {\mathrm{\Sigma }}_n$ for some $n$. For $a\in \mathrm{\Sigma }$, the >rank of $\mathrm{\Sigma }$, noted $\mathrm{rk}(a)$, is the integer $n$ such that $a\in {\mathrm{\Sigma }}_n$. A >map of ranked sets $f$ from $\mathrm{\Sigma }$ to $\mathrm{\Gamma }$ is a map that preserves the ranks, i.e. a family of maps $f_n:{\mathrm{\Sigma }}_n\to {\mathrm{\Gamma }}_n$ for all  $n\in \mathbb{N}$. A ranked set $\mathrm{\Sigma }$ is >rankwise-finite if ${\mathrm{\Sigma }}_n$ is finite for all $n$. Note that ranked sets equipped with their maps form a category, that we call the >category of ranked sets. We fix an infinite set $\mathrm{Vars}=\{x_1,x_2,\mathrm{\dots }\}$ of >variables. Variables can be seen as having rank $0$. For $n\in \mathbb{N}$, we denote with $[n]$ the set $\{1,\mathrm{\dots },n\}$, and $\mathrm{Vars}[n]$ the variables $\{x_1,\mathrm{\dots },x_n\}$.

Let us define now the notions of set-systems and systems, illustrated on Figure 1.

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

We describe in this section the operations used for composing set-systems (or systems), allowing to build complex ones out of simpler elements. We do it using the categorical approach of monads: the idea is to have a single complex operation of composition, called $\mathrm{flatten}$, that can then be specialized into simpler ones.

The operation $\mathrm{flatten}$, takes a set-system of set-systems as input, and produces a set-system as output. We explain it here through an example: the following picture shows a set-system of set-systems and its >flattening. The subsystems are drawn inside the dashed boxes, and boxes are organised themselves as a set-system structure that we call the pattern²²2Note that the definition enforces that the rank of subsystems (i.e. the number of variables they use) should be consistent with the number of outgoing directions of the vertex in 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 $\mathrm{rk}(\mathrm{𝑙𝑎𝑏𝑒𝑙}(v))$ for the bottommost.

As is shown, the $\mathrm{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 differently: the root vertices from subsystems remain root vertices during the process, while initial vertices of subsystems that are root get promoted to roots.

Note that the $\mathrm{flatten}$ operation, when given a system of systems as input, produces a system. Hence, the same operation shall be used for composing systems or set-systems depending on the context. In a categorical description, $\mathrm{flatten}$, together with the corresponding operation $\mathrm{unit}$ (that turns a single symbol into a one-vertex system), equips the set-system definition (resp. system definition) with a monad structure.

A special form of composition, which is derived from $\mathrm{flatten}$ is the notion of set-context, which are set-systems with a hole that can be filled.

A $\mathrm{\Sigma }$-set-context with a $k$-hole is a $(\mathrm{\Sigma }\uplus \{{\square }_k\})$-set-system, in which ${\square }_k$ is a new symbol of rank $k$, called the >hole symbol, and which labels exactly one vertex, called the >hole vertex. Set-contexts are denoted $C[{\square }_k]$, $D[{\square }_k]$, … A set-context is >closed if it is of rank $0$. Given a $\mathrm{\Sigma }$-set-context $C[{\square }_k]$ and a $\mathrm{\Sigma }$-set-system $S$ of rank $k$, $C[S]$ denotes the $\mathrm{\Sigma }$-set-system obtained by substituting $S$ for the hole. A >context is a set-context which is a system.

An example of a closed context $C[{\square }_2]$, a system $S$ of rank $2$, and the result $C[S]$ are pictured below. The hole vertex is depicted as an empty box.

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

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 $\mathrm{flatten}$ or [set-]contexts. In many situations, this is just a choice of presentation.

So far, we have seen systems and set-systems as “rigid structures”. The notions of morphisms allows us to compare them in more subtle ways.

Set-systems come with a natural definition of morphisms: a >morphism of set-systems from $S$ to $S^{\prime }$, set-systems of same rank, is a map from vertices of $S$ to vertices of $S^{\prime }$ that preserves initial vertices, root vertices and edges.

If we specialise morphisms to $\mathrm{\Sigma }$-systems we obtain the notions of unfolding, unfold-equivalence and regular-trees:

For instance, in the pictures below, the systems $S_1$ and $S_2$ have both $U$ as unfolding, and thus are unfold-equivalent. The system $F$ is a folding of both $S_1$ and $S_2$:

At this point, one can prove that unfold-equivalence interacts nicely with $\mathrm{flatten}$:

From a categorical point of view, this means that systems modulo unfold-equivalence, i.e. regular-trees, equipped with the $\mathrm{flatten}$ and $\mathrm{unit}$ operations form a monad.

In this section, we recall what is the standard definition of a transition system, and we explain how these can be seen as systems as defined above. We also explain how bisimilarity can be phrased in this setting.

A >transition system $(V,i,T,\gamma )$ consists of a finite⁴⁴4In this work, as for systems, transition systems are 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^{𝙿}$. We now explain how to encode transition systems as systems over a specific ranked alphabet $\mathrm{𝐓𝐫}$.

Let $\mathrm{𝐓𝐫}$ be the ranked alphabet which has an element ${\nu }_n$ of rank $n$ for all $𝙿$-valuation $\nu \in 2^{𝙿}$, and all $n\in \mathbb{N}$. Given a closed $\mathrm{𝐓𝐫}$-system $S$, call its >decoding the transition system $\mathrm{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 $\mathrm{decode}(S)$. Note that the decoding is unique, while several non-isomorphic $\mathrm{𝐓𝐫}$-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).

We define the >bisimilarity relation over closed $\mathrm{𝐓𝐫}$-systems as the least equivalence relation that contains unfold-equivalence and the relation “encoding the same transition system”.

The following lemma states why this is consistent with the standard terminology.

From now on, we shall only consider transition systems through this encoding as $\mathrm{𝐓𝐫}$-systems.

The following definitions follow the standard approach via monads.

Call >language of $\mathrm{\Sigma }$-systems a set of closed $\mathrm{\Sigma }$-systems. A >language of $\mathrm{\Sigma }$-regular-trees is a language of $\mathrm{\Sigma }$-systems $L$ which is invariant under unfold-equivalence, i.e. such that if $T,T^{\prime }$ are unfold-equivalent and $T\in L$, then $T^{\prime }\in L$, for all $\mathrm{\Sigma }$-systems $T,T^{\prime }$.

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

We say that $L$ is recognised by $𝒜$ if it is recognised by $(𝒜,\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, i.e. algebras $𝒜=(A,\mathrm{eval})$ such that $A_n$ is finite for all $n\in \mathbb{N}$.

Note, as expected, that the language of systems recognised by regular-tree algebras are languages of regular-trees.

We have seen in Section 2.5 how to see transition systems as $\mathrm{𝐓𝐫}$-systems. Let us explain now how logic interacts with this view. We assume the reader familiar with >monadic second-order logic (>MSO for short). The signature here is the one of transition systems (one binary relation, unary relations for each predicate, and an initial constant). We shall say that an MSO-sentence $\psi$ is >bisimulation-invariant if for all bisimilar transition systems $S,S^{\prime }$, we have $S\vDash \psi$ if and only if $S^{\prime }\vDash \psi$.

Using the “composition method” approach, we get the translation from logic to algebra:

We shall now see how set-systems can be understood as “finite-non-deterministic machines that would non-deterministically produce systems”. This is the notion of yields, that come in two variants: init and root-yields.

We introduce the notion through an example. A set-system is pictured below, as well as one of its init-yields and one of its root-yields.

Informally, an >init-yield of a set-system $S$ is a system $T$ that unfolds to a system that can be obtained starting from some initial vertex of $S$ by resolving all the non-deterministic choices, potentially partially unravelling the set-system at the same time. A >root-yield is similar, starting from a root vertex instead of an initial vertex. Note that the definition is such that the set of init-yields (resp. root-yields) of a set-system are closed under unfold-equivalence. The real definition makes use of morphisms of set-systems. We set:

Two set-systems $S,S^{\prime }$ of same rank are >yield-equivalent if $\mathrm{InitYields}(S)=\mathrm{InitYields}(S^{\prime })$ and $\mathrm{RootYields}(S)=\mathrm{RootYields}(S^{\prime })$.

Note that if $S$ is a system, then an init-yield of $S$ is nothing but an unfold-equivalent system, and there is no root-yield. As a consequence yield-equivalence coincides with unfold-equivalence over systems.

From now, for simplification of the presentation, we shall do as if only init-yields existed.

This section illustrates a difficulty arising from working with yields, and briefly describes the tool of resolution that we use to circumvent it in the complete version of this work.

At a high level, we would like, given a set-context $C[{\square }_n]$, to write the yields of $C[S]$ for some set-system $S$ of rank $n$ as a “composition” of the yields of $S$. The following example shows that it does not work.

This situation is in fact a well-identified mathematical difficulty. For instance, this is what prevents the existence of a distributive law with the powerset monad over the monads of non-linear trees [4].

To circumvent this problem, we introduce the notion of >resolution, which combines the yield with some variable renaming.

In Example 13, 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 the information that could not be caught by yields.

Now, it makes sense to understand a yield of $C[S]$ as a combination of resolutions of $C$ and $S$. This notion of resolution is one of the arguments used for showing that yield-equivalence is a congruence:

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-algebras are naturally endowed with an order $⊑$ that provides an inf-semi-lattice structure (note that the non-deterministic sum will be noted $\sqcap$, i.e. as an infimum rather than a supremum; this is a choice of presentation that corresponds to the fact that we see in this work this non-determinism as “adversarial”, i.e. controlled by an opponent).

Note that since systems are particular cases of set-systems, yield-algebras are in particular algebras. Furthermore, since yield-equivalence coincides with unfold-equivalence over systems, 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. This means that we can use yield-algebras for recognising languages of regular-trees:

The following lemma shows the intention behind the definition.

One can now state the key lemma of this section (which involves new arguments compared to the literature).

For other kind of algebras, such as monoids, deterministic automata over words or trees, forest algebras, …, a similar result is classically obtained by applying a form of powerset construction. Let us explain by an example why this standard approach fails here.

Our argument for avoiding the problem and proving Lemma 20 involves two ideas. Let $𝒜$ be a rankwise-finite regular-tree algebra recognising a language of regular-trees $L$.