Generalized Equivalence Checking of Concurrent Programs
We study the spectroscopy problem that asks which notions from a spectrum of behavioral equivalences relate a pair of states in a transition system. This allows a generalized handling of questions on how equivalent two programs are.
As main result, we solve the spectroscopy problem for finite-state systems and a hierarchy of semantic models known as the weak linear-time–branching-time spectrum, due to van Glabbeek. The spectrum arises because of different ways of understanding nondeterminism and internal behavior in models of concurrent programs. We also treat the strong spectrum (without internal behavior) as well as use cases of generalized equivalence checking in verification and concurrency theory.
Our approach relies on a quantitative understanding of spectra in terms of how many syntactic features of Hennessy–Milner modal logic are used to characterize equivalences.
As key trick to solve the spectroscopy problem, we prove spectra of equivalence to be captured by spectroscopy games where energy budgets bound the features an attacker may use to express differences of states. Optimal attack strategies correspond to distinguishing formulas with a minimal usage of syntax. The spectroscopy problem thus reduces to the problem of computing minimal attacker-winning budgets in spectroscopy games. For this, we provide an algorithm to compute such budgets on a wider class of Galois energy games. The resulting spectroscopy algorithms are exponential for the \textsf{PSPACE}-hard spectrum of equivalence problems, but can be instantiated to polynomial-time solutions on the \textsf{P}-easy part.
Aiming for applicability, we implement the spectroscopy procedure in the web tool equiv.io, which continues a tradition of concurrency workbenches. Using it, we can check for dozens of equivalences at once. We apply the spectroscopy approach to small case studies from verification and translation of concurrent programs. Core parts of the thesis are supported by an Isabelle/HOL formalization.
Wir befassen uns mit dem Spektroskopie-Problem. Dieses fragt, welche Verhaltensgleichheiten eines Spektrums Zustände in einem Transitionssystem in Beziehung setzen. Damit wird es möglich, die Frage, wie äquivalent zwei Programme sind, allgemein zu handhaben.
Als Hauptergebnis lösen wir das Spektroskopie-Problem für Systeme mit endlichem Zustandsraum und eine Hierarchie semantischer Modelle, die als „Schwaches Linearzeit–Verzweigungszeit-Spektrum“ nach van Glabbeek bekannt ist. Dieses Spektrum ergibt sich aus verschiedenen Wegen, Nichtdeterminismus und internes Verhalten in Modellen nebenläufiger Programme zu fassen. Wir behandeln auch das „Starke Spektrum“ (ohne internes Verhalten) sowie diverse Anwendungsfälle generalisierter Äquivalenzprüfung in Verifikation und Nebenläufigkeitstheorie.
Unser Ansatz ruht auf einem quantitativen Verständnis von Spektren darin, wie viele syntaktische Möglichkeiten in Hennessy–Milner-Modallogik zur Charakterisierung verwendet werden.
Der zentrale Trick zur Lösung des Spektroskopie-Problems ist, zu zeigen, wie Gleichheitsspektren durch Spektroskopie-Spiele abgedeckt werden. In diesen begrenzen Energiebudgets die Möglichkeiten eines Angreifers, der Unterschiede zwischen Zuständen ausdrücken möchte. Optimale Angriffsstrategien korrespondieren zu unterscheidenden Formeln, die minimale syntaktische Möglichkeiten nutzen. Das Spektroskopie-Problem reduziert sich damit auf die Berechnung minimaler Budgets, mit denen der Angreifer in Spektroskopie-Spielen gewinnt. Hierzu liefern wir einen Algorithmus, mit dem sich solche Budgets für eine größere Klasse von Galois-Energie-Spielen ermitteln lassen. Die sich ergebenden Spektroskopie-Algorithmen sind exponentiell für das \textsf{PSPACE}-harte Spektrum von Gleichheitsproblemen, aber lassen sich zu polynomiellen Lösungen für den \textsf{P}-einfachen Teil instanziieren.
Mit dem Ziel der Anwendbarkeit implementieren wir die Spektroskopie im Web-Tool equiv.io. Dieses Programm folgt einer Tradition von Concurrency-Workbenches. Mit ihm lassen sich dutzende Gleichheiten auf einmal prüfen. Wir wenden den Spektroskopie-Ansatz in kleinen Fallbeispielen aus Verifikation und Übersetzung nebenläufiger Programme an. Zentrale Teile der Arbeit werden durch eine Isabelle/HOL-Formalisierung gestützt.
Dedication
To the memory of Mark Alexander Sibly,
creator of the programming language in which I wrote my first concurrent program, and a profound influence on me and so many others!
Acknowledgments
This research project started due to Covid, in a way. Because of the pandemic, CONCUR’20 was taking place as an online event. And one afternoon, after listening to the talks, sitting alone in my office, I started to implement a small idea on generalizing the bisimulation game. Last year, the office was closed—together with the whole building—because of rusty pipes. Unfortunately, that’s not the only thing that’s been going wrong, since. Crazy times!
That this research project has still reached the stage of a PhD thesis, is thanks to many great people (sorted by category, mostly in order of appearance).
- Environment: Uwe Nestmann and my colleagues at the Modelle und Theorie Verteilter Systeme group, especially my lovely office mates Edgar Arndt and Valeria Zahoransky. Alex Wiemhoefer, who offered a desk in her office when mine was closed. My “Sunday friends” and my parents. You’re all amazing!
- Hospitality: The organizers of the VTSA Summer School 2021 in Liège. Rob van Glabbeek and the Laboratory for Foundations of Computer Science for my 2023 stay in Edinburgh. Julia (and Fréd and kids) as well as Rosi for hosting me during visits in Paris and Oldenburg. David N. Jansen together with Lijun Zhang’s group at the Institute of Software, Chinese Academy of Sciences for my 2024 stay in Beijing.
- Collaboration: David N. Jansen, who discovered and corrected crucial flaws in my ideas. Caroline Lemke, who found out why “my” energy games are indeed decidable. And many more marvelous students and collaborators (listed in Artifacts and Papers).
- Co-writing: Schrippe, Baum, Alina, and Anna S0phia.
- Feedback on parts of this thesis: Nadine Karsten, Caroline Lemke, Andrei Aleksandrov, Dominik Geißler, Uli Fahrenberg, Karl Mattes, Jeroen Keiren, Uwe Nestmann, Amelie Heindl, Gabriel Vogel, Sebastian Wolf, David Karcher, David N. Jansen.