Projekt

Generische algorithmische Verfahren und Komplexitätsschranken für Modal- und Hybridlogiken auf koalgebraischer Basis

Modallogiken spielen in der Informatik traditionell eine zentrale Rolle; so sind etwa die in der Spezifikation nebenläufiger Systeme verwendeten Temporallogiken, moderne Beschreibungslogiken sowie epistemische, deontische und spielbasierte Logiken aus der agentenorientierten Modellierung Spielarten der modalen Logik. Während viele dieser Logiken eine in Begriffen von verschiedenen Typen von Kripkerahmen oder Transitionssystemen definierte relationale Semantik besitzen, weicht die Semantik anderer wichtiger Familien von Logiken vom relationalen Paradigma deutlich ab, indem sie stattdessen z.B. auf Nachbarschaftsrahmen, nebenläufigen Spielen (Concurrent Game Structures), probabilistischen Systemen oder Präferenzstrukturen basiert. Bekannte Beispiele dieser Art sind etwa Parikhs Game Logic (mit der nebenläufigen propositionalen dynamischen Logik CPDL als Fragment), die Alternating-Time Temporal Logic ATL, probabilistische und gewichtete Modallogiken sowie verschiedene Konditionallogiken. Die koalgebraische Logik stellt mittels einer Parametrisierung von Systemen über ihren Verzweigungstyp einen einheitlichen Rahmen für solche Modallogiken zur Verfügung (unter Einschluss der relationalen Semantik als Spezialfall). Trotz ihres hohen Allgemeinheitsgrads bietet die koalgebraische Logik hinreichend innere Struktur für die Entwicklung generischer Deduktionssysteme und -algorithmen und daraus erwachsender Komplexitätsresultate; dies ist der Hauptgegenstand des Projekts. Die dritte Projektphase ist auf die Erweiterung der Ausdrucksmächtigkeit der koalgebraischen Logik zur Erhöhung ihrer Anwendbarkeit in der temporalen und epistemischen Modellierung und in der Wissensrepräsentation ausgerichtet. Dies betrifft insbesondere neuentwickelte bzw. verbesserte Unterstützung für Selbstreferenz, dynamische epistemische Operatoren, Fixpunkte undFuzzy-Modalitäten. Diese Ausdrucksmittel erlauben die Behandlung von Schlüsselaspekten nebenläufiger Systeme und terminologischen Wissens, z.B. hinsichtlich der Weitergabe von Wissen zwischen Agenten, temporalen Schließens über einem breiten Spektrum von Verzweigungstypen oder vager Konzepte. Wir werden ferner vertiefte Resultate zu effizient, d.h. in Polynomialzeit, lösbaren Fragmenten koalgebraischer Logiken anstreben, in Verallgemeinerung von Methoden für die leichtgewichtige Beschreibungslogik EL. Wir werden sowohl für dieses erweiterte Rahmenwerk Deduktionsalgorithmen entwickeln und die Komplexität von Deduktionsproblemen analysieren als auch die Entwicklung des Coalgebraic Logic Ontology Reasoner COOL vorantreiben und das Werkzeug um in der zweiten und dritten Projektphase entwickelte Algorithmen und Ausdrucksmittel erweitern. Als Instanzen des generischen Werkzeugs COOL ergeben sich so insbesondere ein Single-Pass-Tableaubeweiser mit optimaler Worst- Case-Laufzeit für CTL und ATL, ein polynomieller Algorithmus für die konjunktiven Fragmente von ATL und Game Logic sowie ein Tableaubeweiser für Fuzzy-Beschreibungslogiken.

Projektleitung:
Prof. Dr. Lutz Schröder

Stichwörter:
Modallogik; Automatisches Schließen; Hybridlogik; Beschreibungslogik; Temporallogik; Koalgebra

Laufzeit: 1.10.2016 - 30.9.2018

Publikationen

Schröder, Lutz ; Pattinson, Dirk ; Litak, Tadeusz: A van Benthem/Rosen Theorem for Coalgebraic Predicate Logic. In: J. Log. Comput. (2015), Nr. (Advance Access)

Milius, Stefan ; Pattinson, Dirk ; Schröder, Lutz: Generic Trace Semantics and Graded Monads. In: Moss, Lawrence ; Sobocinski, Pawel (Hrsg.) : 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015 (6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015 Nijmegen June 24-26, 2015). Dagstuhl : Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015, S. 253-269. (LIPIcs Bd. 35) - ISBN 978-3-939897-84-2
[doi>10.4230/LIPIcs.CALCO.2015.253]

Hausmann, Daniel ; Schröder, Lutz: Global Caching for the Flat Coalgebraic mu-Calculus. In: Grandi, Fabio ; Lange, Martin ; Lomuscio, Alessio (Hrsg.) : 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015 (TIME 2015 Kassel 23.-25.09.2015). 2015, S. 121-130. (IEEE Comp. Soc.) - ISBN 978-1-4673-9317-1
[doi>10.1109/TIME.2015.15]

Kupke, Clemens ; Pattinson, Dirk ; Schröder, Lutz: Reasoning with Global Assumptions in Arithmetic Modal Logics. In: Kosowski, Adrian ; Walukiewicz, Igor (Hrsg.) : Proc. 20th International Symposium on Fundamentals of Computation Theory, FCT 2015 (FCT 2015 Gdansk, Poland 17.-19.08.2015). Bd. 9210. 2015, S. 367-380. (Lecture Notes in Computer Science) - ISBN 978-3-319-22176-2
[doi>10.1007/978-3-319-22177-9_28]

Kurz, Alexander ; Milius, Stefan ; Pattinson, Dirk ; Schröder, Lutz: Simplified Coalgebraic Trace Equivalence. In: de Nicola, Rocco ; Hennicker, Rolf (Hrsg.) : Software, Services, and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering. Bd. 8950. Berlin : Springer, 2015, (Lecture Notes in Computer Science), S. 75-90. - ISBN 978-3-319-15544-9
[doi>10.1007/978-3-319-15545-6_8]

Enqvist, Sebastian ; Seifan, Fatemeh ; Venema, Yde : Completeness for Coalgebraic Fixpoint Logic. In: Talbot, Jean-Marc ; Regnier, Laurent (Hrsg.) : 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) (25th EACSL Annual Conference on Computer Science Logic (CSL 2016) Marseille (France) 29.08.-01.09.2016). Schloss Dagstuhl : Leibniz-Zentrum fuer Informatik, 2016, S. 7:1-7:19. (Leibniz International Proceedings in Informatics (LIPIcs) Bd. 62) - ISBN 978-3-95977-022-4
[doi>10.4230/LIPIcs.CSL.2016.7]

Hausmann, Daniel ; Schröder, Lutz ; Egger, Christoph: Global Caching for the Alternation-free Coalgebraic mu-calculus. In: Desharnais, Josée ; Jagadeesan, Radha (Hrsg.) : Proceedings of the 27th International Conference on Concurrency Theory, CONCUR 2016 (27th International Conference on Concurrency Theory Québec City, Canada 23.-26.08.2016). Dagstuhl : Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016, S. 34:1-34:15. (LIPIcs Bd. 59)
[doi>10.4230/LIPIcs.CONCUR.2016.34]