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 since twenty years.

翻译：我们证明了在有限转移系统上，MSO的互模拟不变片段在表达能力上等价于模态μ-演算，这一开放问题已存在数十年。证明通过将问题转化到代数框架，并证明由零阶和一阶均为有限的有限树代数所识别的正则树语言正是正则语言，即那些可用μ-演算表达的语言。这对应于树上Wilke代数到无限字上ω-半群关键转换的弱形式，也是二十年来无限树正则语言代数理论中缺失的一环。