On the logical definability of topologically closed recognizable languages of infinite trees

Abstract In this paper, we prove that for any language L of finitely branching finite and infinite trees, the following properties are equivalent: (1) L is definable by an existential MSO sentence which is bisimulation invariant over graphs, (2) L is definable by a FO-closed existential MSO sentence which is bisimulation invariant over graphs, (3) L is definable in the nu-level of the modal mu-calculus, (4) L is the projection of a locally testable tree language and is bisimulation closed, (5) L is closed in the prefix topology and recognizable by a modal finite tree automaton, (6) L is recognizable by a modal finite tree automaton of index zero. The equivalence between (3), (4), (5) and (6) is known for quite a long, time, although maybe not in such a form, and can be considered as a classical result. The logical characterization of this class of languages given by (1) (and (2)) is new. It. is an extension of analogous results over finite structures such as words, trees and grids relating full existential MSO and definability by finite automata.