Detailseite
Projekt Druckansicht

Dynamische Ausdrucksstärke von Logiken

Fachliche Zuordnung Theoretische Informatik
Förderung Förderung von 2013 bis 2020
Projektkennung Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 228818952
 
Erstellungsjahr 2020

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)

 
 

Zusatzinformationen

Textvergrößerung und Kontrastanpassung