Coalgebra-based generic decision procedures and complexity bounds for modal and hybrid logics (GenMod)

Modallogiken und verschiedene Erweiterungen der modalen Grundsprache wie z.B. Hybridlogiken, die die logische Behandlung individueller Zustände erlauben, oder Fixpunktlogiken für temporale Spezifikation spielen in der Informatik und insbesondere in Teilgebieten wie der Analyse reaktiver Systeme und der Wissensrepräsentation traditionell eine zentrale Rolle. In neuerer Zeit ist hierbei eine Tendenz zu semantischen Konzepten zu beobachten, die über die klassische relationale Semantik hinausgehen, etwa zu spielbasierten, probabilistischen oder präferentiellen Systemen; hierdurch ergeben sich dann Logiken wie z.B. alternierende Temporallogik, probabilistische Beschreibungslogiken oder nichtmonotone Konditionallogiken, deren Eigenschaften von denen der rein relationalen Modallogik stark abweichen. Die koalgebraische Logik stellt für solche Logiken einen einheitlichen semantischen Rahmen zur Verfügung, der überraschenderweise auch eine einheitliche algorithmische Behandlung und daran anschließend eine einheitliche Komplexitätsanalyse erlaubt. Ziel des aktuellen Projekts ist die Erweiterung und Vertiefung der algorithmischen Grundlagen der koalgebraischen Logik, insbesondere hinsichtlich iterativer Logiken, Fixpunktlogiken, entscheidbarer Fragmente der koalgebraischen Prädikatenlogik und mehrdimensionaler koalgebraischer Logiken. In Verbindung mit generischen heuristischen Optimierungsstrategien entsteht auf diese Weise ein effizientes generisches Deduktionswerkzeug für koalgebraische Temporal- und Beschreibungslogiken.