Automatisierte Analyse unendlicher Familien von probabilistischen Systemen (InFamoSS)

• Antragsteller: Professor Dr. Christoph Matheja
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2026
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 569960716

Große und hochgradig konfigurierbare Systeme wie Netzwerke, Energienetze oder Software-Produktlinien sind mit Unsicherheit behaftet, da ihr funktionales und nicht-funktionales Verhalten nicht genau spezifiziert werden kann. Um ihre Leistung, Sicherheit, Privatsphäre, Kosten und Ressourcennutzung zu analysieren und zu optimieren, werden solche Systeme häufig durch Markow-Modelle beschrieben, die Unsicherheit mit Wahrscheinlichkeiten abbilden. Probabilistic Model Checking ist ein weit verbreitetes automatisches Verfahren, welches beweisbare Garantien für das erwartete Verhalten von Markow-Modellen bietet. Die Zuweisung von Wahrscheinlichkeiten an komplexe Systemaktionen ist jedoch ebenfalls mit Unsicherheit behaftet. Daher werden oft Markow-Familien, d.h. Mengen von Markow-Modellen, um verschiedene Szenarien abzudecken. Bestehende Analysetechniken für Markow-Familien konzentrieren sich auf Mengen von Modellen, die (a) von den gewählten Wahrscheinlichkeiten abgesehen identisch sind oder (b) eine Auswahl von Merkmalen eines Gesamtmodells mit einer festen Struktur darstellen. Die Struktur realistischer Systeme kann sich jedoch im Laufe der Zeit dynamisch ändern oder sogar wachsen. So können beispielsweise neue Teilnehmer einem Netzwerk beitreten und neue Funktionen verlangen. Zur Beschreibung und Analyse solcher Systeme muss man daher unendliche Familien von Markow-Modellen betrachten, deren zugrundeliegende Struktur sich anpassen und weiterentwickeln kann. Das Hauptziel des Projekts InFamoSS ist die Entwicklung neuer Methoden für die quantitative Analyse unendlicher Familien von Markow-Modellen mit sich ändernden Zustandsräumen. Hierzu werden solche Familien als formale Sprache von Graphen betrachtet. Wir werden dann Graphgrammatiken verwenden, um zu kontrollieren, wie sich die Topologie einer Familie entwickelt. Anschließend werden wir nachweisbar korrekte Algorithmen und Werkzeuge entwickeln, die die Regeln solcher Graphengrammatiken analysieren, um alle Familienmitglieder ein für alle Mal zu analysieren. Diese Techniken werden die gut ausgebaute Theorie der formalen Sprachen von Graphen und aktuelle Entwicklungen von Zertifikaten für probabilistische Systeme, wie z.B. quantitative Invarianten und Supermartingale, nutzen und miteinander kombinieren.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Dänemark
• Kooperationspartner: Professor Dr. Alberto Lluch-Lafuente