On the Rlationship Between Monadic and Weak Monadic Second Order Logic on Arbitrary Trees, with Applications to the mu-Calculus
David Janin, Giacomo Lenzi · Fundamenta Informaticae · 2004
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.