TY - JOUR AU - Janin, David AU - Lenzi, Giacomo PY - 2012/02/21 Y2 - 2024/03/29 TI - On the logical definability of topologically closed recognizable languages of infinite trees JF - COMPUTING AND INFORMATICS JA - Comput. Inform. VL - 21 IS - 3 SE - Articles DO - UR - https://www.cai.sk/ojs/index.php/cai/article/view/495 SP - 185-203 AB - 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. ER -