h1

000837422 001__ 837422
000837422 005__ 20251016114854.0
000837422 0247_ $$2HBZ$$aHT021207901
000837422 0247_ $$2Laufende Nummer$$a40943
000837422 0247_ $$2datacite_doi$$a10.18154/RWTH-2021-12010
000837422 037__ $$aRWTH-2021-12010
000837422 041__ $$aEnglish
000837422 082__ $$a004
000837422 1001_ $$0P:(DE-588)125028323X$$aLandwehr, Patrick$$b0$$urwth
000837422 245__ $$aTree automata with constraints on infinite trees$$cvorgelegt von Patrick Landwehr, Master of Science$$honline
000837422 246_3 $$aBaumautomaten mit Constraints auf unendlichen Bäumen$$yGerman
000837422 260__ $$aAachen$$bRWTH Aachen University$$c2021
000837422 260__ $$c2022
000837422 300__ $$a1 Online-Ressource : Illustrationen, Diagramme
000837422 3367_ $$02$$2EndNote$$aThesis
000837422 3367_ $$0PUB:(DE-HGF)11$$2PUB:(DE-HGF)$$aDissertation / PhD Thesis$$bphd$$mphd
000837422 3367_ $$2BibTeX$$aPHDTHESIS
000837422 3367_ $$2DRIVER$$adoctoralThesis
000837422 3367_ $$2DataCite$$aOutput Types/Dissertation
000837422 3367_ $$2ORCID$$aDISSERTATION
000837422 500__ $$aVeröffentlicht auf dem Publikationsserver der RWTH Aachen University 2022
000837422 502__ $$aDissertation, RWTH Aachen University, 2021$$bDissertation$$cRWTH Aachen University$$d2021$$gFak01$$o2021-07-14
000837422 5203_ $$aAutomaten 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.$$lger
000837422 520__ $$aTree 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).$$leng
000837422 588__ $$aDataset connected to Lobid/HBZ
000837422 591__ $$aGermany
000837422 653_7 $$aautomata theory
000837422 653_7 $$ainfinite trees
000837422 653_7 $$atree automata
000837422 7001_ $$0P:(DE-82)IDM01355$$aLöding, Christof$$b1$$eThesis advisor$$urwth
000837422 7001_ $$0P:(DE-82)IDM00039$$aGrädel, Erich$$b2$$eThesis advisor$$urwth
000837422 8564_ $$uhttps://publications.rwth-aachen.de/record/837422/files/837422.pdf$$yOpenAccess
000837422 8564_ $$uhttps://publications.rwth-aachen.de/record/837422/files/837422_source.zip$$yRestricted
000837422 909CO $$ooai:publications.rwth-aachen.de:837422$$pdnbdelivery$$pdriver$$pVDB$$popen_access$$popenaire
000837422 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-588)125028323X$$aRWTH Aachen$$b0$$kRWTH
000837422 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM01355$$aRWTH Aachen$$b1$$kRWTH
000837422 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM00039$$aRWTH Aachen$$b2$$kRWTH
000837422 9141_ $$y2021
000837422 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess
000837422 9201_ $$0I:(DE-82)122910_20140620$$k122910$$lLehrstuhl für Informatik 7 (Logik und Theorie diskreter Systeme)$$x0
000837422 9201_ $$0I:(DE-82)120000_20140620$$k120000$$lFachgruppe Informatik$$x1
000837422 961__ $$c2022-02-01T15:39:48.986850$$x2021-12-21T14:16:02.181821$$z2022-02-01T15:39:48.986850
000837422 9801_ $$aFullTexts
000837422 980__ $$aI:(DE-82)120000_20140620
000837422 980__ $$aI:(DE-82)122910_20140620
000837422 980__ $$aUNRESTRICTED
000837422 980__ $$aVDB
000837422 980__ $$aphd