Tree algebras and bisimulation-invariant MSO on finite graphs
Tree algebras and bisimulation-invariant MSO on finite graphs
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 …