Tree automata with constraints on infinite trees

Landwehr, Patrick; Löding, Christof; Grädel, Erich

doi:10.18154/RWTH-2021-12010

Tree automata with constraints on infinite trees = Baumautomaten mit Constraints auf unendlichen Bäumen

Landwehr, Patrick^RWTH*

2021 & 2022

Verantwortlichkeitsangabevorgelegt von Patrick Landwehr, Master of Science

ImpressumAachen : RWTH Aachen University 2021

Umfang1 Online-Ressource : Illustrationen, Diagramme

Dissertation, RWTH Aachen University, 2021

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2022

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Löding, Christof (Thesis advisor)^RWTH* ; Grädel, Erich (Thesis advisor)^RWTH*

Tag der mündlichen Prüfung/Habilitation
2021-07-14

Online
DOI: 10.18154/RWTH-2021-12010
URL: https://publications.rwth-aachen.de/record/837422/files/837422.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
automata theory (frei) ; infinite trees (frei) ; tree automata (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Automaten auf unendlichen Bäumen sind ein nützliches Werkzeug, welches oft in Entscheidungsalgorithmen und der Synthese von logischen Spezifikationen Anwendung findet. Endliche Automaten haben bekannterweise gute algorithmische Eigenschaften. Allerdings haben sie auch eine etwas eigeschränkte Ausdrucksstärke. Zum Beispiel können Baumautomaten nicht überprüfen, ob bestimmte Teilbäume des Eingabebaumes übereinstimmen. Um solche Eigenschaften modellieren zu können, analysieren wir Erweiterungen von Baumautomaten, welche so genannte `Constraints' verwenden um Teilbäume zu vergleichen. Hierbei unterscheiden wir zwischen zwei Arten von Constraints: Lokale Constraints und globale Constraints. Baumautomaten mit lokalen Constraints wurden zuerst in den 90er Jahren von Bogaert und Tison eingeführt. Diese Autoren analysierten ein Modell von Baumautomaten, welches auf endlichen, beschränkt verzweigten Bäumen arbeitet und zusätzliche Einschränkungen an die erlaubten Transitionen stellt. Diese Einschränkungen ermöglichen zum Beispiel, dass eine bestimmte Transition nur an denjenigen Positionen angewendet werden kann, an denen die Kinder-Teilbäume gleich sind. Vor kurzem haben dann Carayol, Löding und Serre dieses Modell auf unendliche Bäume als Eingabe verallgemeinert. Sie zeigten, dass die Klasse von Sprachen, die von solchen Automaten erkannt werden, effektiv unter allen Boolschen Operationen abgeschlossen ist. Außerdem zeigten sie, dass das Leerheitsproblem für Paritäts-Baumautomaten mit lokalen Geschwister-Constraints entscheidbar ist. In dieser Arbeit fassen wir zunächst die bestehenden Resultate über Baumautomaten mit lokalen Constraints für unendliche Bäume zusammen. Danach geben wir eine Teil-Antwort auf die offene Frage, ob die Klasse der Sprachen die von diesen Automaten erkannt werden unter Projektionen abgeschlossen ist. Genauer gesagt zeigen wir, dass im Fall von Automaten mit Büchi-Akzeptanzbedingung die Klasse von erkannten Sprachen effektiv unter Projektionen abgeschlossen ist. Als eine Konsequenz aus diesem Resultat erhalten wir einen neuen Entscheidungsalgorithmus für das Leerheitsproblem, sowie einen Beweis dafür, dass jede nicht-leere erkannte Sprache einen regulären Baum enthält. Zusätzlich dazu geben wir in dieser Arbeit eine logische Charakterisierung für diese Klasse von Sprachen. Im Gegensatz zu den lokalen Constraints wurden Baumautomaten mit globalen Constraints in 2008 von Filiot, Tison und Talbot eingeführt. Sie präsentierten ein Modell auf endlichen Bäumen, welches in der Lage ist Teilbäume zu vergleichen, die beliebig weit voneinander entfernt sind. Zum Beispiel können diese Baumautomaten mit globalen Constraints überprüfen, ob alle Teilbäume an Positionen an denen der Automat einen bestimmten Zustand erreicht gleich sind. Dieses Modell wurde später von Barguñó und anderen erweitert, welche einen Entscheidungsalgorithmus für das Leerheitsproblem dieses Automaten-Modells entwickelt haben. Bezüglich globaler Constraints erweitern wir in dieser Arbeit das Modell, welches von Barguñó und anderen vorgestellt wurde, auf unendliche Bäume als Eingabe. Hier zeigen wir, dass die meisten Abschlusseigenschaften und Entscheidbarkeits-Resultate von endlichen auf unendliche Bäume übertragen werden können. Allerdings werden hierbei neue Methoden benötigt. Obwohl die Entscheibarkeit des Leerheitsproblems für diese Automaten auf unendlichen Bäumen eine offene Frage bleibt, präsentieren wir Entscheidbarkeitsergebnisse für verschiedene eingeschränkte Modelle. Genauer gesagt, wenn der Automat Teilbäume nur auf Gleichheit (und nicht auf Ungleichheit) überprüfen kann, ist das Leerheitsproblem entscheidbar. Dasselbe gilt in dem Fall, dass die zu Grunde liegende Sprache (die Sprache des Automaten, wenn die Constraints ignoriert werden) abzählbar ist. Außerdem analysieren wir Automaten mit globalen Constraints, die als Eingabe nur unäre Bäume (ω-Wörter) erlauben. Hier zeigen wir, dass im Gegensatz zum Fall von verzweigten Bäumen die Klasse von erkannten Sprachen unter Komplement abgeschlossen ist. Abschließend präsentieren wir auch hier logische Charakterisierungen für die verschiedenen, oben erwähnten Teilklassen, indem wir die monadische Logik zweiter Stufe auf für unendliche Bäume (oder ω-Wörter) um Prädikate und Quantoren erweitern, die Vergleiche von Teilbäumen ermöglichen.

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).

OpenAccess:
PDF
(additional files)