Algorithmic Solutions via Model Theoretic Interpretations

Abu Zaid, Faried; Kuske, Dietrich; Grädel, Erich

doi:10.18154/RWTH-2017-07663

Algorithmic Solutions via Model Theoretic Interpretations = Algorithmische Lösungskonzepte basierend auf modelltheoretischen Interpretationen

Abu Zaid, Faried

2016 & 2017

Verantwortlichkeitsangabevorgelegt von Diplom Informatiker Faried Abu Zaid, geb. Schreven

ImpressumAachen 2016

Umfang1 Online-Ressource (199 Seiten) : Illustrationen

Dissertation, RWTH Aachen University, 2016

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2017

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Grädel, Erich (Thesis advisor) ; Kuske, Dietrich (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2016-09-23

Online
DOI: 10.18154/RWTH-2017-07663
URL: http://publications.rwth-aachen.de/record/698352/files/698352.pdf
URL: http://publications.rwth-aachen.de/record/698352/files/698352.pdf?subformat=pdfa

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
algorithmic (frei) ; model theory (frei) ; automata theory (frei)

Thematische Einordnung (Klassifikation)
DDC: 510

Kurzfassung
Modelltheoretische Interpretationen gehören zu den unverzichtbaren Werkzeugen der algorithmischen Modelltheorie. Klassische Anwendungen sind beispielsweise Reduktionen zwischen logischen Theorien oder die Verwendung zur Konstruktion von Algorithmen für im allgemeinen schwierige Probleme, die auf eingeschränkten Strukturklassen jedoch effizient lösbar sind, wie etwa 3-Färbbarkeit auf Graphen beschränkter Baumweite. Wir untersuchen dieses Konzept und seine Anwendungen in drei verschiedenen Bereichen der algorithmischen Modelltheorie: Automatenbasierte Entscheidungsverfahren, algorithmische Metatheoreme und deskriptive Komplexität.Automaten basierte Darstellungen unendlicher Objekte, welche Interpretationen der monadischen Logik zweiter Stufe in Mengenvariablen entsprechen, ist ein besonderes Augenmerk gewidmet. Wir führen parametrisierte automatische Präsentationen ein, welche gewöhnliche automatische Darstellungen dadurch erweitern, dass die Automaten Zugriff auf eine fixierte zusätzliche Hilfseingabe haben. Wir entwickeln algebraische sowie kombinatorische Methoden zur Analyse automatischer Präsentationen. Wir wenden diese an, um zu beweisen, dass bestimmte Strukturen keine automatische Darstellung besitzen. Das Hauptergebnis in dieser Hinsicht ist, dass der Körper der reellen Zahlen keine solche parametrisierte omega-automatische Darstellung zulässt. Dies war seit der Einführung omega-automatischer Präsentationen durch Blumensath und Grädel ein offenes Problem. Das Ergebnis kann auch als die Antwort auf eine abgeschwächte Version einer Frage von Rabin verstanden werden, nämlich ob der Körper der reellen Zahlen in unendlichen Binärbaum Mengen-interpretierbar ist. Wir beschäftigen uns zudem mit uniform darstellbaren Klassen. Dies sind Strukturklassen, die durch eine feste parametrisierte automatische Präsentation darstellen lassen, indem man Parameter aus einer festgelegten Menge betrachtet. Solche uniforme automatische Präsentationen bilden implizit den Kern vieler algorithmischer Metatheoreme.Wir interessieren uns für die Effizienz dieses Ansatzes undanalysieren die Laufzeit des generischen Algorithmus für das Model Checking Problem von uniform baumautomatischen Strukturen in Abhängigkeit zu der Komplexität der gegebenen Präsentation. Wir wenden unsere Ergebnisse an, um zu zeigen, dass FO Model CheckingFPT auf der Klasse der endlichen booleschen Algebren und der endlichen abelschen Gruppen ist.In beiden Fällen ist Laufzeit elementar im Parameter. Die erhaltenen Laufzeiten sind entweder beweisbar optimal oder verbessern die bisher bekannten oberen Schranken. Zusätzlich beweisen wir, dass die Laufzeit für den generischen FPT Algorithmus für MSO Model Checking auf Graphen mit Baumtiefe höchstens h nur (h+2)-fach exponentiell im Parameter ist.Diese Laufzeit entspricht der Laufzeit der zur Zeit besten bekannten Algorithmen für dieses Problem. Wir betrachten Polynomial Time Interpretation Logic (PIL). Diese wurde als eine alternative Charakterisierung der Logik Choiceless Polynomial Time (CPT) eingeführt, welche zur Zeit der erfolgversprechendste Kandidat für eine Logik ist, die PTIME einfangen könnte.Wir tragen zum Verständnis der Ausdrucksstärke von CPT bei, indem wir eine CPT definierbare Kanonisierungsprozedur für Strukturen mit beschränkt großen abelschen Farbklassen angeben. Eine Struktur hat beschränkt große abelsche Farbklassen, wenn sie nur beschränkt große Farbklassen besitzt und die Automorphismengruppen auf den Farbklassen abelsch sind. Beispiele für solche Strukturklassen erwachsen vor allen Dingen aus den bekannten Beispielen, welche Fixpunktlogik mit Zählen von PTIME trennen. So haben etwa die CFI-Graphen (im wesentlichen) beschränkte abelsche Farbeklassen. Dies gilt auch für die Multipedes von Blass, Gurevich und Shelah. Dementsprechend sind dieentsprechenden Isomorphieprobleme im CPT lösbar. Für Multipedes war dies eine offene Frage.

Model theoretic interpretations are an important tool in algorithmic model theory. Their applications range from reductions between logical theoriesto the construction of algorithms for problems, which are hard in general but efficiently solvable on restricted classes of structures, like 3-Colorability on graphs of bounded treewidth. We investigate this tool in three different areas of Algorithmic Model Theory: automata-based decision procedures for logical theories, algorithmic meta-theorems, and descriptive complexity.One of the main focus points of this dissertation are automata based presentations of infinite objects, which are closely related to monadic second-order interpretations over set variables. We introduce automatic presentations with advice for several automata models. These are presentations where the automata have access to some fixed auxiliary information. We develop algebraic and combinatorial tools, which enable us to prove that certain structures cannot have an omega-automatic presentation with advice. Our main result is that the field of reals is not omega-automatic with any advice, which has been an open problem since the introduction of omega-automatic presentations.The result can also be understood as an answer to a weakened version of a question posed by Rabin, namely whether the field of reals is interpretable in the infinite binary tree. Further, we consider uniformly automatic classes of structures, which are classes generated by a fixed presentation and a set of advices. Prototypic examplesare the class of all finite graphs of treewidth bounded by some constant, the torsion-free abelian groups of rank 1, and the class of all countable linear orders. Uniformly automatic presentations are also found in the mechanics that build the foundation for several algorithmic meta-theorems.We investigate the efficiency of this approach by analysing the runtime of the generic automata-based model checking algorithm in terms of the complexity of the given presentation. We show that the runtime on a presentation of the direct product closure is only one exponential higher than the runtime on the presentation of the primal class. We apply these findings to show that first-order model checking is fixed parameter tractable on the classes of all finite Boolean algebras and the class of all finite abelian groups. In both cases the parameter dependence of the runtime is elementary. The runtime which we achieve on these classes is either provably optimal or outperforms the previously known approaches. Furthermore, we show that the runtime of the generic automata based algorithm for monadic second-order model checking on graphs of treedepth at most h has a (h+2)-fold exponential parameter dependence. This matches the runtime of the best known algorithms for model checking on these classes. In the last part of this dissertation we turn our attention to logics with a build-in interpretation mechanism. Polynomial time interpretation logic (PIL) is an alternative characterisation of choiceless polynomial time (CPT). CPT is currently considered the most promising candidate for a logic capturing PTIME. We contribute to the exploration of the expressive power of CPTby showing that there is a CPT-definable canonisation procedure on classes of structures with bounded abelian colours. A structure has bounded abelian colours if it is of bounded colour class size andthe automorphism group on every colour class is abelian. Examples emerge from the classical examples that separate fixed point logic with Counting from PTIME. The CFI-construction of Cai, Fürer, and Immerman, as well as the Multipedes of Blass, Gurevich, and Shelah have bounded abelian colours. Consequently, the isomorphism problem on these classes is solvable in CPT. For Multipedes this was an open question. In fact, Blass, Gurevich, and Shelah conjectured that the isomorphism problem for Multipedes might not besolvable by a CPT procedure.

OpenAccess:
PDF PDF (PDFA)
(additional files)