Tree algebras and bisimulation-invariant MSO on finite graphs

Thomas Colcombet, Amina Doumane, Denis Kuperberg

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 questi…