Expressive Power of Monadic Second-Order Logic and Modal μ-Calculus

Abstract

We consider monadic second order logic (MSO) and the modal μ-calculus (L_μ) over transition systems (Kripke structures). It is well known that every class of transition systems which is definable by a sentence of L_μ is definable by a sentence of MSO as well. It will be shown that the converse is also true for an important fragment of MSO: every class of transition systems which is MSO-definable and which is closed under bisimulation - i.e., the sentence does not distinguish between bisimilar models - is also L_μ-definable. Hence we obtain the following expressive completeness result: the bisimulation invariant fragment of MSO and L_μ are equivalent. The result was proved by David Janin and Igor Walukiewicz. Our presentation is based on their article [91]. The main step is the development of automata-based characterizations of L_μ over arbitrary transition systems and of MSO over transition trees (see also Chapter 16). It turns out that there is a general notion of automaton subsuming both characterizations, so we obtain a common ground to compare these two logics. Moreover we need the notion of the ω-unravelling for a transition system, on the one hand to obtain a bisimilar transition tree and on the other hand to increase the possibilities of choosing successors.