Verhaltensäquivalenzen: Umgebungsaspekte, Metriken und generische Algorithmen

• Antragstellerin: Professorin Dr. Barbara König
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2014 bis 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 260261790

Verhaltensäquivalenzen sind ein wichtiges Konzept für die Analyse und Verifikation von nebenläufigen Systemen. Zwei Prozesse oder Systemzustände sind verhaltensäquivalent, wenn sie ununterscheidbar aus Sicht eines externen Beobachters sind. Je nach Fähigkeit diesesexternen Beobachters erhält man verschiedene Äquivalenzen, wie starke und schwache Bisimularität oder Sprachäquivalenz. Solche Äquivalenzen werden verwendet, um ein System mit seiner Spezifikation zu vergleichen, um große Zustandsräume zu minimieren oder umModelltransformationen und kryptographische Protokolle zu verifizieren. Das Ziel dieses Projektes ist es, eine allgemeine Sicht auf den Begriff der Verhaltensäquivalenz zu erhalten, effiziente Algorithmen für spezifische Systeme bereitzustellen und entsprechende Werkzeuge zuentwickeln. Im Vergleich zur ersten Phase des Projekts wird sich die zweite Phase stärker auf quantitative Aspekte, Logik und Spiele konzentrieren.Insbesondere planen wir auf den folgenden Gebieten zu arbeiten:- Grundlagen (Metriken, Bisimulationsspiele, Bisimularität mit stillen Transitionen)- Spezifische Arten von Systemen (gewichtete Automaten, Transitionssysteme mit Bedingungen, Graphtransformationssysteme)- Werkzeuge und Fallstudien (Werkzeug T-Beg für Verhaltensspiele, Werkzeug Paws für die Analyse von gewichteten Systemen, Fallstudien).

• DFG-Verfahren: Sachbeihilfen
• Mitverantwortlich: Harsh Beohar, Ph.D.