Fixpunktlogiken: Ausdrucksstärke, Struktur, Komplexität
Zusammenfassung der Projektergebnisse
Fixpunktlogiken spielen in vielen Gebieten der Mathematischen Logik und ihren Anwendungen in der Informatik eine zentrale Rolle. In diesem Vorhaben haben wir Fixpunktlogiken insbesondere im Zusammenhang mit der Suche nach einer Logik für Polynomialzeit und der Definierbarkeit algorithmischer Probleme der Linearen Algebra untersucht, ausserdem im Kontext von Fragen der Bisimulationssicherheit auf Transitionssystemen und der Definierbarkeit von Gewinnstrategien in unendlichen Spielen. Eine zentrale Herausforderung im Gebiet der Endlichen Modelltheorie ist die Frage nach der Existenz einer Logik für Polynomialzeit (Ptime). Die wichtigsten Kandidaten für eine solche Logik sind einerseits Fixpunktlogiken mit Operatoren der Linearen Algebra, insbesondere die Ranglogik, und andererseits Choiceless Polynomial Time als Modell für symmetrie-invariante Algorithmen, welche jede explizite, symmetriebrechende Auswahl zwischen ununterscheidbaren Elementen vermeiden. Für beide Ansatze hat dieses Forschungsprojekt zahlreiche neue Einsichten in Struktur, Ausdrucksstärke und Komplexität dieser Formalismen geliefert. Highlights dieses Projekts sind z.B. das Resultat, dass die Ranglogik in ihrer ursprünglichen Form nicht ausreicht um Ptime zu charakterisieren (was zu einer stärkeren Variante der Ranglogik als neuer Kandidat für eine solche Charakterisierung führt) und neue Konstruktionen von symmetrieinvarianten Choiceless-Algorithmen für die Kanonisierung bestimmter Strukturklassen und das Losen wichtiger Klassen von linearen Gleichungssystemen. Methodisch haben wir in diesem Vorhaben eine Reihe neuer Konstruktionen für symmetrieinvariante Algorithmen und für Definierbarkeit in Fixpunktformalismen gefunden, welche auch in zukünftigen Projekten fruchtbar sein werden. Ausserdem haben wir in diesem Projekt eine neue modale und bisimulationssichere Fixpunktlogik eingeführt und untersucht, welche über die klassische Definition von Zustandseigenschaften hinaus auch Eigenschaften von Transitionen definiert, und damit auch in dieser Hinsicht dynamische Logiken wie PDL verallgemeinert, mit interessanten Zusammenhängen zu kontextfreien Sprachen. Schliesslich haben wir gezeigt, dass Fixpunktlogiken auch für die Konstruktion von Gewinnstrategien in Paritätsspielen sehr nützlich und ausdrucksstark sind. Insgesamt zeigen die Resultate dieses Projekts, dass die untersuchten verschiedenen Varianten von Fixpunktformalismen eine deutlich höhere Ausdrucksstärke besitzen, als wir dies zu Beginn dieses Vorhabens erwarten konnten.
Projektbezogene Publikationen (Auswahl)
-
Characterising Choiceless Polynomial Time with First-Order Interpretations, Logic in Computer Science (LICS), 2015
E. Grädel, L. Kaiser, W. Pakusa, S. Schalthöfer
-
Defining winning strategies in fixedpoint logic. Logic in Computer Science (LICS), 2015
F. Canavoi, E. Grädel, S. Lessenich, and W. Pakusa
-
Is Polynomial Time Choiceless?, Fields of Logic and Computation II. Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, vol. 9300 of LNCS, pp. 193-209. Springer, 2015
E. Grädel and M. Grohe
-
Linear Equation Systems and the Search for a Logical Characterization of Polynomial Time, Doctoral Dissertation, RWTH Aachen University, 2015
W. Pakusa
-
Algorithmic Solutions via Model Theoretic Interpretations, Doctoral Dissertation, RWTH Aachen University, 2016
F. Abu Zaid
-
Definability of Summation Problems for Abelian Groups and Semigroups, Logic in Computer Science (LICS), 2017
F. Abu Zaid, A. Dawar, E. Grädel, and W. Pakusa
-
The Model-Theoretic Expressiveness of Propositional Proof Systems, Computer Science Logic (CSL), 2017
E. Grädel, B. Pago, and W. Pakusa
-
(2019). Rank logic is dead, long live rank logic!. The Journal of Symbolic Logic, 84 (1) 54-87
Grädel, Erich, Wied Pakusa
