+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +**********************************************************************

Zeit: Mittwoch, 14. Juli 2021, 10.00 Uhr Ort: Zoom Videokonferenz

Link: https://rwth.zoom.us/j/94853770165?pwd=Uzk4TjI4TGNJQ3owaXJDbUxMT2d0UT09 Meeting-ID: 948 5377 0165 Kenncode: 046795

Referent: Patrick Landwehr M.Sc. Lehrstuhl Informatik 7

Thema: Tree Automata with Constraints on Infinite Trees

Abstract:

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.

Local constraints can be used to compare the direct subtrees of each node. 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 are able to compare 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. In this thesis we generalize the model introduced on finite trees 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 (omega-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 omega-words).

Es laden ein: die Dozentinnen und Dozenten der Informatik