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 Buchi 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 Sigma(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 mucalculus: it shows that the bisimulation invariant fragment of the monadic Sigma(2) level equals the vmu-level of the mu-calculus hierarchy.
On the relationship between monadic and weak monadic second order on arbitrary trees, with application to the mu-calculus
LENZI, Giacomo;
2004
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 Buchi 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 Sigma(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 mucalculus: it shows that the bisimulation invariant fragment of the monadic Sigma(2) level equals the vmu-level of the mu-calculus hierarchy.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
