On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic

Abstract

Monadic second order logic (MSOL) over transition systems is considered. It is shown that every formula of MSOL which does not distinguish between bisimilar models is equivalent to a formula of the propositional µ-calculus. This expressive completeness result implies that every logic over transition systems invariant under bisimulation and translatable into MSOL can be also translated into the µ-calculus. This gives a precise meaning to the statement that most propositional logics of programs can be translated into the µ-calculus.