Dynamische Ausdrucksstärke von Logiken
Zusammenfassung der Projektergebnisse
Wenn ein kleiner Teil einer Eingabe zu einem algorithmischen Problem verändert wird, kann das Ergebnis von Grund auf neu berechnet werden. Unter Umständen ist es allerdings ressourcenschonender, das bestehende Ergebnis zu aktualisieren, möglicherweise unter Verwendung weiterer gespeicherter Hilfsinformationen. Dieses Projekt hat sich mit der Frage beschäftigt, für welche Probleme die nötige Aktualisierung durch prädikatenlogische Formeln spezifiziert werden kann, und wie komplex die dabei beherrschbaren Änderungen werden können. Als formaler Rahmen diente dabei das von Patnaik und Immerman definierte Setting um die dynamische Komplexitätsklasse DynFO, die alle Anfragen enthält, deren Ergebnis durch prädikatenlogische Update-Formeln unter Verwendung von zusätzlichen Hilfsrelationen aktualisiert werden kann, sowie eine sehr ähnliche Formalisierung von Dong, Su und Topor. Bereits vor Start des Projekts war bekannt, dass in diesem dynamischen Setting die Prädikatenlogik sehr ausdrucksstark ist, und zum Beispiel Erreichbarkeit in ungerichteten sowie in kreisfreien gerichteten Graphen unter Einfügungen und Löschungen einzelner Kanten in DynFO ist. Im Rahmen des Projekts konnte gezeigt werden, dass die dynamische Ausdrucksstärke der Prädikatenlogik noch deutlich größer ist als bekannt. So konnte in Zusammenarbeit mit Ko-Autoren in der ersten Projektphase zunächst bewiesen werden, dass Erreichbarkeit auch in allgemeinen gerichteten Graphen unter einzelnen Kantenänderungen in DynFO ist. Dieses Resultat hat die 20 Jahre alte Vermutung von Patnaik und Immerman bestätigt. Es konnte in der zweiten Projektphase noch einmal deutlich erweitert werden für Änderungen von Mengen von Kanten, die O(log n/log log n) Knoten berühren, für Graphen mit n Knoten. Weiterhin konnten wir für bisher nicht untersuchte Klassen von Anfragen zeigen, dass sie in DynFO aufrechterhalten werden können, zum Beispiel für alle Anfragen für Graphen mit beschränkter Baumweite, die in der monadischen Logik zweiter Stufe spezifiziert werden können, und wir konnten bekannte Resultate für komplexe Änderungsoperationen erweitern. Wir haben insbesondere Änderungen betrachtet, die sich durch prädikatenlogische Formeln definieren lassen [P6], sowie Mengen von f (n) Einzeländerungen, wobei die Funktion f (n) eine Höchstzahl an Änderungen relativ zur Eingabegröße festlegt. Für beide Arten von Änderungen konnten wir bestehende Resultate für Erreichbarkeit und formale Sprachen verallgemeinern. Daneben wurden im Projekt auch Klassen von formalen Sprachen, wie reguläre und kontextfreie Sprachen, sowie statisch in Prädikatenlogik und Erweiterungen von Prädikatenlogik ausdrückbare Anfragen untersucht und ihre dynamische Komplexität bestimmt: welche Logik ist nötig, um das Ergebnis unter Änderungen aufrecht zu erhalten? Für das Fragment von DynFO, das nur quantorenfreie prädikatenlogische Update-Formeln erlaubt, wurden starke Ausdrückbarkeitsresultate gezeigt, aber auch Methoden vorgestellt, um untere Schranken zu zeigen. Im Zusammenspiel dieser Resultate verstehen wir die Beziehungen von Fragmenten von DynFO zueinander nun besser. Für diese Resultate haben wir eine Reihe von Techniken zur Konstruktion von Update-Formeln entwickelt, die auch für weitere Ergebnisse verwendet werden können. Dies betrifft zum Beispiel die Muddling-Technik, mit deren Hilfe nur noch gezeigt werden muss, dass eine Anfrage unter bestimmten Bedingungen für eine begrenzte Anzahl von Änderungsschritten aufrecht erhalten werden kann. Es folgt dann, dass die Anfrage auch unter unbeschränkt vielen Änderungsschritten aufrecht erhalten werden kann. Eine prototypische Implementierung zeigt, dass der DynFO-Ansatz in der Praxis zu kompetitiven Laufzeiten führen kann.
Projektbezogene Publikationen (Auswahl)
- „On the quantifier-free dynamic complexity of Reachability“. In: Inf. Comput. 240 (2015). S. 108–129
Thomas Zeume und Thomas Schwentick
(Siehe online unter https://doi.org/10.1016/j.ic.2014.09.011) - „Static Analysis for Logic-based Dynamic Programs“. In: 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany. Bd. 41. LIPIcs. Schloss Dagstuhl - Leibniz- Zentrum fuer Informatik, 2015, S. 308–324
Thomas Schwentick, Nils Vortmeier und Thomas Zeume
(Siehe online unter https://doi.org/10.4230/LIPIcs.CSL.2015.308) - „Dynamic complexity: recent updates“. In: SIGLOG News 3.2 (2016), S. 30–52
Thomas Schwentick und Thomas Zeume
(Siehe online unter https://doi.org/10.1145/2948896.2948899) - „Dynamic Graph Queries“. In: 19th International Conference on Database Theory, ICDT 2016, Bordeaux, France, March 15-18, 2016. Bd. 48. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016, 14:1–14:18
Pablo Muñoz, Nils Vortmeier und Thomas Zeume
(Siehe online unter https://doi.org/10.4230/LIPIcs.ICDT.2016.14) - Small Dynamic Complexity Classes: An Investigation into Dynamic Descriptive Complexity. Bd. 10110. Lecture Notes in Computer Science. Springer, 2017
Thomas Zeume
(Siehe online unter https://doi.org/10.1007/978-3-662-54314-6) - „Dynamic conjunctive queries“. In: J. Comput. Syst. Sci. 88 (2017). S. 3–26
Thomas Zeume und Thomas Schwentick
(Siehe online unter https://doi.org/10.1016/j.jcss.2017.03.014) - „The dynamic descriptive complexity of k-clique“. In: Inf. Comput. 256 (2017), S. 9–22
Thomas Zeume
(Siehe online unter https://doi.org/10.1016/j.ic.2017.04.005) - „Dynamic Complexity Under Definable Changes“. In: ACM Trans. Database Syst. 43.3 (Okt. 2018). 12:1–12:38
Thomas Schwentick, Nils Vortmeier und Thomas Zeume
(Siehe online unter https://doi.org/10.4230/LIPIcs.ICDT.2017.19) - „Reachability and Distances under Multiple Changes“. In: 45th International Colloquium on Automata, Languages, and Programming, ICALP 2018. Bd. 107. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018, 120:1–120:14
Samir Datta, Anish Mukherjee, Nils Vortmeier und Thomas Zeume
(Siehe online unter https://doi.org/10.4230/LIPIcs.ICALP.2018.120) - „Reachability Is in DynFO“. In: J. ACM 65.5 (Aug. 2018). 33:1–33:24
Samir Datta, Raghav Kulkarni, Anish Mukherjee, Thomas Schwentick und Thomas Zeume
(Siehe online unter https://doi.org/10.1145/3212685) - „A Strategy for Dynamic Programs: Start over and Muddle through“. In: Logical Methods in Computer Science Volume 15, Issue 2 (Mai 2019)
Samir Datta, Anish Mukherjee, Thomas Schwentick, Nils Vortmeier und Thomas Zeume
(Siehe online unter https://doi.org/10.23638/LMCS-15(2:12)2019) - „Dynamic Complexity Meets Parameterised Algorithms“. In: 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain. Bd. 152. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, 36:1–36:17
Jonas Schmidt, Thomas Schwentick, Nils Vortmeier, Thomas Zeume und Ioannis Kokkinis
(Siehe online unter https://doi.org/10.4230/LIPIcs.CSL.2020.36) - „Dynamic Complexity of Parity Exists Queries“. In: 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain. Bd. 152. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, 37:1–37:16
Nils Vortmeier und Thomas Zeume
(Siehe online unter https://doi.org/10.4230/LIPIcs.CSL.2020.37)
