1 Introduction: What’s the Difference?
Have you ever looked at two program models and wondered how equivalent they are —or, conversely: how they can be distinguished?
I have run into this problem often, for instance when analyzing models of distributed algorithms or when devising examples for teaching. But obviously, the question already occurs every time one rewrites a program part and hopes for it to still do its job.
1 The aim was to bridge between the tools FDR2 and UPPAAL for Göthel’s dissertation (2012). Previous work I was to base the translations on had serious flaws: One approach introduced spurious deadlocks to the model, the other was unable to handle nesting of choices and parallel composition. Clearly, we had to change the encoding!
The first time I had to formally face the question was when working as a student research assistant: I was tasked with implementing a translation from the process algebra Timed CSP to Timed Automata.1 … How to tell whether the translation would properly honor the semantics of the two formalisms? Did it translate CSP terms to automata with the same meaning? Even the definition of the question is tricky, as there are different notions of what counts as “same meaning” in the semantics of programs.
I then took my very first look into the seminal paper on the landscape of process equivalences with internal behavior, the “Linear-time–branching-time spectrum II” by van Glabbeek (1993). Its central figure, reproduced in Figure 1.1, mesmerized me. But, how to use the spectrum to decide for a given pair of processes which of the many equivalences apply, is far from straightforward. Over the years, I have learned that others too have run into this problem: For instance, Nestmann & Pierce (2000) thinking about process algebra encodings and Bell (2013) verifying compiler optimizations. The problem can be summarized as follows:
How does one conveniently decide for a pair of systems which notions from a spectrum of behavioral equivalences equate the two?
Above question will be the research question of this thesis. We2 want to enable future researchers to tap into the wisdom of the linear-time–branching-time spectrum and to easily determine what equivalences fit their models.
2 As you might have noticed, this text uses more personal pronouns than is common in much of computer science literature. Their meaning is the same as in a lecture: “I” = “The author”; “You” = “The audience”; “We” = “The asynchronous collective of author and readers.”
1.1 Linear-Time–Branching-Time Spectroscopy
Van Glabbeek’s papers on comparative concurrency semantics (1990, 1993) treat a zoo of distinct qualitative questions of the form “Are processes p and q equivalent with respect to notion N?”, where N would for example be trace or bisimulation equivalence. He unveils an underlying structure where the questions can easily be compared with respect to their distinctive power. This is analogous to the spectrum of light where seemingly qualitative properties (“The light is blue / green / red.”) happen to be quantitative (“The distribution of wavelengths peaks at 460 / 550 / 630~\mathrm{nm}.”).
For light (i.e. electromagnetic radiation), the mix of wavelengths can be determined through a process called spectroscopy. So, we may ask:
If there exists a “linear-time–branching time spectrum,” does this mean, there also is some kind of “linear-time–branching-time spectroscopy”?
This thesis answers the question positively, which is the key step to tackle our research question. One can compute what mix of (in-)distinguishabilities exists between a pair of processes, and this places the two on the spectrum of equivalences. We thus turn a set of qualitative equivalence problems into one quantitative problem of how equivalent two systems are. As we will see, this amounts to an abstract form of subtraction between programs, determining what kinds of differences an outside examiner might observe.
1.2 This Thesis
The algorithm at the core of this thesis describes how to decide all behavioral equivalences at once for varying spectra of equivalence using games that can count to limit possible distinctions by attacker energy levels. More precisely, we make the following contributions:
- Chapter 2 lays some foundations and makes precise how bisimilarity games relate to grammars of distinguishing formulas of Hennessy–Milner modal logic.
- Chapter 3 shows how to understand the strong linear-time–branching-time spectrum quantitatively and formalizes the spectroscopy problem.
- Chapter 4 introduces the approach of characterizing equivalence spectra through a class of energy games and how to decide such games.
- TODO Chapter 5 applies the approach to decide the whole strong spectrum through one game for linear-time–branching-time spectroscopy.
- TODO Chapter 6 adapt the game for the weak spectrum of equivalences accounting for silent-steps.
- TODO Chapter 7 showcases implementations to conveniently perform equivalence spectroscopies in web browsers and using GPU parallelization.
1.3 Artifacts and Papers
This thesis ties together the work of several publications in a coherent presentation. It is written to be understandable on its own. For details, we usually refer to the original publications or to other artifacts for implementation and machine-checked proofs.
Publications. The following four publications (with me as main author) fuel the following chapters:
- “Deciding All Behavioral Equivalences at Once: A Game for Linear-Time–Branching-Time Spectroscopy” (LMCS 2022) introduces the spectroscopy problem and the core idea to decide the whole strong spectrum using games that search trees of possible distinguishing formulas. (Conference version: TACAS 2021)
- “Process Equivalence Problems as Energy Games” (CAV 2023a) makes a big technical leap by using energy games, removing the necessity for explicit formula construction. (Tech report: arXiv 2023b)
- “Characterizing Contrasimilarity through Games, Modal Logic, and Complexity” (Information & Computation 2024) closes gaps in the weak spectrum of equivalences for games and their complexity and their link to modal logics. (Isabelle/HOL theory: AFP 2023; Workshop version: EXPRESS/SOS 2021)
- “One Energy Game for the Spectrum Between Branching Bisimilarity and Weak Trace Semantics” (EXPRESS/SOS 2024) adapts the spectroscopy approach for the weak spectrum.
Prototype. The algorithms of this thesis have been validated through a Scala prototype implementation. It can be tried out in the browser on https://equiv.io. The source is available openly on https://github.com/benkeks/equivalence-fiddle.
Isabelle formalization. Instead of swamping the document with technical proofs, these are contained in machine-checkable Isabelle/HOL theories.
- Equivalence spectrum formalization contains proofs for the early chapters: https://benkeks.github.io/ltbt-spectroscopy-isabelle/.
- Weak Equivalence Spectroscopy formalizes the core results of Chapter 6: https://equivio.github.io/silent-step-spectroscopy. The theory has been developed together with TU Berlin students Lisa Annett Barthel, Leonard Moritz Hübner, Caroline Lemke, Karl Parvis Philipp Mattes, and Lenard Mollenkopf.
Student theses. Some parts of this thesis strongly rely on student work that I have supervised, in particular, on the following theses:
- Trzeciakiewicz (2021): Linear-Time–Branching-Time Spectroscopy as an Educational Web Browser Game provides a computer game version of the spectroscopy procedure to be discussed in Subsection 7.3.1.
- Ozegowski (2023): Integration eines generischen Äquivalenzprüfers in CAAL extends the Concurrency Workbench Aalborg Edition with a spectroscopy feature, reported in Subsection 7.3.2.
- Mattes (2024): Measuring Expressive Power of HML Formulas in Isabelle/HOL proves the approach to modal characterization of Section 3.2.
- Vogel (2024): Accelerating Process Equivalence Energy Games using WebGPU, topic of Section 7.2, allows massive parallelization on the GPU of key parts of our algorithm.
- Lemke (2024): A Formal Proof of Decidability of Multi-Weighted Declining Energy Games formalizes the fixedpoint algorithm of Section 4.3.
Other publications. Only indirectly connected to this dissertation project are my prior publications in leading me to topic and techniques:
- Bisping et al. (2016, ITP): “Mechanical Verification of a Constructive Proof for FLP.”
- Bisping & Nestmann (2019, TACAS): “Computing Coupled Similarity.”
- Bisping et al. (2020, Acta Informatica): “Coupled similarity: the first 32 years.”
Other Bachelor theses. During my dissertation project, I also supervised several other Bachelor theses, many of which played important roles in shaping the research. Although they do not appear directly on the following pages, I want to acknowledge the students’ vital contribution to the research.
- Peacock (2020): Process Equivalences as a Video Game
- Lê (2020): Implementing Coupled Similarity as an Automated Checker for mCRL2
- Wrusch (2020): Ein Computerspiel zum Erlernen von Verhaltensäquivalenzen
- Reichert (2020): Visualising and Model Checking Counterfactuals
- Wittig (2020): Charting the Jungle of Process Calculi Encodings
- Bulik (2021): Statically Analysing Inter-Process Communication in Elixir Programs
- Montanari (2021): Kontrasimulation als Spiel
- Pohlmann (2021): Reducing Strong Reactive Bisimilarity to Strong Bisimilarity
- England (2021): HML Synthesis of Distinguished Processes
- Duong (2022): Developing an Educational Tool for Linear-Time–Branching-Time Spectroscopy
- Alshukairi (2022): Automatisierte Reduktion von reaktiver zu starker Bisimilarität
- Adler (2022): Simulation fehlertoleranter Konsensalgorithmen in Hash.ai
- Sandt (2022): A Video Game about Reactive Bisimilarity
- Lönne (2023): An Educational Computer Game about Counterfactual Truth Conditions
- Hauschild (2023): Nonlinear Counterfactuals in Isabelle/HOL
- Stöcker (2024): Higher-Order Diadic µ-Calculus—An Efficient Framework for Checking Process Equivalences?
- Kurzan (2024): Implementierung eines Contrasimilarity-Checkers für mCRL2