Strukturkonstruktionen und modelltheoretische Spiele in speziellen Strukturklassen
Final Report Abstract
Das Projekt Strukturkonstruktionen und modelltheoretische Spiele in speziellen Strukturklassen hat in Bezug auf zwei seit längerer Zeit offene Probleme, die meine eigene Arbeit schon seit Jahren begleitet haben, mit innovativen Methoden Klarheit schaffen können. Zum einen konnte ein praktisch vollständiges Erklärungsmuster für die Entscheidbarkeit des monadischen Boundedness-Problems für Fragmente der Logik erster Stufe (und in mancher Richtung weit darüber hinaus) gegeben werden, das zusätzlich auch neue Entscheidbarkeitsaussagen geliefert hat. Die Entscheidbarkeitsfrage, ob positiv-monotone Rekursionen ihren Fixpunkt in uniform beschränkter Schrittzahl erreichen, konnte - ganz im Sinne des Projekttitels - durch Variation der zugrunde gelegten Strukturklassen anstelle der syntaktischen Fragmente weitgehend vollständig aufgeklärt werden. Wesentliche Durchbrüche basieren auf diesem fruchtbaren Wechsel der Sichtweise und auf den großen methodischen Neuerungen, die eine technisch anspruchsvolle Reduktion auf ebenfalls ganz neue Resultate in der Automatentheorie erlaubten. Diese entscheidenden Fortschritte hinsichtlich des Boundedness-Problems wurden in Kooperation mit Achim Blumensath und Mark Weyer, aufbauend auch auf erfolgreiche Ansätze aus der Kooperation mit Stephan Kreutzer und Nicole Schweikardt, erzielt. Zum anderen wurden wesentliche technische Durchbrüche in modelltheoretischer und kombinatorischer Hinsicht erzielt in einem Bereich, der die Analyse und Konstruktion endlicher Hypergraphen und die Ausdrucksstärke einer prominenten Klasse von algorithmisch beherrschbaren Logiken betrifft, nämlich die sogenannten bewachten Fragmente der Logik erster Stufe (guarded fragment, GF, GGF). Diese Logiken spielen auch in verschiedensten Anwendungsbereichen als gut angepasste Erweiterungen von Modallogiken eine große Rolle. Es konnten kombinatorische Techniken für Hypergraphen und relationale Strukturen entwickelt werden, die es erlauben, die Analyse der Ausdrucksstärke dieser Logiken anhand modelltheoretischer Spiele (Bisimulationsspiele und das klassische Ehrenfeucht-Fraissé Spiel) im Rahmen der endlichen Modelltheorie besser in den Griff zu bekommen. Insbesondere konnte die natürliche semantische Charakterisierung von GF als Fragment der Logik erster Stufe mit gänzlich neuen Methoden auch für die endliche Modelltheorie bewiesen werden. Weiterhin konnten Fragen zum Verhältnis zwischen homomorphen Einbettungen endlicher Konfigurationen und Nebenbedingungen, die in solchen bewachten Logiken formuliert sind, geklärt werden, die für die Theorie von Datenbanken Bedeutung haben. Schließlich wurden bekannte Schranken für kleine- Modell-Eigenschaften dieser Logiken verbessert, die für die algorithmische Komplexität entsprechender Probleme wichtig sind, und nachgewiesen, dass die Klasse aller unter bewachter Bisimulation invarianten Polynomialzeit-Eigenschaften endlicher Strukturen syntaktisch charakterisiert werden kann. Weitere wichtige, technisch sehr innovative Beiträge aus dem Projekt finden sich in den Arbeiten von Achim Blumensath zur Modelltheorie der monadischen Logik zweiter Stufe (MSO); und besonders auch in den Arbeiten von Alexander Kartzow zur erststufigen Entscheidbarkeit von sehr interessanten unendlichen Strukturen, die hierarchische Klammer-Strukturen darstellen können wie man sie aus rekursiven Programmen kennt, und deren MSO-Theorien im Allgemeinen unentscheidbar sind. In diesen Bereichen wurden exemplarische Einsichten in die grundsätzliche Grenze zwischen Entscheidbarkeit und Unentscheidbarkeit für die algorithmische Modelltheorie erzielt.
Publications
- Boundedness of monadic FO over acyclic Structures. In: Proc. 34th Int. Colloquium on Automata, Languages and Programming, ICALP=07. Lecture Notes in Computer Science, Volume 4596. 2007, pp 571-582
S. Kreutzer, M. Otto, N. Schweikardt
(See online at https://dx.doi.org/10.1007/978-3-540-73420-8_50) - A Lindström characterisation ofthe guarded fragment and of modal logic with a global modality. Advances in Modal Logic, Vol. 7. 2008, pp. 273-287.
M. Otto, R. Piro,
- On the structure of graphs in the Caucal hierarchy, Theoretical Computer Science, Vol. 400. 2008, Issues 1–3, pp. 19–45.
Achim Blumensath
(See online at https://dx.doi.org/10.1016/j.tcs.2008.01.053) - Simple Monadic Theories, Habilitationsschrift, Fachbereich Mathematik, TU Darmstadt, 2008.
Achim Blumensath
- Boundedness of monadic second-order formulae over finite words. In: Automata, Languages and Programming: 36th Int. Colloquium, ICALP 2009, Rhodes, July 5-12, 2009, Proceedings, Part II. Lecture Notes in Computer Science, Vol. 5556. 2009, pp. 67-78.
A. Blumensath, M. Otto, M. Weyer
(See online at https://dx.doi.org/10.1007/978-3-642-02930-1_6) - Modal characterisation theorems over special classes of frames.
Annals of Pure and Applied Logic, Vol. 161. 2009, Issue 1, pp. 1–42.
A. Dawar, M. Otto
(See online at https://dx.doi.org/10.1016/j.apal.2009.04.002) - Collapsible pushdown graphs of level 2 are tree-automatic. In Proc. of the 27th Int. Symp. on Theoretical Aspects of Computer Science STACS'lO, Leibniz Int. Proc. in Informatics, vol. 5. 2010, pp. 501-512. (Logical Methods in Computer Science, Vol. 9.2013, Issue 1, Paper 12)
Alexander Kartzow
(See online at https://dx.doi.org/10.2168/LMCS-9(1:12)2013) - Guarded second-order logic, spanning trees, and network flows. Logical Methods in Computer Science, Vol. 6. 2010, Issue 1, Paper 4.
Achim Blumensath
(See online at https://dx.doi.org/10.2168/LMCS-6(1:4)2010) - Highly acyclic groups, hypergraph covers and the guarded fragment. Logic in Computer Science (LICS), 2010 25th Annual IEEE Symposium on 11-14 July 2010, pp. 11-20.
Martin Otto
(See online at https://dx.doi.org/10.1109/LICS.2010.14) - On the monadic second-order transduction hierarchy. Logical Methods in Computer Science, Vol. 6. 2010, Issue 2, Paper 2.
A. Blumensath, B. Courcelle,
(See online at https://dx.doi.org/10.2168/LMCS-6(2:2)2010) - Querying the guarded fragment, in Proceedings of 25th IEEE Symposium on Logic in Computer Science LICS'lO, 2010, pp. 1-10.
V. Barany, G. Gottlob, M. Otto
(See online at https://dx.doi.org/10.1109/LICS.2010.26) - Decidability results for the boundedness problem. Logical Methods in Computer Science, Vol. 10. 2011, Issue 3, Paper 2.
Achim Blumensath, Martin Otto, Mark Weyer
(See online at https://dx.doi.org/10.2168/LMCS-10(3:2)2014) - First-Order Model Checking on Generalisations of Pushdown Graphs. Dissertation, Fachbereich Mathematik, TU Darmstadt, 2011.
Alexander Kartzow
- Simple monadic theories and indiscemibles. Mathematical Logic Quarterly, Vol. 57. 2011, Issue 1, pp. 65–86.
Achim Blumensath
(See online at https://dx.doi.org/10.1002/malq.200910121) - Simple monadic theories and partition width, Mathematical Logic Quarterly, Vol. 57. 2011,Issue 4, pp. 409-431.
Achim Blumensath
(See online at https://dx.doi.org/10.1002/malq.201010019) - Highly acyclic groups, hypergraph covers and the guarded fragment, Journal of the ACM, Vol. 59. 2012, Issue 1, Article No. 5.
Martin Otto
(See online at https://dx.doi.org/10.1145/2108242.2108247) - Querying the guarded fragment. Logical Methods in Computer Science, Vol. 10.2014, Issue 2, Paper 3.
V. Barany, G. Gottlob, M. Otto
(See online at https://doi.org/10.2168/LMCS-10(2:3)2014)
