Tree algebras and bisimulation-invariant MSO on finite graphs

TL;DR

This work settles a long-standing question by proving that over finite transition systems the bisimulation-invariant fragment of MSO coincides with the $\mu$-calculus. It develops an algebraic framework based on yield-algebras and a compositional method that reduces MSO-definable languages to rankwise finite algebras and regular-tree automata. Key components include the automaton property for syntactic yield-algebras, a robust notion of unfoldings and regular trees, and a translation from algebraic recognisers to unfold-automata, which then yields a $\mu$-calculus representation for bisimulation-invariant MSO. The results generalize the Janin–Walukiewicz correspondence to finite graphs, provide effective translations and discuss recognition closure properties, with implications for verification and model checking on finite structures. The paper also clarifies the interplay between tree algebras, the composition method, and automata-theoretic techniques in a finite setting.

Abstract

We establish that the bisimulation invariant fragment of MSO over finite transition systems is expressively equivalent over finite transition systems to modal mu-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 recognized by finitary tree algebras whose sorts zero and one are finite are the regular ones, ie. the ones expressible in mu-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.

Figures (4)

• Figure 1: A "$\alphabet$-set-system" $S_1$ and a "$\alphabet$-system" $S_2$, both over "variables" $\{x_1,x_2\}$ (ie of rank $2$), for $\alphabet$ 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 $\initcircle$ denotes an "initial vertex", the symbol $\mass$ denotes a "root vertex", and $\meetsquare$ emphasizes the presence of multiple successors in the same direction. Implicitly, edges are directed from left to right unless explicitly using an arrow notation.
• Figure 2: $S_1$ and $S_2$ are "unfold-equivalent", $F$ is a common "folding" of both, and $U$ a common "unfolding" of both.
• Figure 3: Plugging $S$ in the $2$-context $C[\hole_2]$
• Figure 4: Left: Evaluating $a_1b_1c_1d_0$ of $Y_1^*Y_0$Right: Evaluating $a_1e_1^\omega$ of $Y_1^\omega$

Theorems & Definitions (97)

• Theorem 1: JaninW96
• Theorem 2
• Remark 3
• Definition 4: set-systems
• Definition 5: systems
• Remark 6: the nature of set-systems
• Remark 7: category of set-systems and systems
• Definition 8
• Lemma 9: composition
• Remark 10