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

• Applicant: Professor Dr. Lutz Schröder
• Subject Area: Theoretical Computer Science
• Term: from 2007 to 2021
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 59369218

• Final Report Year: 2020

Final Report Abstract

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.

Publications

• 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
  
• 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
  
• Completeness of flat coalgebraic fixpoint logics. ACM Trans. Comput. Log. (TOCL), 19(1):4:1–4:34, 2018
  Lutz Schröder and Yde Venema
  
• 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