Tree automata with constraints on infinite trees

• Baumautomaten mit Constraints auf unendlichen Bäumen

Landwehr, Patrick; Löding, Christof (Thesis advisor); Grädel, Erich (Thesis advisor)

Aachen : RWTH Aachen University (2021, 2022)
Doktorarbeit

Dissertation, RWTH Aachen University, 2021

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.

Einrichtungen

• Fachgruppe Informatik [120000]
• Lehrstuhl für Informatik 7 (Logik und Theorie diskreter Systeme) [122910]