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.