Algorithmic Solutions via Model Theoretic Interpretations

• Algorithmische Lösungskonzepte basierend auf modelltheoretischen Interpretationen

Abu Zaid, Faried; Grädel, Erich (Thesis advisor); Kuske, Dietrich (Thesis advisor)

Aachen (2016, 2017)
Doktorarbeit

Dissertation, RWTH Aachen University, 2016

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.

Einrichtungen

• Lehr- und Forschungsgebiet Mathematische Grundlagen der Informatik (Logik und Komplexität) [117220]
• Fachgruppe Mathematik [110000]