Skip to main content

1  Introduction: What’s the Difference?

Have you ever looked at two program descriptions and wondered how equivalent they are–or, conversely, how they can be distinguished?

In concurrency theory, one runs into this problem often, for instance, when analyzing models of distributed algorithms or when devising examples for teaching. More mundanely, the question occurs every time that someone rewrites a program part and hopes for it to still do its job.

My first formal encounter with the question of behavioral equivalence came when I was 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.

1  My job as student research assistant was to bridge between the tools FDR2 and UPPAAL for Göthel (2012). The previous work 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!

Figure 1.1: The linear-time–branching-time spectrum with silent moves as depicted in van Glabbeek (1993). ( This thesis will use a simpler version in Figure fig-weak-spectrum.)

I then took my very first look into seminal work on the landscape of process equivalences: the “linear-time–branching-time spectrum” by van Glabbeek (1990, 1993; 2001 with a combined 2500 citations on Google Scholar). A central figure, reproduced in Figure fig-ltbts2-paper, mesmerized me. So many equivalences! But, how to find out for a given pair of processes which of the many equivalences apply? Over the years, I have learned that others, too, have run into the not-quite-straightforward question which equivalences hold: For instance, Nestmann & Pierce (2000) thinking about process algebra encodings and Bell (2013) verifying compiler optimizations. We share an itch.

Our problem   can abstractly 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?

The above question serves as the research question of this thesis. We 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.

1.1 Linear-Time–Branching-Time Spectroscopy

To illustrate the problem, let us look at an example that we will be able to solve via tool support at the end of the thesis in sec-equivio-peterson. It includes numerous concepts that we are going to define and discuss more deeply on our way there.

Example 1.1 (Verifying Peterson’s mutual exclusion) Many verification tasks can be understood along the lines of “how equivalent” two models are. The models can usually be expressed as labeled transition systems, that is, as graphs where nodes represent program states and edges represent transitions between them, labeled by actions.

Figure fig-peterson-mutex replicates a standard example, known, for instance, from the textbook Reactive systems (Aceto et al., 2007): The left-hand side gives a graph specification of mutual exclusion \mathsf{Mx} as two users \mathsf{A} and \mathsf{B} entering their critical section \mathsf{ec_A} / \mathsf{ec_B} and leaving \mathsf{lc_A} / \mathsf{lc_B} before the other may enter. The right-hand side shows the transition system of Peterson’s mutual exclusion algorithm (1981) starting in \mathsf{Pe}, with internal steps \color{gray}\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}} due to the coordination that needs to happen.2 For \mathsf{Pe} to faithfully implement mutual exclusion, it should behave somewhat similarly to \mathsf{Mx}.

2  To fit on the page, \mathsf{Pe} is minimized by a behavioral equivalence that will be important later on: stability-respecting branching bisimilarity.

Figure 1.2: A specification of mutual exclusion \mathsf{Mx}, and Peterson’s protocol \mathsf{Pe}, minimized with respect to stability-respecting branching bisimilarity.

In sec-equivio-peterson, we will regard how the transitions of \mathsf{Pe} derive from pseudocode and formal model.

Semantics in concurrent models must treat nondeterminism and internal steps in some way. As we will see throughout this thesis, setting the degree to which nondeterminism counts induces equivalence notions with subtle differences. In the example, \mathsf{Pe} and \mathsf{Mx} weakly simulate each other, intuitively meaning that a tree of options passing over internal activity from one process can be matched by a similar tree of the other. This implies that they have the same weak traces, that is, matching paths. However, they are not weakly bi-similar, which would require a higher degree of symmetry than mutual similarity, namely, matching absence of options. There are many more such notions, which can be incomparable in how they relate processes. In our example, one might wonder: Are there notions relating \mathsf{Pe} and \mathsf{Mx} besides mutual weak similarity?

State of the art.   For many of the existing behavioral preorders and equivalences, there are various algorithms and implementations to decide whether processes are equivalent (see Garavel & Lang, 2022 for a survey). So, it would be an option to throw an array of algorithms on the transition systems of Example exm-peterson-mutex. For example, let us pick out stable failures and contrasimilarity, which are close to weak similarity in Figure fig-ltbts2-paper. CAAL (Andersen et al., 2015) could establish mutual weak similarity, but does not support the other notions. mCRL2 (Bunte et al., 2019; Groote & Mousavi, 2014) would rule out stable-failure equivalence. But for contrasimilarity, we would need to implement our own solution because there is no tool supporting it. Combining different tools and algorithms like this is tiresome and prone to subtle errors. It would be desirable to treat the question in just one algorithm!

Our offer.   This thesis describes how to decide all equivalences in one uniform approach based on energy games, which is easily implemented in tools.

As we will discuss in more detail in sec-equivio-peterson, our accompanying tool equiv.io answers the question which equivalences apply for Example exm-peterson-mutex in a small query. Here is an excerpt:

Interactive model on equiv.io. 
Pe = (A1 | B1 | TurnA | ReadyAf | ReadyBf)
    \ {readyAf, readyAt, setReadyAf, setReadyAt, readyBf, readyBt,
       setReadyBf, setReadyBt, turnA, turnB, setTurnA, setTurnB}
Mx = ecA.lcA.Mx + ecB.lcB.Mx

@compareSilent Pe, Mx

This query leads to the output in Figure fig-peterson-spectrum,3 which is to be understood as an interactive version of the linear-time–branching-time spectrum of Figure fig-ltbts2-paper.

3  This thesis often provides snippets for models on equiv.io. You can examine and modify the example models by clicking on the links reading Interactive model on equiv.io.

The big blue circle in Figure fig-peterson-spectrum indicates that weak simulation indeed is the most specific equivalence to equate \mathsf{Pe} and \mathsf{Mx}. Lines mean that the notion at the top implies the one below. Blue half-circles indicate preordering only from blue to red side. For instance, \mathsf{Pe} is preordered to \mathsf{Mx} with respect to two more specific notions, namely \eta-simulation and stable simulation (and notions below). Intuitively, this means that \mathsf{Pe} implements \mathsf{Mx} more faithfully than pure weak similarity would demand. Red triangles mark distinctions.

By running one simple algorithm, the tool decides twenty-six equivalence (and preorder) problems on \mathsf{Pe} and \mathsf{Mx} (in about 150 ms on my laptop).

Spectroscopy analogy.   How does the tool decide so many equivalences in one shot? The key are van Glabbeek’s “linear-time–branching-time spectrum” papers on comparative concurrency semantics (1990, 1993). They 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. The papers unveil an underlying structure where equivalences 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 could reframe the question behind this thesis also:

Idea 1.1: A Spectroscopy for the Spectra

If there are “linear-time–branching time spectra,” does this mean that there also is some kind of “linear-time–branching-time spectroscopy”?

The difference that this thesis makes.   We answer the spectroscopy 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 finite-state processes, and this places the two on a spectrum of equivalences. We thus turn a set of qualitative equivalence problems into one quantitative problem of how equivalent two systems are. This amounts to an abstract form of subtraction between programs, determining what kinds of differences an outside examiner might observe. Thereby, one algorithm works for all of a spectrum.

1.2 This Thesis

At the core, this thesis presents an algorithm to decide all behavioral equivalences at once for varying spectra of equivalence using energy games to limit possible distinctions through attacker budgets. More precisely, we make the following contributions, each coming with a “side quest:”

  • sec-preliminaries lays some foundations and makes precise how bisimulation games relate to grammars of distinguishing formulas from Hennessy–Milner modal logic.
    • Main result: Attacker strategies in the bisimulation game \mathcal{G}_{\mathrm{B}} correspond to distinguishing formulas in a subset \smash{\mathcal{O}^{}_{\mathrm{\smash{\lfloor B \rfloor}}}} of modal logic \mathsf{HML} (Theorem thm-game-formulas).
    • Side quest: Certifying algorithms to check equivalences.
  • sec-spectrum shows how to understand the strong linear-time–branching-time spectrum quantitatively and formalizes the spectroscopy problem.
    • Main result: The spectroscopy problem (Problem prob-spectroscopy-problem) is \textsf{PSPACE}-hard for the strong spectrum \mathbf{N}^\mathsf{strong}.
    • Side quest: Equivalence checking as subtraction.
  • sec-approach introduces the approach of characterizing equivalence spectra through energy games and how to decide such games.
  • sec-strong-spectroscopy applies the approach to decide the whole strong spectrum through one game for linear-time–branching-time spectroscopy.
  • sec-weak-spectrum recharts the weak spectrum of equivalences accounting for silent steps to fit our game approach.
    • Main result: The Hennessy–Milner logic subset \mathsf{HML}_{\mathsf{SRBB}} characterizes stability-respecting branching bisimilarity (Theorem thm-srbb-characterization), and its sublogics describe the weak spectrum \mathbf{N}^\mathsf{weak}.
    • Side quest: Case studies in concurrency theory research.
  • sec-weak-spectroscopy adapts the game for the weak spectrum of equivalences.
  • sec-implementations showcases four implementations to conveniently perform equivalence spectroscopies in web browsers and reports some benchmarking results.
    • Main result: Our approach is more general than what is usually found in tools and can compete with algorithms for simulation-like notions.
    • Side quest: Analyzing Peterson’s mutual exclusion protocol.

Each chapter ends with a discussion of its position in the context of the thesis and of related work. sec-conclusion recapitulates how the thesis ascends through a hierarchy of game characterizations and considers the wider picture. Recurring symbols can be looked up under Notation.

Figure 1.4: The theory stack of this thesis. Chapters and ideas build upon those underneath.

Figure fig-thesis-overview gives an overview of how parts of this thesis build upon each other. An example of how to read the figure: sec-approach describes the approach to frame equivalence problems as energy games. It builds on a part of the modal characterization for the strong spectrum in sec-spectrum and on game theory from sec-preliminaries, which is adapted through energy games.

Not this thesis.   We limit ourselves to the relevant parts of the strong spectrum (van Glabbeek, 1990) and the weak spectrum (van Glabbeek, 1993). For instance, this excludes questions around value-passing, open/late/early bisimilarities, and barbed congruences on the \pi-calculus (cf. Sangiorgi, 1996). Also, we do not consider timed or probabilistic equivalences (cf. Baier et al., 2020), nor behavioral distances (Fahrenberg & Legay, 2014). Neither do we aim to re-survey behavioral equivalences in encyclopedic detail, which means that several notions are covered without a detailed discussion of their features and merits.

1.3 Artifacts and Papers

This thesis ties together the work of several publications. It is written to be understandable on its own. For details, we typically refer to the original publications or to other artifacts for implementation and machine-checked proofs.

Publications.   The following five publications fuel the thesis:

  • “Deciding all behavioral equivalences at once: A game for linear-time–branching-time spectroscopy” (LMCS 2022, with Nestmann & Jansen) 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, which removes the necessity for explicit formula construction. (Tech report: arXiv 2023b)
  • “Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems” (CONCUR 2025, with Lemke) generalizes and formalizes the decision procedure of my energy game model. (Lemke’s Isabelle/HOL theory: AFP 2025)
  • “Characterizing contrasimilarity through games, modal logic, and complexity” (Information & Computation 2024, with Montanari) closes gaps in the weak spectrum of equivalences for complexity, games, and their links 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, with Jansen) adapts the spectroscopy approach for the weak spectrum. (Journal version: Preprint 2025; Isabelle/HOL theory: AFP 2025)

Prototype.   The algorithms of this thesis have been validated through a Scala prototype implementation. Throughout the thesis, many examples come with listings of equiv.io input and a link to try it out in the browser. You have already seen one such example for Peterson’s mutex in sec-ltbt-spectroscopy-idea. sec-equivio-usage explains the usage of equiv.io. The source is available openly on https://github.com/benkeks/equivalence-fiddle.

Isabelle formalization.   In order to relieve the document of technical proofs, these are contained in machine-checkable Isabelle/HOL theories archived on https://proofs.equiv.io/. They are split into two Isabelle sessions:

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 sec-spectro-invaders.
  • Ozegowski (2023): “Integration eines generischen Äquivalenzprüfers in CAAL” extends the Concurrency Workbench Aalborg Edition with a spectroscopy feature, reported in sec-spectroscopy-caal, extended by Straßnick & Ozegowski (2024).
  • Mattes (2024): “Measuring expressive power of HML formulas in Isabelle/HOL” proves the approach to modal characterization of sec-ltbt-spectrum.
  • Vogel (2024): “Accelerating process equivalence energy games using Web­GPU,” topic of sec-gpu-equiv, allows massive parallelization of key parts of our algorithm on the GPU.
  • Lemke (2024): “A formal proof of decidability of multi-weighted declining energy games” formalizes the Galois energy games of sec-deciding-energy-games.

Other publications.   My prior publications are only indirectly connected to this PhD thesis. Still, they lead me to topics and techniques:

  • Bisping, Brodmann, Jungnickel, Rickmann, Seidler, Stüber, Wilhelm-Weidner, Peters, Nestmann (ITP 2016): “Mechanical verification of a constructive proof for FLP.”
  • Bisping & Nestmann (TACAS 2019): “Computing coupled similarity.”
  • Bisping, Nestmann, Peters (Acta Informatica 2020): “Coupled similarity: The first 32 years.”

Other student theses.   During this research project, I have also supervised several other Bachelor theses, many of which played important roles in shaping the research. Although most of them do not appear directly on the following pages, I want to acknowledge the students’ vital contributions to this 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–bran­ching-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.”
  • Watermann (2025): “User-friendly web application for high-performance process equivalence checking.”
  • Lifante (2025): “Automating legal reasoning in Isabelle/HOL: An embedding of logics for legal dynamics.”

This thesis itself.   This document itself is created using Quarto (2025). Its HTML version is deployed to https://generalized-equivalence-checking.equiv.io/. One can find its source on https://github.com/benkeks/generalized-equivalence-checking/.

And of course, one can just continue reading it right here. In sec-preliminaries, we will dive into the formal description of equivalence and difference in program behavior, and start building a game framework that lets us solve our problem of generalized equivalence checking in one shot.

Aceto, L., Ingólfsdóttir, A., Larsen, K. G., & Srba, J. (2007). Reactive systems: Modelling, specification and verification (pp. 142–158). Cambridge University Press. https://doi.org/10.1017/CBO9780511814105.008
Adler, R. (2022). Simulation fehlertoleranter Konsensalgorithmen in Hash.ai [Bachelor's thesis]. Tech­ni­sche Uni­ver­si­tät Berlin.
Allaire, J. J., Teague, C., Scheidegger, C., Xie, Y., Dervieux, C., & Woodhull, G. (2025). Quarto (Version 1.7) [Computer software]. https://doi.org/10.5281/zenodo.5960048
Alshukairi, Z. (2022). Automatisierte Reduktion von reaktiver zu starker Bisimilarität [Bachelor's thesis]. Tech­ni­sche Uni­ver­si­tät Berlin.
Andersen, J. R., Andersen, N., Enevoldsen, S., Hansen, M. M., Larsen, K. G., Olesen, S. R., Srba, J., & Wortmann, J. K. (2015). CAAL: Concurrency workbench, aalborg edition. In M. Leucker, C. Rueda, & F. D. Valencia (Eds.), Theoretical aspects of computing — ICTAC 2015 (pp. 573–582). Springer International Publishing. https://doi.org/10.1007/978-3-319-25150-9_33
Baier, C., D’Argenio, P. R., & Hermanns, H. (2020). On the probabilistic bisimulation spectrum with silent moves. Acta Informatica, 57(3), 465–512. https://doi.org/10.1007/s00236-020-00379-2
Barthel, L. A., Hübner, L. M., Lemke, C., Mattes, K. P. P., Mollenkopf, L., & Bisping, B. (2025). The weak spectroscopy game to characterize behavioral equivalences [Isabelle/HOL formalization]. Archive of Formal Proofs. https://isa-afp.org/entries/Weak_Spectroscopy.html
Bell, C. J. (2013). Certifiably sound parallelizing transformations. In International conference on certified programs and proofs (pp. 227–242). Springer. https://doi.org/10.1007/978-3-319-03545-1_15
Bisping, B. (2023a). Process equivalence problems as energy games. In C. Enea & A. Lal (Eds.), Computer aided verification (pp. 85–106). Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-37706-8_5
Bisping, B. (2023b). Process equivalence problems as energy games [Technical Report]. Technische Universität Berlin. https://doi.org/10.48550/arXiv.2303.08904
Bisping, B., Brodmann, P.-D., Jungnickel, T., Rickmann, C., Seidler, H., Stüber, A., Wilhelm-Weidner, A., Peters, K., & Nestmann, U. (2016). Mechanical verification of a constructive proof for FLP. In J. C. Blanchette & S. Merz (Eds.), LNCS: Vol. 9807. Interactive theorem proving (pp. 107–122). Springer International Publishing. https://doi.org/10.1007/978-3-319-43144-4_7
Bisping, B., & Jansen, D. N. (2024). One energy game for the spectrum between branching bisimilarity and weak trace semantics. In G. Caltais & C. Di Giusto (Eds.), EPTCS: Vol. 412. Proceedings Combined 31st International Workshop on expressiveness in concurrency and 21st Workshop on structural operational semantics, Calgary, Canada, 9th September 2024 (pp. 71–88). Open Publishing Association. https://doi.org/10.4204/EPTCS.412.6
Bisping, B., & Jansen, D. N. (2025). Deciding all behavioral equivalences at once II: The silent-step spectrum [Preprint]. https://code.keks.in/papers/2025/silent-step-spectroscopy_journal.pdf
Bisping, B., Jansen, D. N., & Nestmann, U. (2022). Deciding all behavioral equivalences at once: A game for linear-time–branching-time spectroscopy. Logical Methods in Computer Science, 18(3). https://doi.org/10.46298/lmcs-18(3:19)2022
Bisping, B., & Montanari, L. (2021). A game characterization for contrasimilarity. In O. Dardha & V. Castiglioni (Eds.), EPTCS: Vol. 339. Proceedings Combined 28th International Workshop on expressiveness in concurrency and 18th Workshop on structural operational semantics (pp. 27–42). Open Publishing Association. https://doi.org/10.4204/EPTCS.339.5
Bisping, B., & Montanari, L. (2023). Coupled similarity and contrasimilarity, and how to compute them. Archive of Formal Proofs. https://www.isa-afp.org/entries/Coupledsim_Contrasim.html
Bisping, B., & Montanari, L. (2024). Characterizing contrasimilarity through games, modal logic, and complexity. Inf. Comput., 300, 105191. https://doi.org/10.1016/J.IC.2024.105191
Bisping, B., & Nestmann, U. (2019). Computing coupled similarity. In T. Vojnar & L. Zhang (Eds.), LNCS: Vol. 11427. Tools and algorithms for the construction and analysis of systems: TACAS (pp. 244–261). Springer. https://doi.org/10.1007/978-3-030-17462-0_14
Bisping, B., & Nestmann, U. (2021). A game for linear-time–branching-time spectroscopy. In J. F. Groote & K. G. Larsen (Eds.), LNCS: Vol. 12651. Tools and algorithms for the construction and analysis of systems: TACAS (pp. 3–19). Springer. https://doi.org/10.1007/978-3-030-72016-2_1
Bisping, B., Nestmann, U., & Peters, K. (2020). Coupled similarity: The first 32 years. Acta Informatica, 57(3–5), 439–463. https://doi.org/10.1007/s00236-019-00356-4
Bulik, J. (2021). Statically analysing inter-process communication in Elixir programs [Bachelor's thesis, Tech­ni­sche Uni­ver­si­tät Berlin]. https://gitlab.com/MrGreenTea/stille-post
Bunte, O., Groote, J. F., Keiren, J. J. A., Laveaux, M., Neele, T., Vink, E. P. de, Wesselink, W., Wijs, A., & Willemse, T. A. C. (2019). The mCRL2 toolset for analysing concurrent systems. In T. Vojnar & L. Zhang (Eds.), Tools and algorithms for the construction and analysis of systems (pp. 21–39). Springer International Publishing. https://doi.org/10.1007/978-3-030-17465-1_2
Duong, T. M. (2022). Developing an educational tool for linear-time–branching-time spectroscopy [Bachelor's thesis]. Tech­ni­sche Uni­ver­si­tät Berlin.
England, J. (2021). HML synthesis of distinguished processes [Bachelor's thesis]. Tech­ni­sche Uni­ver­si­tät Berlin.
Fahrenberg, U., & Legay, A. (2014). The quantitative linear-time–branching-time spectrum. Theoretical Computer Science, 538, 54–69. https://doi.org/10.1016/j.tcs.2013.07.030
Garavel, H., & Lang, F. (2022). Equivalence checking 40 years after: A review of bisimulation tools. In N. Jansen, M. Stoelinga, & P. van den Bos (Eds.), LNCS: Vol. 13560. A journey from process algebra via timed automata to model learning: Essays dedicated to Frits Vaandrager on the occasion of his 60th birthday (pp. 213–265). Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-15629-8_13
Göthel, T. (2012). Mechanical verification of parameterized real-time systems [PhD thesis, Berlin Institute of Technology]. https://doi.org/10.14279/depositonce-3248
Groote, J. F., & Mousavi, M. R. (2014). Modelling and analysis of communicating systems. MIT Press. https://doi.org/10.7551/mitpress/9946.001.0001
Hauschild, J. (2023). Nonlinear counterfactuals in Isabelle/HOL [Bachelor's thesis, Tech­ni­sche Uni­ver­si­tät Berlin]. https://github.com/johanneshauschild/NonlinearCounterfactuals
Kurzan, T. (2024). Implementierung eines Contrasimilarity-Checkers für mCRL2 [Bachelor's thesis]. Tech­ni­sche Uni­ver­si­tät Berlin.
Lê, H. N. (2020). Implementing coupled similarity as an automated checker for mCRL2 [Bachelor's thesis]. Tech­ni­sche Uni­ver­si­tät Berlin.
Lemke, C. (2024). A formal proof of decidability of multi-weighted declining energy games [Master’s thesis, Technische Universität Berlin]. https://github.com/crmrtz/galois-energy-games/blob/main/master-thesis/masters_thesis.pdf
Lemke, C. (2025). Galois energy games. Archive of Formal Proofs. https://isa-afp.org/entries/Galois_Energy_Games.html
Lemke, C., & Bisping, B. (2025). Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems. In P. Bouyer & J. van de Pol (Eds.), 36th international conference on concurrency theory (CONCUR 2025) (Vol. 348, pp. 29:1–29:19). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2025.29
Lifante, E. (2025). Automating legal reasoning in Isabelle/HOL: An embedding of logics for legal dynamics [Bachelor's thesis]. Tech­ni­sche Uni­ver­si­tät Berlin.
Lönne, B. (2023). An educational computer game about counterfactual truth conditions [Bachelor's thesis, Tech­ni­sche Uni­ver­si­tät Berlin]. https://github.com/Brunololos/counterfactuals-demo
Mattes, K. P. P. (2024). Measuring expressive power of HML formulas in Isabelle/HOL [Bachelor's thesis, Tech­ni­sche Uni­ver­si­tät Berlin]. https://github.com/ekeln/BA_formula_prices/raw/main/output/outline.pdf
Montanari, L. (2021). Kontrasimulation als Spiel [Bachelor's thesis, Tech­ni­sche Uni­ver­si­tät Berlin]. https://github.com/luisamontanari/ContrasimGame
Nestmann, U., & Pierce, B. C. (2000). Decoding choice encodings. Information and Computation, 163(1), 1–59. https://doi.org/10.1006/inco.2000.2868
Ozegowski, F. (2023). Integration eines generischen Äquivalenzprüfers in CAAL [Bachelor's thesis, Tech­ni­sche Uni­ver­si­tät Berlin]. https://github.com/Fabian-O01/CAAL
Peacock, D. A. (2020). Process equivalences as a video game [Bachelor's thesis, Tech­ni­sche Uni­ver­si­tät Berlin]. https://drive.google.com/drive/folders/19YuOCXI_7CEB4p9fgr6kDKCTbFwx2VU9
Peterson, G. L. (1981). Myths about the mutual exclusion problem. Inf. Process. Lett., 12, 115–116. https://doi.org/10.1016/0020-0190(81)90106-X
Pohlmann, M. (2021). Reducing strong reactive bisimilarity to strong bisimilarity [Bachelor's thesis, Tech­ni­sche Uni­ver­si­tät Berlin]. https://maxpohlmann.github.io/Reducing-Reactive-to-Strong-Bisimilarity/thesis.pdf
Reichert, J. M. (2020). Visualising and model checking counterfactuals [Bachelor's thesis]. Tech­ni­sche Uni­ver­si­tät Berlin.
Sandt, E. (2022). A video game about reactive bisimilarity [Bachelor's thesis, Tech­ni­sche Uni­ver­si­tät Berlin]. https://github.com/eloinoel/ReactiveBisimilarityGame
Sangiorgi, D. (1996). A theory of bisimulation for the \pi-calculus. Acta Informatica, 33(1), 69–97. https://doi.org/10.1007/s002360050036
Stöcker, V. (2024). Higher-order diadic µ-calculus—an efficient framework for checking process equivalences? [Bachelor's thesis]. Tech­ni­sche Uni­ver­si­tät Berlin.
Straßnick, T., & Ozegowski, F. (2024). Integration of the weak spectroscopy into CAAL. Tech­ni­sche Uni­ver­si­tät Berlin. https://github.com/equivio/CAAL/blob/spectroscopy/docs/CAAL_weak_Spectroscopy.pdf
Trzeciakiewicz, M. (2021). Linear-time–branching-time spectroscopy as an educational web browser game [Bachelor's thesis, Tech­ni­sche Uni­ver­si­tät Berlin]. https://github.com/Marii19/the-spectroscopy-invaders
van Glabbeek, R. J. (1990). The linear time–branching time spectrum: Extended abstract. In J. C. M. Baeten & J. W. Klop (Eds.), LNCS: Vol. 458. CONCUR’90 (pp. 278–297). Springer. https://doi.org/10.1007/BFb0039066
van Glabbeek, R. J. (1993). The linear time–branching time spectrum II: The semantics of sequential systems with silent moves; extended abstract. In E. Best (Ed.), LNCS: Vol. 715. CONCUR’93 (pp. 66–81). Springer. https://doi.org/10.1007/3-540-57208-2_6
van Glabbeek, R. J. (2001). The linear time–branching time spectrum I: The semantics of concrete, sequential processes. In J. A. Bergstra, A. Ponse, & S. A. Smolka (Eds.), Handbook of process algebra (pp. 3–99). Elsevier. https://doi.org/10.1016/B978-044482830-9/50019-9
Vogel, G. (2024). Accelerating process equivalence energy games using WebGPU [Bachelor's thesis, Tech­ni­sche Uni­ver­si­tät Berlin]. https://github.com/Gobbel2000/gpuequiv
Watermann, F. (2025). User-friendly web application for high-performance process equivalence checking [Bachelor's thesis]. Tech­ni­sche Uni­ver­si­tät Berlin.
Wittig, T. (2020). Charting the jungle of process calculi encodings [Bachelor's thesis, Tech­ni­sche Uni­ver­si­tät Berlin]. https://games.equiv.io/play/process-jungle/
Wrusch, M. (2020). Ein Computerspiel zum Erlernen von Verhaltensäquivalenzen [Bachelor's thesis]. Tech­ni­sche Uni­ver­si­tät Berlin.