9 Conclusion
The main contribution of this thesis has been to solve Problem 3.1, the spectroscopy problem, deciding all behavioral preorders and equivalences of strong and weak spectrum, in one go. For this objective, we have provided generalized game characterizations for both spectra. To turn these into decision procedures, we have developed a theory of Galois energy games. Thanks to the decision procedures, we can offer tool support for equivalence spectroscopies. So, indeed, there is such a thing as “linear-time–branching-time spectroscopy” (Idea 1.1).
The big picture. Figure 9.1 shows the steps our theory has taken:
- We have started at the level of individual equivalences by revisiting the classical Hennessy–Milner theorem on the dualism of modal distinguishability and behavioral relatability for bisimilarity.
- Chapter 2 has revealed how relations and modal formulas in the Hennessy–Milner theorem are just certificates for defender and attacker strategies in the bisimulation reachability game (Idea 2.1).
- Chapter 3 has taken us to the level of spectra of equivalence, following van Glabbeek’s approach of a hierarchy of Hennessy–Milner theorems (Idea 2.2, Idea 3.1). The spectroscopy problem (Idea 3.2) emerges naturally.
- On this level, Chapter 4 has discovered that the bisimulation game just is an instance of the bisimulation energy game, which characterizes a small spectrum of \textsf{P}-easy strong equivalences (Idea 4.1). We can use it in algorithms thanks to our decision procedure for such Galois energy games (Idea 4.2).
- The bisimulation energy game then again is only a lower-dimensional sibling of the strong spectroscopy game, which characterizes the full strong spectrum in Chapter 5 by a subset construction (Idea 5.1). We can still project it back all the way to the bisimulation game (Idea 5.2).
- With Chapter 6, we have entered the level of van Glabbeek’s (1993) weak spectrum, where silent steps are abstracted, through a weakening of HML (Idea 6.1).
- Chapter 7 has introduced the weak spectroscopy game, where the defender profits from internal transitions (Idea 7.1). Where there is no internal \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}-activity, the game could still serve as a strong spectroscopy game.
In much the same way as we understand equivalences in a hierarchy by folding away dimensions of distinctions, this thesis itself has followed a hierarchy of spectroscopies. Starting from the Hennessy–Milner theorem, we have unfolded aspects, up to the weak spectroscopy. If one looks closely, we have even started one level below: Remark 2.6 notices that the subtractive \leq-game on natural numbers is an instance of the simulation game.
One could frame this journey along Plato’s allegory of the cave: The Hennessy–Milner theorem is a shadow of the bisimulation game, which is a shadow of an energy game, which is a shadow of the strong spectroscopy game, which is a shadow of the weak spectroscopy game. With the tool implementations of Chapter 8, we have returned from the abstract realm of ideas back to a more material level.
But in reality, there is not one single ideal hierarchy of abstraction. Our journey has crossed many routes by other researchers and could have taken different paths. Many interesting ones have been the topic of “Discussion” sections at the end of chapters. Let us close by looking at some ways one could go from here.
Blank spots. There are some classical points to extend research around this thesis. For instance:
- More formalization: Our Isabelle/HOL theory of the weak spectroscopy strengthens many results of the thesis (thanks to the hierarchy of shadows, Figure 9.1). But so far, it does not cover revivals and thus failure-trace-like notions. The proofs in Bisping (2023) give some confidence that the construction is correct, but an Isabelle/HOL formalization would be even nicer.
- More Galois energy games: There exist some interesting questions around the theory of Galois energy games of Chapter 4 and their generalizability to more game variants.1
- More tool support: Proliferation of spectroscopy features to more tools beyond Chapter 8 would be great. Our existing open source implementations can hopefully serve as good starting points.
1 Lemke and Bisping are already writing a paper on this.
More spectra. Concurrency theory knows other variants of linear-time–branching-time spectra. For some, it might be worthwhile to ask spectroscopy questions or to adapt our approach of generalized game characterizations.
There are various quantitative notions, often understood in terms of behavioral distances. They could be included into our game model by allowing the defender a certain amount of “cheating.” For instance, the Q-sets in game positions could be fuzzy, and some budget could define how unlikely positions the defender can pick.
The (strong) quantitative spectrum of Fahrenberg & Legay (2014) already is phrased in terms of a game model. Combining it with our game would likely demand deeper changes to our game mechanics, because one has to remember traces (and not just current states) to compute the resulting distances in full generality.
For Markovian models and probabilistic bisimilarities, there is recent work of “spectro-fication” in Bian & Abate (2017), Baier et al. (2020), and Spork et al. (2024), also extending to silent-step notions. So, this might be the kind of quantitative equivalences where a connection to our approach works best.
Timed equivalences would face conceptual boundaries to decision procedures on finite models: While bisimilarity is decidable, trace preordering is not (Čerāns, 1993).
Barbed and other congruences on \pi-calculi rely on some system of contexts in which to place processes. Fournet & Gonthier (2005) present a hierarchy for asynchronous name-passing calculi, on which one could base a spectroscopy. Valmari (2020) even identifies a spectrum of all linear-time congruences for a sensible set of operators.
Conceptually, it is clear that the selection of a distinguishing context could also happen as an attacker move. In practice, it might be hard to do this elegantly in a way where games remain finite for finite systems. Likely, the most feasible route leads through conditional equivalences (Hülsbusch et al., 2020).
Some kinds of bisimilarity are based on special modalities. For instance, there are forward/reverse bisimilarities (Bernardo & Esposito, 2023) that add modalities to move backwards through the transition graph.
Many such modalities could be added as special moves to the game graph. For modalities where satisfaction depends on infinite behavior, the reachability game framework is not sufficiently expressive. An example would be the divergence modalities mentioned in Section 7.3.3, which require a parity-game winning condition.
A modal-logical turn? This thesis has approached the rich body of work on equivalence and refinement through one unified lens of finding differences in behavior. These were expressed in modal logics (Idea 2.2 “Modal first!”). The perks of modal characterizations have been a recurring topic of the thesis.
In recent years, there seems to be a shift towards the “modal first” approach. The shift is visible in Geuvers and Golov’s work on apartness (Geuvers, 2022; Geuvers & Golov, 2023), similarly in Ford et al. (2021) and Forster et al. (2024) connecting graded modal logics and monads, in Wißmann et al. (2021) strongly linking partition refinement and modal logic, as well as in Beohar et al. (2023) using Galois connections to obtain Hennessy–Milner theorems.
This thesis and its surrounding publications, too, participate in this movement. However, we leave the stack of abstractions around coalgebras and monads aside. One of the effects of this decision is that our framework can be implemented by regular Bachelor students after one introductory course on reactive systems.
The encyclopedic project. Concurrency theory as a field has entered a stage where the initial explosion of questions and approaches has faded. A wave of Festschriften has been appearing. As Garavel (2023) puts it:
Time has come for encyclopedic synthesis: reexamine / select / simplify / sort
This thesis hopes to fit into this project with a “search engine” for equivalences. It shows how to quickly survey spectra of equivalence and how the approach can easily be implemented into tools to support generalized equivalence checking of concurrent programs. While pioneers of the field are retiring, parts of their wisdom thus can be materialized into new generations of software.
After all, concurrent computation will remain relevant, and so will questions on the equivalence of concurrent programs.