Spektren von Verhaltensdistanzen und quantitativen Logiken

• Antragstellerinnen / Antragsteller: Professorin Dr. Barbara König; Professor Dr. Lutz Schröder
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2020
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 434050016

Ein zentrales Thema in der Theorie der Nebenläufigkeit sind Begriffe von Systemäquivalenz, die festlegen, wann sich zwei Systemzustände bezüglich einer gegebenen Semantik gleich verhalten. Für klassische relationale Transitionssysteme variieren solche Systemsemantiken auf einem Spektrum zwischen Äquivalenzen mit verzweigendem Zeitbegriff und solchen mit linearem Zeitbegriff (Branching Time bzw. Linear Time); sie spiegeln unterschiedliche Auffassungen von möglichen Interaktionen mit dem System wieder und werden meist durch geeignete Modallogiken charakterisiert. In diesem Szenario sind Äquivalenzen und Logikenzweiwertig, d.h. zwei Zustände sind stets entweder äquivalent oder inäquivalent, und eine Formel ist in einem Zustand entweder erfüllt oder nicht erfüllt. Für Systeme mit quantitativen Daten wie etwa Wahrscheinlichkeiten, Gewichten oder, allgemeiner, Werten in einem metrischen Raum hat sich gezeigt, dass quantitative Äquivalenzbegriffe, d.h. Verhaltensmetriken, und quantitative Logikenfür manche Zwecke geeigneter sind und eine feinergranulare Systemanalyse erlauben. Während zum Beispiel zwei Zustände inMarkovketten mit kleinen Abweichungen in den Transitionswahrscheinlichkeiten unter zweiwertiger probabilistischer Bisimilarität einfach nur inäquivalent sind, liefert eine geeignete Verhaltensmetrik die genauere Information, dass die beiden Zustände zwar nicht exakt äquivalent, aber in ihrem Verhalten dennoch sehr ähnlich sind.Wie aus den oben genannten Beispielen bereits hervorgeht, finden Verhaltensmetriken natürlicherweise Anwendung auf Systemtypen, die vom üblichen relationalen Modell abweichen; derartige Szenarien sind im Allgemeinen weniger standardisiert und legen eine große Variationsbreite an den Tag. Es besteht insofern Bedarf an uniformen Methoden, die auf viele Systemtypen einheitlich anwendbar sind. Für Branching-Time-Verhaltensmetriken haben wir bereits solche Methoden mit Mitteln der universellen Koalgebra entwickelt, die Systemtypen als Funktoren und Systeme als Funktorkoalgebren abstrahiert. Ziel von SpeQT ist es, diese Methoden zusätzlich über die Systemsemantik zu parametrisieren und so Unterstützung für Spektren von Verhaltensmetriken in koalgebraischer Allgemeinheit bereitzustellen.Das für diese Parametrisierung vorgesehene Werkzeug sind gradierte Monaden, die wir in Vorarbeiten erfolgreich für die entsprechende Parametrisierung zweiwertiger Äquivalenzen eingesetzt haben. Zentrale Forschungsziele sind unter anderem spieltheoretische und logische Charakterisierungen sowie die effiziente Berechnung von Verhaltensdistanzen. Unsere Resultate werden die systematische Herleitung von Logiken, Spielen und Algorithmen für eine große Bandbreite von Systemtypen und das volle Spektrum von Semantiken zwischen Branching Time und Linear Time ermöglichen. Wir werden die entwickelten Algorithmen in Fallstudien zu Differential Privacy und Konformanztests für hybride Systeme testen und evaluieren.

• DFG-Verfahren: Sachbeihilfen