FINGO: Endliche Graphautomaten treffen dynamische Logik

Die Thematik des Projekts betrifft die Schnittstelle von Logik, Datenbanktheorie, Wissensrepräsentation, formaler Softwareverifikation und Automatentheorie. Das im Projekt untersuchte Hauptproblem ist das Erfüllbarkeitsproblem: Gegeben sei eine Formel phi, die in einer bestimmten formalen Sprache L geschrieben ist; wir fragen, ob die Formel phi erfüllbar ist, d.h., ob es eine erfüllende Struktur gibt. In beispielhaften Anwendungen, so wie in der formalen Softwareverifikation, ist die Formel phi die Spezifikation des Betriebs eines Computersystems, und die Struktur ist eine Abstraktion des Programms oder IT-Systems. Dann kann die Frage nach der Erfüllbarkeit verwendet werden, um zu überprüfen, ob das System niemals in eine gefährliche Zone gerät oder ob es darin keine Deadlocks gibt. In Datenbankanwendungen ist phi eine Abfrage an die Datenbank, und die Struktur ist eine relationale Datenbank. Abhängig davon, was L ist, kann das Erfüllbarkeitsproblem rechnerisch einfacher oder schwieriger und sogar unentscheidbar sein. Im Projekt konzentrieren wir uns auf das Problem der endlichen Erfüllbarkeit, das zusätzlich erfordert, dass die gesuchten Strukturen eine endliche Größe haben. Dies spiegelt unsere Realität genauer wider, in der Datenbanken oder biochemische Systeme von Natur aus endlich sind. Wir werden auch unser Interessengebiet auf dynamische Logiken eingrenzen, die zur Programmverifikation dienen, wie Erweiterungen des Mu-Kalküls oder PDL, für die das Problem der endlichen Erfüllbarkeit weiterhin offen ist. Erwähnen wir nur, dass, obwohl es kontraintuitiv erscheinen mag, das Problem der endlichen Erfüllbarkeit oft schwieriger ist und einen völlig anderen Satz von Techniken erfordert als das klassische Erfüllbarkeitsproblem. Zum Beispiel stützt sich das klassische Problem für viele Computerlogiken auf die Baummodelleigenschaft: Wenn eine Struktur existiert, die phi erfüllt, dann existiert auch eine, die einem Baum ähnelt. Und mit Bäumen können wir viel einfacher umgehen, so wie unter Verwendung bekannter Ergebnisse über Automaten, die auf unendlichen Bäumen operieren. Ziel des Projekts ist es, neue Techniken für den Umgang mit dem Problem der endlichen Erfüllbarkeit auf eine Weise vorzuschlagen, die analog zu der oben beschriebenen ist; diesmal werden die Automaten jedoch statt auf unendlichen Bäumen auf endlichen Strukturen arbeiten. Wir wollen eine Reihe von Ergebnissen (Entscheidbarkeit) zu Leerheitsproblemen (wird ein gegebener Automat irgendeinen Graphen akzeptieren?) für Erweiterungen dieser Art von Automaten erarbeiten. Sobald dies gelingt, werden wir unser Framework anwenden, um offene Probleme anzugreifen, so wie die endliche Erfüllbarkeit des Two-Way Graded Mu-Kalküls. Wir hoffen auch, dass unsere Forschung uns der Lösung des Problems der endlichen Erfüllbarkeit von LoopPDL, PDL with Intersection oder Non- Regular PDL, die seit den 80er Jahren offen sind, näherbringen wird.