A characterization of Buchi tree automata

摘要

We show that a language of infinite binary trees is definably by a ∑_2-formula of the monadic second order logic of two successor (with no additional symbols) iff it can be accepted by a Buchi automaton. The same result has been obtained by G. Lenzi, but our proof is simpler.