Diploma Thesis DIP-3610

BibliographyWächter, Jan: Das Wortproblem für Omega-Terme über Zweivariablenlogik.
University of Stuttgart, Faculty of Computer Science, Electrical Engineering, and Information Technology, Diploma Thesis No. 3610 (2014).
56 pages, german.
CR-SchemaF.2.2 (Nonnumerical Algorithms and Problems)
F.4.1 (Mathematical Logic)
F.4.3 (Formal Languages)
Abstract

Kaum ein Maschinenmodell ist von so großer Bedeutung wie das der endlichen Automaten. Es findet nicht nur Anwendung in der technischen, theoretischen und praktischen Informatik, sondern auch in vielen anderen Wissenschaften und Wissenschaftsbereichen. Von daher mag es kaum verwundern, dass nicht nur die mit den endlichen Automaten untrennbar verbundenen regulären Sprachen, sondern auch viele darin enthaltene Sprachklassen von großem akademischen und praktischen Interesse sind. Neben der automatentheoretischen Untersuchung der regulären Sprachen gibt es daher noch andere Herangehensweisen: beispielsweise durch Logiken oder durch algebraische Strukturen. Dass es sich bei endlichen Automaten um recht einfache Maschinen handelt, überträgt sich auch auf die algebraischen Strukturen. So werden reguläre Sprachen durch endliche Monoide erkannt, einer algebraischen Struktur, die nur wenigen Axiomen gerecht werden muss. Ein Sprachklasse unterhalb der regulären Sprachen erhält man beispielsweise, indem man sich auf Sprachen beschränkt, die durch Sätze der Prädikatenlogik erster Stufe oder "first-order logic" FO definierbar sind. Durch Beschränkung der Anzahl der in einem solchen Satz erlaubten Variablen lässt sich diese Sprachklasse weiter spezialisieren. Es ist bekannt, dass die Verwendung von nur drei Variablen keine Einschränkung darstellt. Die Untersuchung jener Sprachen, die sich mit Prädikatenlogik erster Stufe unter Verwendung von nur zwei Variablen, also durch die Zweivariablenlogik FO2[<] definieren lassen, ergibt sich daher auf natürliche Weise. Auf algebraischer Seite korrespondiert diese Klasse von Sprachen mit der Menge endlicher Monoide, genauer der Varietät endlicher Monoide DA. Jene Varietät DA erhält man auch durch Vereinigung der abzählbar unendlich hohen, sogenannten Trotter-Weil-Hierarchie. Diese besteht aus Ecken, Join-Ebenen und Schnitt-Ebenen und ist zentraler Gegenstand der Betrachtungen dieser Arbeit. Diese Betrachtungen befassen sich mit dem Wortproblem für Omega-Terme von Varietäten in der Trotter-Weil-Hierarchie. Bei Omega-Termen oder, wie sie hier genannt werden, Pi-Termen handelt es sich um Terme von Variablen, die mit einer zusätzlichen Pi-Potenz versehen werden können. Anschließend können für die Variablen Elemente eines Monoids eingesetzt werden, die Pi-Potenzen erhalten dann einen Wert, der als "unendlich oft" interpretiert werden kann. Anschaulich lässt sich ein Pi-Term daher mit dem Verhalten eines endlichen Automaten, dessen Ausführung nicht durch eine bestimmte Anzahl an Schritten beschränkt ist, verknüpfen. Zwei Pi-Terme u und v lassen sich zu einer Gleichung u = v verknüpfen. Es ist dann möglich zu fragen, ob ein Monoid M diese Gleichung erfüllt. Dies ist dann der Fall, wenn sich links und rechts stets das selbe Monoidelement ergibt, sobald man für die Variablen beliebige Elemente einsetzt. Diese Fragestellung lässt sich erweitern: Erfüllt jedes Monoid in einer Varietät die Gleichung? Dabei handelt es sich um die Frage des Wortproblems für Pi-Terme der Varietät. Diese Arbeit wird zeigt, dass sich das Wortproblem für Pi-Terme der Ecken und Join-Ebenen der Trotter-Weil-Hierarchie durch eine logarithmisch platzbeschränkte nichtdeterministische Turingmaschine entscheiden lässt, dass es also zur Komplexitätsklasse NL gehört. Obwohl es sich bei NL um eine nichtdeterministische Platzklasse handelt, ist dieses Ergebnis interessant, da sich die Probleme aus NL effizient parallel entscheiden lassen. Eine Eigenschaft, die nicht zuletzt seit dem Aufkommen von Mehrkernprozessoren, eine immer größere Rolle spielt. Gleichzeitig liefert ein NL-Algorithmus auch einen deterministischen Polynomialzeitalgorithmus. Der NL-Algorithmus für die Entscheidung des Wortproblems für Pi-Terme der Ecken und Join-Ebenen der Trotter-Weil-Hierarchie lässt sich leicht abwandeln, um die Zugehörigkeit des Wortproblems für Pi-Terme von DA zu NL zu zeigen. Im Sinne der Komplexitätsklassen verbessert dies ein Ergebnis von A.~Moura, das einen deterministischen Polynomialzeitalgorithmus zur Entscheidung dieses Problems liefert und damit Erkenntnisse von Almeida und Zeitoun erweitert, die zeigten, dass sich das Wortproblem für Pi-Terme der Varietät der endlichen R-trivialen Halbgruppen in Linearzeit entscheiden lässt. Die Varietät der endlichen R-trivialen Monoide tritt auch als Ecke in der Trotter-Weil-Hierarchie auf. Das Vorgehen in dieser Arbeit unterscheidet sich von dem Vorgehen in den genannten anderen Arbeiten. Das zentrale Konzept ist dabei das Einsetzen linearer Ordnungstypen für die Pi-Potenzen der Pi-Terme, ähnlich wie bei Huschenbett und Kufleitner. Auf die dabei entstehenden, im Allgemeinen unendlichen, verallgemeinerten Wörter werden dann einige Instrumente, die bei der Untersuchung der Trotter-Weil-Hierarchie sonst in einer endlichen Form vorkommen, übertragen. Am wichtigsten dabei sind die sogenannten Ranker, die auf die "trurtle programs" von Schwentick, Thérien und Vollmer zurückgehen und anschließend u.a. durch Weis und Immerman weiter entwickelt wurden. Über die eindeutige Intervall-Temporallogik von Lodaya, Pandya und Shah ergibt sich ihr Bezug zur Logik.

Full text and
other links
PDF (339246 Bytes)
Department(s)University of Stuttgart, Institute of Formal Methods in Computer Science, Theoretical Computer Science
Superviser(s)Kufleitner, Manfred
Entry dateSeptember 23, 2014
   Publ. Computer Science