2026-08-16T08:03:20Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23529 2025-10-08T13:13:20Z ddc:004 open_access

Tree Algebras and Bisimulation-Invariant MSO on Finite Graphs Colcombet, Thomas Doumane, Amina Kuperberg, Denis MSO mu-calculus finite graphs bisimulation tree algebra 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. 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Thomas Colcombet and Amina Doumane and Denis Kuperberg 2025 Is Part Of LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2025.152 urn:nbn:de:0030-drops-235294 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.152 eng https://creativecommons.org/licenses/by/4.0/legalcode