Finite automata on unranked trees : extensions by arithmetical and equality constraints

Wong, Karianto; Thomas, Wolfgang; Löding, Christof; Schwentick, Thomas

doi:30429

Finite automata on unranked trees : extensions by arithmetical and equality constraints = Endliche Automaten auf unbeschränkt verzweigten Bäumen : Erweiterungen um arithmetische Bedingungen und Gleichheitsvergleiche

Wong, Karianto

2010

Verantwortlichkeitsangabevorgelegt von Karianto Wong

ImpressumAachen : Publikationsserver der RWTH Aachen University 2010

UmfangVIII, 180 S.

Aachen, Techn. Hochsch., Diss., 2010

Zsfassung in dt. und engl. Sprache

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Löding, Christof (Thesis advisor)^RWTH* ; Thomas, Wolfgang (Thesis advisor) ; Schwentick, Thomas (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2010-06-22

Online
URN: urn:nbn:de:hbz:82-opus-33834
URL: https://publications.rwth-aachen.de/record/63210/files/3383.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Automatentheorie (Genormte SW) ; Baumautomat (Genormte SW) ; Monadische Logik (Genormte SW) ; Presburger-Arithmetik (Genormte SW) ; Informatik (frei) ; Automaten auf unbeschränkt verzweigten Bäumen (frei) ; Presburger-Arithmetik (frei) ; monadische Logik zweiter Stufe (frei) ; Gleichheitsbedingungen und Ungleichheitsbedingungen (frei) ; unranked tree automata (frei) ; Presburger arithmetic (frei) ; monadic second-order logic (frei) ; equality and disequality constraints (frei)

Thematische Einordnung (Klassifikation)
DDC: 004
ccs: F.1.1 * F.4.3

Kurzfassung
Das Modell der unbeschränkt verzweigten Bäume ist in der aktuellen Forschung von großem Interesse, insbesondere aufgrund ihrer Anwendung als formale Modelle von XML-Dokumenten. Hierzu sind in der Literatur Automatenmodelle und Logikformalismen für unbeschränkt verzweigte Bäume (erneut) betrachtet worden. Es hat sich herausgestellt, dass viele Resultate, die zuvor im Kontext der beschränkt verzweigten Bäume gezeigt wurden, ihre Gültigkeit behalten. In der vorliegenden Arbeit werden zwei Arten von Erweiterungen des Modells der endlichen Automaten auf unbeschränkt verzweigten Bäumen, die die Klasse der regulären Baumsprachen charakterisieren, studiert, nämlich die Erweiterung um arithmetische Bedingungen und die Erweiterung um Gleichheitsvergleiche von direkten Teilbäumen. Im ersten Teil der vorliegenden Arbeit wird ein Automatenmodell auf unbeschränkt verzweigten Bäumen eingeführt, das zwei verschiedene Ansätze zur Erweiterung des Modells der endlichen Baumautomaten um arithmetische Bedingungen in sich vereinen: zum Einen den Ansatz der globalen Bedingungen (Klaedtke und Rueß, 2003) und zum Anderen den Ansatz der lokalen Bedingungen (Seidl et al., 2003). Im Kontext des erweiterten Automatenmodells werden die beiden genannten Ansätze bezüglich ihrer Ausdruckskraft verglichen und es wird gezeigt, dass das Leerheitsproblem für das erweiterte Automatenmodell entscheidbar ist. Im zweiten Teil dieser Arbeit wird ein Automatenmodell auf unbeschränkt verzweigten Bäumen mit Gleichheits- und Ungleichheitsbedingungen über direkten Teilbäumen eingeführt, welches das entsprechende Automatenmodell aus dem Fall der beschränkt verzweigten Bäume (Bogaert und Tison, 1992) erweitert. Aufgrund des unbeschränkten Verzweigungsgrads kann es in einer Transition allerdings zu einer unbeschränkten Anzahl von Sohnpositionen, die auf Gleichheit beziehungsweise Ungleichheit getestet werden müssen, kommen. Um dies zu erfassen, werden in der Definition des Automatenmodells Formeln der monadischen Logik zweiter Stufe benutzt, um Gleichheits- und Ungleichheitsbedingungen zu spezifizieren. Es wird gezeigt, dass das Leerheitsproblem für dieses Automatenmodell entscheidbar ist. Auf diesem Resultat aufbauend wird anschließend eine bezüglich des Erfüllbarkeitsproblems entscheidbare Logik über Wörtern über einem unendlichen Alphabet definiert.

The notion of unranked trees has attracted much interest in current research, especially due to their application as formal models of XML documents. In particular, several automata and logic formalisms on unranked trees have been considered (again) in the literature, and many results that had previously been shown for the ranked-tree setting have turned out to hold for the unranked-tree setting as well. In this thesis, we study two kinds of extensions of finite automata on unranked trees, namely, the extension by arithmetical constraints and the extension by subtree-equality constraints. In the first part of the thesis we introduce a framework of automata on unranked trees that unifies two different approaches to incorporating arithmetical constraints known from the literature, namely the global-constraint approach of Klaedtke and Rueß (2003) and the local-constraint approach of Seidl et al. (2003). We investigate the relationship between the two types of arithmetical constraints with respect to language recognition, and we show that the emptiness problem for this automaton model is decidable. In the second part of this thesis, we introduce automata on unranked trees that are equipped with equality and disequality constraints between direct subtrees, thereby extending the corresponding automaton model in the ranked-tree setting, which was introduced by Bogaert and Tison (1982). In the definition of the automaton model, we propose using formulas of monadic second-order logic to capture the possibility of comparing unboundedly many direct subtrees for equality, a feature that arises naturally in light of the unrankedness. Our main result is that the emptiness problem for this automaton model is decidable. Based upon this result, furthermore, we introduce a logic over data words (that is, words over an infinite alphabet) for which the satisfiability problem is decidable.

Fulltext:
PDF