Koalgebraische Modellprüfung

• 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

In der Spezifikation reaktiver Eigenschaften nebenläufiger Systeme nehmen temporale Logiken verschiedenster Ausprägung einen zentralen Platz ein; sie erlauben die flexible Formulierung von Anforderungen wie Sicherheit, Verklemmungsfreiheit, verlässlicher Beantwortung von Anfragen u.v.m. Nebenläufige Programme und Systeme werden hierbei typischerweise zu geeigneten Formen von endlichen Zustandsmaschinen abstrahiert. Die Überprüfung der Erfülltheit von Anforderungen der genannten Art stellt sich dann als ein Modellprüfungsproblem dar, d.h. man benötigt Entscheidungsalgorithmen für die Erfülltheit von temporalen Formeln über endlichen Zustandsmaschinen. Die Entwicklung solcher Algorithmen und hieraus gewonnener Verifikationswerkzeuge ist eine sowohl wissenschaftlich als auch industriell etablierte Forschungsrichtung.Nachdem man unter Zustandsmaschinen ursprünglich vor allem relativ einfache relationale Strukturen verstanden hatte, 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 Temporallogiken zur Modellierung solcher Verhaltensweisen; bekannte Beispiele sind probabilistische Temporallogiken, Parikhs Game Logic und alternierende Temporallogiken. Ziel von CoMoC ist die Entwicklung generischer Logiken sowie semantischer und algorithmischer Methoden zur Modellprüfung in solchen Logiken. Als Grundlage der beabsichtigten generischen Entwicklung dient die universelle Koalgebra, die eine große Bandbreite an Systemtypen jenseits der rein relationalen Welt unter dem Begriff der Funktorkoalgebra subsumiert und mittlerweile ein umfangreiches Arsenal an allgemeinen metatheoretischen, logischen und algorithmischen Techniken zur Spezifikation und Verifikation solcher Systeme bereitstellt. In CoMoC werden wir sowohl verzweigende als auch lineare generische Temporallogiken in koalgebraischer Allgemeinheit entwickeln. Wir werden hierbei den Stand der Technik insbesondere hinsichtlich der automaten- und spielbasierten Analyse des Modellprüfungsproblems sowie hinsichtlich des Allgemeinheitsgrades der Linearzeitvarianten der verwendeten Logiken vorantreiben. Besonderes Interesse gilt ferner der Behandlung von Logiken über Datenströmen sowie über reaktiven Modellen mit zusätzlichen Berechnungskapazitäten, etwa geteiltem Speicher oder Stapelverarbeitung. Zusammenfassend entsteht so ein vereinheitlichtes Rahmenwerk zur temporalen Spezifikation und Verifikation einer Vielzahl verschiedener Systemtypen.

• DFG-Verfahren: Sachbeihilfen