@article{Janin_Lenzi_2012, title={On the logical definability of topologically closed recognizable languages of infinite trees}, volume={21}, url={https://www.cai.sk/ojs/index.php/cai/article/view/495}, abstractNote={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.<br />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.}, number={3}, journal={COMPUTING AND INFORMATICS}, author={Janin, David and Lenzi, Giacomo}, year={2012}, month={Feb.}, pages={185–203} }