Tree automata with constraints on infinite trees

Tree automata on infinite trees are a powerful tool that is widely used for decision procedures and synthesis of logical specifications. It is well known that finite tree automata have good algorithmic properties, but somewhat limited expressive power. For example, they cannot verify that certain subtrees of an input tree are equal. In order to model such properties, we study extensions of tree automata that use so called constraints to compare whole subtrees of an input. We distinguish between two types of constraints: local constraints and global constraints. Tree automata with local constraints were introduced in the 90s by Bogaert and Tison, who analyzed a model of tree automata on finite ranked trees that use guard terms in the transitions in order to compare sibling subtrees at each node. Recently Carayol, Löding and Serre generalized the model to the setting of infinite trees. They proved that the class of languages recognizable by these automata is effectively closed under all Boolean operations and that the emptiness problem for parity tree automata with these local sibling constraints is decidable. In this thesis we first summarize the existing results of tree automata with local constraints for infinite trees. Then we paritally answer the open question whether the class of languages recognizable by these automata is closed under projection. That is, we show that in the case of automata with Büchi acceptance condition the class of recognizable languages is closed under projection. As a consequence, we obtain a new decision algorithm for the emptiness problem as well as a proof for the fact that each non-empty language recognized by a Büchi tree automaton with sibling constraints contains a regular tree. Moreover, we also study logical characterizations of this class of languages. Tree automata with global constraints were introduced by Filiot, Tison and Talbot in 2008. They studied tree automata on finite trees that can compare subtrees whose positions are defined by the states reached in a run. For example, this model can verify that all subtrees rooted at positions where a certain state is reached are equal. This model was then generalized by Barguñó et. al., who showed the decidability of the emptiness problem. In this thesis we generalize the model of Barguñó et. al. to the setting of infinite trees. We show that most closure properties and decidability results can be extended from finite to infinite trees. However, new techniques are required in order to do so. While the decidability of the emptiness problem remains an open question in general, we present decidability results for some subclasses of tree automata with global constraints. That is, if the automaton tests only for equality of subtrees (and not for inequality) the emptiness problem is decidable. The same is true if the underlying language (i.e. when ignoring the constraints) is countable. We also study the special case of automata with global constraints on unary infinite trees (ω-words). Here we show that in contrast to branching trees, the class of languages recognizable by these automata is closed under complement. Finally, we present precise logical characterizations for all of the subclasses mentioned, by extensions of monadic second order logic on infinite trees (or ω-words)