Skalierbare und qualitätsbeachtende Synthese von reaktiven Systemen aus LTL Spezifikationen

• Antragsteller: Dr. Salomon Sickert-Zehnter
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2019 bis 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 436811179

Das Sicherstellen von korrektem Verhalten kritischer Systeme, z.B. einer Kontrollsoftware für Flugzeuge oder einer Kraftwerksteuerung, ist von größter Dringlichkeit, um den sicheren und verlässlichen Betrieb von solchen Systemen zu gewährleisten. Weitverbreitete Techniken, wie das Testen solcher Systeme in verschiedenen Situationen, können nicht die Abwesenheit von unerwünschtem Verhalten in allen Fällen garantieren. Formale Methoden wenden mathematisch-fundierte Analysen auf solche Probleme an und können, wenn sie erfolgreich angewendet werden, das korrekte Verhalten der untersuchten Systeme garantieren. Reaktive Systeme, d.h. nicht-terminierende Systeme, die mit einer Umgebung interagieren, sind oft eine passende Abstraktion, um solche kritischen Systeme zu modellieren. Das erwünschte Verhalten des Systems wird oft in einer temporalen Logik, hierbei ist lineare temporale Logik eine weitverbreitete Logik, spezifiziert, da diese erlauben die Interaktion von System und Umgebung in einem zeitlichen Verlauf zu spezifizieren. Obwohl Model-checking, d.h. das automatische Prüfen von Systemen gegen eine Spezifikation, erfolgreich in industriellen Kontext eingesetzt worden ist, ist die Synthese von reaktiven Systemen, d.h. die automatische Konstruktion von reaktiven Systemen aus Spezifikationen, noch nicht für die praktische Anwendung relevant. Es gibt hierbei zwei Faktoren, die diese Entwicklung behindern: Erstens, die bekannten Algorithmen sind nicht in der Lage große Spezifikationen, die notwendig für komplexe Systeme sind, zu verarbeiten. Zweitens, bekannte Algorithmen konstruieren häufig Implementierungen mit schlechter Qualität, d.h die Systeme sind z.B. zu groß, zu ineffizient, oder zu langsam. Im Kontext des Vorhabens sollen neue Ansätze für das Syntheseproblem entwickelt werden. Das Ziel ist neue Algorithmen zu finden, die in der Lage sind komplexe Spezifikationen zu verarbeiten und Implementierungen mit hoher Qualität zu konstruieren. Neben dem Antrieb diese beiden Faktoren, die einer Anwendung von Synthese in der Praxis im Weg stehen, zu beseitigen ist es auch das Ziel zu der Automatentheorie und dem Gebiet der temporalen Logik, die zusammen das Fundament für diese Techniken darstellen, theoretische Ergebnisse beizutragen.

• DFG-Verfahren: Forschungsstipendien
• Internationaler Bezug: Israel
• Gastgeberin: Professorin Orna Kupferman, Ph.D.