On the logical definability of topologically closed recognizable languages of infinite trees
David Janin ; Giacomo Lenzi
Computing and Informatics, Tome 28 (2012) no. 1, / Harvested from Computing and Informatics
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.
Publié le : 2012-01-26
Classification: 
@article{cai495,
     author = {David Janin and Giacomo Lenzi},
     title = {On the logical definability of topologically closed recognizable languages of infinite trees},
     journal = {Computing and Informatics},
     volume = {28},
     number = {1},
     year = {2012},
     language = {en},
     url = {http://dml.mathdoc.fr/item/cai495}
}
David Janin; Giacomo Lenzi. On the logical definability of topologically closed recognizable languages of infinite trees. Computing and Informatics, Tome 28 (2012) no. 1, . http://gdmltest.u-ga.fr/item/cai495/