Generische algorithmische Verfahren und Komplexitätsschranken für Modal- und Hybridlogiken auf koalgebraischer Basis
Zusammenfassung der Projektergebnisse
Modale und temporale Logiken spielen in der Informatik eine etablierte Rolle als Formalismen für Softwarespezifikation und Wissensrepräsentation. Ihre Semantik wird klassischerweise über relationalen Strukturen definiert, in denen einzelne Knoten – interpretiert z.B. als Systemzustände oder Individuen in einer Grundgesamtheit – über Kanten verbunden sind, die z.B. Zustandsübergänge oder Beziehungen zwischen Individuen repräsentieren. Andererseits besteht aber auch seit Langem substanzielles Interesse an Logiken, in denen die Knoten auf kompliziertere Weise verbunden sind, z.B. durch Übergangswahrscheinlichkeiten, Spiele, deren Ausgang durch die Entscheidungen mehrerer Agenten bestimmt wird, Ähnlichkeitsrelationen und vieles mehr. Bekannte Logiken dieser Spielart sind z.B. die alternierende Temporallogik, die der Spezifikation der langfristigen Einflussmöglichkeiten von Gruppen von Agenten dient; probabilistische Modallogiken, die über die Wahrscheinlichkeit zukünftiger Ereignisse sprechen; oder Konditionallogiken, die sich mit nichtmateriellen Implikationen etwa der Art wenn – dann normalerweise befassen. Im Projekt GenMod sind generische Methoden entwickelt worden, die das systematische und automatisierte Schlussfolgern über solchen Logiken unterstützen. Besonderer Fokus liegt dabei auf der Effizienz solcher Methoden hinsichtlich Zeit- und Speicherverbrauch, zum einen im Sinne einer theoretisch optimalen Effizienz im schlechtest denkbaren Fall als auch im Sinne einer heuristischen Optimierung, die in praktisch auftretenden Fällen schnelle Antworten liefert. Die im Projekt entwickelten Algorithmen sind im frei verfügbaren Coalgebraic Ontologiy Logic Solver (COOL) implementiert, der, obwohl in erster Linie für nichtrelationale Logiken ausgelegt, auch für einige weitverbreitete klassischrelationale Logiken wie etwa die Computation Tree Logic (CTL) zur Zeit eines der weltweit effizientesten automatischen Beweiswerkzeuge ist, und für zahlreiche andere Logiken – einschließlich vergleichsweise bekannter Beispiele wie der Alternating-Time Temporal Logic, die der Spezifikation von Agentensystemen dient – im wesentlichen das einzige verfügbare hinreichend effiziente Werkzeug darstellt.
Projektbezogene Publikationen (Auswahl)
- Automatic verification of application-tailored OSEK kernels. In Daryl Stewart and Georg Weissenbacher, eds., Formal Methods in Computer Aided Design, FMCAD 2017, pp. 196–203. IEEE, 2017
Hans-Peter Deifel, Merlin Göttlinger, Stefan Milius, Lutz Schröder, Christian Dietrich, and Daniel Lohmann
(Siehe online unter https://doi.org/10.23919/FMCAD.2017.8102260) - Uniform interpolation in coalgebraic modal logic. In Filippo Bonchi and Barbara König, eds., 7th Conference on Algebra and Coalgebra in Computer Science, CALCO 2017, vol. 72 of LIPIcs, pp. 21:1–21:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017
Fatemeh Seifan, Lutz Schröder, and Dirk Pattinson
(Siehe online unter https://doi.org/10.4230/LIPIcs.CALCO.2017.21) - Completeness of flat coalgebraic fixpoint logics. ACM Trans. Comput. Log. (TOCL), 19(1):4:1–4:34, 2018
Lutz Schröder and Yde Venema
(Siehe online unter https://doi.org/10.1145/3157055) - Game-based local model checking for the coalgebraic mu-calculus. In Wan Fokkink and Rob van Glabbeek, eds., 30th International Conference on Concurrency Theory, CONCUR 2019, vol. 140 of LIPIcs, pp. 35:1–35:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019
Daniel Hausmann and Lutz Schröder
(Siehe online unter https://doi.org/10.4230/LIPIcs.CONCUR.2019.35)
