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

Abstract

We consider monadic second order logic (MSO) and the propositional μ-calculus (Lμ) over transition systems. 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 [JW96]. The main step is the development of automata-based characterizations of Lμ over arbitrary transition systems and of MSO over transition trees. 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. Further 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. We start with a section introducing the notions of transition systems and transition trees, bisimulations and the ω-unravelling. In Section 3 we repeat the definitions of MSO and Lμ. In Section 4 we develop a general notion of automaton and acceptance conditions in terms of games to obtain the characterizations of the two logics. In the last section we will prove the main result mentioned above.