On the Rlationship Between Monadic and Weak Monadic Second Order Logic on Arbitrary Trees, with Applications to the mu-Calculus

Article type: Research Article

Authors: Janin, David | Lenzi, Giacomo

Affiliations: LaBRI, Université de Bordeaux I, 351, cours de la libération, F-33 405, Talence cedex, France | Dipartimento di Matematica Università di Pisa via Buonarroti 2, I-56127 Pisa, Italy

Abstract: In 1970 [26], in Weakly definable relations and special automata, Math. Log. and Found. of Set Theory, pp 1-23, Rabin shows that a language is recognizable by a tree automaton with Büchi like infinitary condition if and only if it is definable as the projection of a weakly definable language. In this paper, we refine this result characterizing such languages as those definable in the monadic Σ2 level of the quantifier alternation depth hierarchy of monadic second order logic (MSO). This new result also contributes to a better understanding of the relationship between the quantifier alternation depth of hierarchy of MSO and the fixpoint alternation depth hierarchy of the mu-calculus: it shows that the bisimulation invariant fragment of the monadic Σ2 level equals the νμ-level of the mu-calculus hierarchy.

Journal: Fundamenta Informaticae, vol. 61, no. 3-4, pp. 247-265, 2004