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代数转换为无限词上ω-半群的关键理论在树结构上的弱化形式，也是二十年来无限树正则语言代数理论中缺失的一环。