Koalgebraische Modellprüfung (CoMoC2)

• Antragsteller: Professor Dr. Stefan Milius; Professor Dr. Lutz Schröder
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2019 bis 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 419850228

Eines der zentralen Verifikationsprobleme in der formalen Systementwicklung ist die Modellprüfung, d.h. zu entscheiden, ob ein gegebenes Modell eines Hard- oder Softwaresystems eine gegebene Spezifikation erfüllt, wie etwa Sicherheit, Verklemmungsfreiheit, verlässliche Anfragebeantwortung u.v.m. Eine Spezifikation kann dabei in einer geeigneten Temporallogik formuliert sein, alternativ aber etwa auch als ein weiteres System, das vom zu verifizierenden System in geeigneter Weise verfeinert werden soll. Sich anschließende algorithmische Fragestellungen reichen von der theoretischen Komplexitätsanalyse über die Entwicklung effizienter Modellprüfungsalgorithmen bis hin zu deren Implementierung in automatischen Verifikationswerkzeugen; in diesem Sinne ist die Modellprüfung eine sowohl wissenschaftlich als auch industriell etablierte Forschungsrichtung. Nachdem unter Systemmodellen ursprünglich vor allem relativ einfache relationale Strukturen verstanden wurden, haben mittlerweile ausdrucksstärkere Modelle starke Verbreitung gefunden, in denen die Systemevolution beispielsweise auch probabilistische, gewichtete oder spieltheoretische Aspekte beinhaltet. Damit einher gehen eine entsprechende Auffächerung und zahlenmäßige Vervielfachung von Formalismen zur Modellierung solcher Verhaltensweisen; bekannte Beispiele sind etwa probabilistische Temporallogiken, Game Logic und alternierende Temporallogiken. Ziel von CoMoC ist die Erforschung generischer Formalismen, Methoden und Algorithmen zur einheitlichen Behandlung von Modellprüfungsproblemen über verschiedenen Systemtypen und Systemsemantiken. Erreicht wird dies mittels eines parametrisierten Rahmenwerks: Wir verkapseln den Systemtyp gemäß dem Paradigma der universellen Koalgebra als einen Mengenfunktor, wir abstrahieren lokale Modalitäten mittels Begriffen der koalgebraischen Logik, und wir bilden auf verallgemeinerten linear-time-branching-time-Spektren angesiedelte Systemsemantiken verschiedener Granularität mittels gradierter Monaden ab. In der zweiten Projektphase CoMoC2 werden wir den Anwendungsbereich der generischen Theorie und der aus ihr erwachsenden Algorithmen und Werkzeuge erweitern, mit besonderem Augenmerk auf der Entwicklung effizienter Modellprüfungsalgorithmen für alternierungsfreie Fixpunktlogiken sowie auf Techniken der beschränkten und symbolischen Modellprüfung. Ferner werden wir generische Ausdruckssprachen zur Repräsentation koalgebraischer Systeme im Stile der Prozessalgebra weiterentwickeln, woran sich als weiterer Schwerpunkt der zweiten Projektphase eine Perspektive auf Modellprüfung als Verfeinerung von Ausdrücken anschließt, wie sie klassischerweise etwa für die Prozessalgebra CSP Verwendung findet. Insgesamt entsteht so ein hochgradig generisches Rahmenwerk - parametrisch sowohl im Systemtyp als auch in der Systemsemantik - an Modellrepräsentationssprachen und Spezifikationslogiken mit entsprechenden Modellprüfungsalgorithmen und -werkzeugen.

• DFG-Verfahren: Sachbeihilfen