Behavioural Equivalences: Environmental Aspects, Metrics and Generic Algorithms (BEMEGA)
Final Report Abstract
Eine klassische und sehr erfolgreiche Modellierungsmethode der Informatik ist die zustandsbasierte Modellierung. Dabei wird ein System durch seine Zustände und die Übergänge zwischen diesen Zuständen beschrieben. Solche Modelle können entweder manuell erstellt oder aus Code generiert werden. Darauf aufbauend kann man Methoden entwickeln, um Systeme besser zu verstehen und sie insbesondere zu verifizieren, d.h., automatisch ihre Korrektheit – die Erfüllung der Spezifikation – nachzuweisen. Techniken zur Programmverifikation so weit wie möglich zu automatisieren, ist ein sehr erstrebenswertes Ziel, weil es zu garantiert korrekter Software führen kann, andererseits gibt es auf diesem Weg viele Hindernisse: Unentscheidbarkeitsresultate und Probleme mit der Skalierbarkeit. Zahlreiche Forschungsgruppen forschen derzeit auf diesem Gebiet und treiben es weiter voran. Das Ziel des jetzt abgeschlossenen DFG-Projekts BEMEGA (Behavioural Equivalences: Environmental Aspects, Metrics and Generic Algorithms; deutsch: Verhaltensäquivalenzen: Umgebungsaspekte, Metriken und generische Algorithmen) war es dabei, Techniken für Verhaltensäquivalenzen zu erweitern. Dabei stellt man sich die Frage, ob zwei gegebene Systemzustände (beispielsweise die initialen Zustände zweier Systeme) ununterscheidbar aus der Sicht eines externen Beobachters sind. Wenn man diese Frage beantworten kann, so kann man ein System mit seiner Spezifikation vergleichen, Modelle minimieren oder dafür sorgen, dass ein Subsystem problemlos durch ein verhaltensäquivalentes Subsystem ausgetauscht werden kann. Es gibt zahlreiche Anwendungen, beispielsweise bei der Verifikation kryptographischer Protokolle und von Modelltransformationen. Dabei gibt es verschiedene alternative Definitionen für Verhaltensäquivalenzen. Neben der Beschreibung durch Fixpunktgleichungen, die das Verhalten eines Zustands aus dem Verhalten seiner Nachfolger bestimmen, gibt es beispielsweise eine Beschreibung mit Hilfe modallogischer Formeln, die eng mit Verifikationstechniken wie Model-Checking verwandt ist. Es gilt im Allgemeinen, dass zwei Zustände verhaltensäquivalent sind, genau dann, wenn sie dieselben Formeln erfüllen. Außerdem gibt es die Möglichkeit, Verhaltensäquivalenzen über Zwei-Personen-Spiele zu beschreiben, bei denen ein Angreifer gegen eine Verteidigerin antritt. Eine wichtige zu lösende Frage ist immer die effiziente Berechnung von Verhaltensäquivalenzen, um zu beantworten, ob zwei gegebene Zustände tatsächlich das gleiche Verhalten zeigen. In dem Projekt wurden verschiedene Verallgemeinerungen von Verhaltensäquivalenzen untersucht. Beispielsweise ist es bei der quantitativen Modellierung von Systemen, bei der unter anderem Wahrscheinlichkeiten oder Gewichte eine Rolle spielen, nicht sinnvoll zu fragen, ob sich zwei Zustände exakt gleich verhalten, vielmehr kann ihr Verhaltensabstand berechnet werden, der unterhalb einer gegebenen Schranke liegen sollte. So kann man sichergehen, dass zwei Systeme in ihrem Verhalten ausreichend ähnlich sind, was zum Begriff der Verhaltensmetriken führt. Durch die Tatsache, dass Metriken in die reellen Zahlen abbilden und dadurch die Menge aller Metriken immer unendlich ist (such wenn der Zustandsraum selbst endlich ist), ergeben sich bei der Berechnung von Verhaltensmetriken zahlreiche algorithmische Herausforderungen. Zum anderen ist die Tatsache, ob zwei Systeme tatsächlich dasselbe Verhalten zeigen, oft von der Umgebung abhängig. Beispielsweise kann es sein, dass man davon ausgehen kann, dass die Umgebung mit einem System nur auf eine bestimmte Art und Weise interagiert, was dazu führt, dass aus dieser Sicht zwei – ansonsten nicht äquivalente Systeme – das gleiche Verhalten zeigen. Daher wurden im Rahmen des Projekts auch Umgebungsaspekte in Form von bedingten oder kontextuellen Verhaltensäquivalenzen betrachtet, bei denen die Möglichkeiten des Beobachters beschränkt sind. Dabei möchte man beispielsweise berechnen, unter welchen Umgebungen dasselbe Verhalten gezeigt wird. Ein anderer, verwandter, Aspekt ist die Betrachtung von unsichtbaren (internen) Aktionen, die der Beobachter nicht sehen kann. Eine dazu orthogonale Verallgemeinerung ist es, über den Verzweigungs-Typ der betrachteten Systeme zu parameterisieren. Es gibt beispielsweise Verhaltensäquivalenzbegriffe für nichtdeterministische, gewichtete und probabilistische Systeme, die sich bei genauerem Hinsehen als Instanzen des gleichen Konzepts herausstellen. Anstatt Algorithmen, Logiken und Spiele für jeden Begriff einzeln zu entwickeln, ist es deutlich effizienter, diese Konzepte einmal herzuleiten und für jeden System-Typ neu zu instanziieren. So muss man die entsprechenden Eigenschaften und Garantien nur einmal beweisen. Solche Ergebnisse können in der Theorie der Koalgebren erzielt werden. Die bereits weiter oben erwähnten Fixpunktgleichungen sind ein Ansatzpunkt für eine noch abstraktere Sicht auf das Problem, bei denen Lösungsverfahren und auch Spiele direkt in diese Domäne übertragen werden können. Erstaunlicherweise können manche Konzepte und Probleme sogar ohne einen konkreten Bezug auf zustandsbasierte Systeme beschrieben und gelöst werden. Dafür arbeitet man auf bestimmten mathematischen Strukturen, sogenannten vollständigen Verbänden. Im Rahmen dieses Projekts wurden daher Fixpunktgleichungen, Logiken und Spiele sowohl auf Koalgebren, als auch auf vollständige Verbände verallgemeinert und entsprechende Lösungsverfahren beschrieben. Eine der Leistungen ist die Bereitstellung von Methoden, die ganz allgemein funktionieren, aber auch in ganz konkreten Fällen zur Berechnung von Verhaltensäquivalenzen/-metriken, zur Erzeugung unterscheidender modallogischer Formeln oder zur Strategieberechnung bei stochastischen Spielen eingesetzt werden können. Dies erlaubt den Einsatz mathematisch exakter Verfahren in der Systemverifikation. Verschiedene Verfahren wurden in prototypischen Software-Werkzeugen implementiert, in Bezug auf ihre Laufzeit evaluiert und in Fallstudien eingesetzt.
Publications
- (Metric) bisimulation games and realvalued modal logics for coalgebras. In Proc. of CONCUR ’18, volume 118 of LIPIcs, pages 37:1–37:17. Schloss Dagstuhl – Leibniz Center for Informatics, 2018
Barbara König and Christina Mika-Michalski
(See online at https://doi.org/10.4230/LIPIcs.CONCUR.2018.37) - A van Benthem theorem for fuzzy modal logic. In Proc. of LICS ’18, pages 909–918. ACM, 2018
Paul Wild, Lutz Schröder, Dirk Pattinson, and Barbara König
(See online at https://doi.org/10.1145/3209108.3209180) - Coalgebraic behavioral metrics. Logical Methods in Computer Science, 14(3), 2018. Selected Papers of the 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)
Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König
(See online at https://doi.org/10.23638/LMCS-14(3:20)2018) - Up-to techniques for behavioural metrics via fibrations. In Proc. of CONCUR ’18, volume 118 of LIPIcs, pages 17:1– 17:17. Schloss Dagstuhl – Leibniz Center for Informatics, 2018
Filippo Bonchi, Barbara König, and Daniela Petrişan
(See online at https://doi.org/10.4230/LIPIcs.CONCUR.2018.17) - A modal characterization theorem for probabilistic fuzzy modal logic. In Proc. of IJCAI ’19, pages 1900–1906. ijcai.org, 2019
Paul Wild, Lutz Schröder, Dirk Pattinson, and Barbara König
(See online at https://doi.org/10.24963/ijcai.2019/263) - Fixpoint games on continuous lattices. PACMPL (Proc. of POPL ’19), 3:26:1–26:29, 2019
Paolo Baldan, Barbara König, Christina Mika-Michalski, and Tommaso Padoan
(See online at https://doi.org/10.1145/3290339) - Abstraction, up-to techniques and games for systems of fixpoint equations. In Proc. of CONCUR ’20, volume 171 of LIPIcs, pages 25:1–25:20. Schloss Dagstuhl – Leibniz Center for Informatics, 2020
Paolo Baldan, Barbara König, and Tommaso Padoan
(See online at https://doi.org/10.4230/LIPIcs.CONCUR.2020.25) - Conditional bisimilarity for reactive systems. Logical Methods in Computer Science, 18(1), 2022. Selected Papers of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Mathias Hülsbusch, Barbara König, Sebastian Küpper, and Lars Stoltenow
(See online at https://doi.org/10.4230/LIPIcs.FSCD.2020.10) - Conditional transition systems with upgrades. Science of Computer Programming, 186, 2020
Harsh Beohar, Barbara König, Sebastian Küpper, and Alexandra Silva
(See online at https://doi.org/10.1016/j.scico.2019.102320) - Fixpoint theory – upside down. In Proc. of FOSSACS ’21, pages 62–81. Springer, 2021. LNCS/ARCoSS 12650
Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan
(See online at https://doi.org/10.1007/978-3-030-71995-1_4)
