6  Recharting the Weak Silent-Step Spectrum

Virtually all applications of concurrency theory use weak behavioral equivalences, which can equate systems in spite of differing internal activity. Therefore, it matters that we can lift our approach to also account for such equivalences.

This chapter serves as a second round of preliminaries and context needed for the spectrum of weak equivalences. Some things are more complicated in the weak spectrum. For instance, we will be discussing eight weak forms of bisimilarity.

At its heart, this chapter aims to find a modal spectrum characterization, where HML grammar and pricing are designed in such a way that we can apply the spectroscopy approach in the following Chapter 7. The top element of the weak spectrum will be the logic of stability-respecting branching bisimilarity.

This is where the thesis arrives at “The linear time–branching time spectrum II: The semantics of sequential systems with silent moves” (van Glabbeek, 1993), already featured in Figure 1.1 of the introduction. We will reframe a big chunk of it to fit our modal framework in Figure 6.5. In particular, we try to be much more restricted in the use of special modalities than the presentation of van Glabbeek (1993).

Idea 6.1: Taking a sublogic to weaken HML

We can use a subset of Hennessy–Milner logic to characterize most interesting weak equivalences.

Section 6.1 provides some preliminaries and defines the \mathsf{HML} subset \mathsf{HML}_{\mathsf{SRBB}}, which will correspond to the notion of stability-respecting branching bisimilarity. Section 6.2 illustrates the use of some of the weak notions through small case studies from compiler verification and concurrency theory. In Section 6.3, we unfold the hierarchy of modal characterizations for the weak spectrum.

Related publications.   This chapter is based on parts of the draft “Deciding all behavioral equivalences at once II: The silent-step spectrum” (Bisping & Jansen, 2025) and of “Characterizing contrasimilarity through games, modal logic, and complexity” (Bisping & Montanari, 2024). For a fuller presentation of the spectrum of weak equivalences itself, van Glabbeek (1993) is the authoritative work. A gentler introduction to key concepts is provided by Sangiorgi (2012).

6.1 Weak Equivalences in General

For practical problems, the equivalences we have discussed so far usually are too strong. They notice where in a process the internal action \tau happens, that is: \mathsf{a} \nsim_\mathrm{} \tau\ldotp\! \mathsf{a} \nsim_\mathrm{} \tau\ldotp\! \tau\ldotp\! \mathsf{a} \nsim_\mathrm{} \tau\ldotp\!\mathsf{a}\ldotp\! \tau \nsim_\mathrm{} \mathsf{a}\ldotp\! \tau For real-world models, we want equivalences to disregard such kinds of internal behavior as “silent” when comparing processes, such that: \mathsf{a} \sim_\mathrm{} \tau\ldotp\! \mathsf{a} \sim_\mathrm{} \tau\ldotp\! \tau\ldotp\! \mathsf{a} \sim_\mathrm{} \tau\ldotp\!\mathsf{a}\ldotp\! \tau \sim_\mathrm{} \mathsf{a}\ldotp\! \tau Equivalences with this feature are called weak, alluding to the fact that they are less distinctive than the “strong” equivalences that treat \tau like any other action.

Figure 6.1 shows the (strong-bisimulation-minimal) transition system of the example processes we would like to equate in weak equivalences.

Figure 6.1: Processes that we would like to equate in weak equivalences (blue groups).

The basic principle is that weak equivalences should maintain that some internal behavior happening before or after a visible action does not make a difference from the point of view of an observer. But this idea leads into a lot of fine points.

6.1.1 Silent Transitions

To help us with our abstractions of weak activity, we use some additional notation:

Definition 6.1 (Transition systems with internal activity) For a transition system \mathcal{S}=(\mathcal{P},\mathit{Act},\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}) with an internal action \tau \in \mathit{Act}, we call \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}-transitions “silent” and define the following special transition relations plus HML modalities, where \mathit{Act}_👁\mathrel{≔}\mathit{Act}\mathbin{\backslash}\{\tau\} denotes “visible” actions:

Internal transition relation

p \mathrel{\twoheadrightarrow}p' iff p \mathrel{\smash{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}}^*} p', where \mathrel{\smash{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}}^*} is the reflexive transitive closure of silent steps.¹

inductive LTS.LTS_Tau.silent_reachable

The internal modality \langle \varepsilon \rangle\varphi has p \in \llbracket \langle \varepsilon \rangle\varphi \rrbracket iff there is p' \in \llbracket \varphi \rrbracket with p \mathrel{\twoheadrightarrow}p'.

Soft transition relation

p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{(\alpha)}$}}} p' iff p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\alpha}$}}} p', or if \alpha = \tau and p = p'.²

abbreviation LTS.LTS_Tau.soft_step

We accompany it by the soft observation modality ( \alpha ) \varphi with p \in \llbracket ( \alpha )\varphi \rrbracket iff there is p' \in \llbracket \varphi \rrbracket with p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{(\alpha)}$}}} p'.

Weak word steps

p \xtwoheadrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\vec w}$}}} p' for \vec w = (w_1 w_2 \dots w_n) \in \mathit{Act}_👁^* iff there is a path with p_i \mathrel{\twoheadrightarrow}\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{w_{i+1}}$}}} p_{i+1} for each 0 \leq i < n such that p_0 = p and p_n \mathrel{\twoheadrightarrow}p'.

Stable state

A state p is called stable iff p \overset{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}{\nrightarrow}.³

abbreviation LTS.LTS_Tau.stable_state

In HML, we can use \neg\langle \tau \rangle\top to express stabilization.

Divergent state

A state p is called divergent iff it allows an infinite sequence of \tau-transitions, p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}^\omega.

Again, we implicitly lift the relations to sets of states, that is, for instance, P \mathrel{\twoheadrightarrow}P' (with P, P' \subseteq \mathcal{P}) iff P' = \{ p' \in \mathcal{P}\mid \exists p \in P \ldotp p \mathrel{\twoheadrightarrow}p'\}.

In upcoming definitions and facts, we use the convention that \alpha continues to stand for elements of \mathit{Act}, while a comes from \mathit{Act}_👁= \mathit{Act}\mathbin{\backslash}\{\tau\}.

Example 6.1 (Weak steps) In Figure 6.1, the state \tau\ldotp\!\tau\ldotp\!\mathsf{a} allows the following weak steps:

• Soft \tau-transitions to itself and its immediate successor: \tau\ldotp\!\tau\ldotp\!\mathsf{a} \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{(\tau)}$}}} \tau\ldotp\!\tau\ldotp\!\mathsf{a} and \tau\ldotp\!\tau\ldotp\!\mathsf{a} \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{(\tau)}$}}} \tau\ldotp\!\mathsf{a}. (But \tau\ldotp\!\tau\ldotp\!\mathsf{a} \overset{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}{\nrightarrow} \tau\ldotp\!\tau\ldotp\!\mathsf{a}!)
• The internal transition \tau\ldotp\!\tau\ldotp\!\mathsf{a} \mathrel{\twoheadrightarrow}\mathsf{a}. (On top of the internal transitions due to {\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{(\tau)}$}}}} \subseteq {\mathrel{\twoheadrightarrow}}.)
• The weak word transition \tau\ldotp\!\tau\ldotp\!\mathsf{a} \xtwoheadrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\mathsf{a}}$}}} \mathbf{0}.
• Starting in \mathsf{a}, all kinds of \mathsf{a}-steps coincide: \mathsf{a} \xtwoheadrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\mathsf{a}}$}}} \mathbf{0} and \mathsf{a} \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{(\mathsf{a})}$}}} \mathbf{0} just as \mathsf{a} \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\mathsf{a}}$}}} \mathbf{0}.

\mathsf{a}, \mathsf{a}\ldotp\! \tau and \mathbf{0} are stable. No state is divergent.

Remark 6.1 (Just notation). Note that the notation for \mathsf{HML} operators \langle \varepsilon \rangle\dots and ( \alpha )\dots introduced in Definition 6.1 does not affect the expressiveness of HML. To see why, assume notation for disjunction \bigvee_{i \in I} \psi_i \mathrel{≔}\neg\textstyle\bigwedge_{i \in I} \neg\psi_i, and for n-time application of an operator. Then, \llbracket \langle \varepsilon \rangle\varphi \rrbracket = \llbracket \bigvee_{n \in \mathbb{N}} \langle \tau \rangle^n \varphi \rrbracket. Also, \llbracket ( \tau )\varphi \rrbracket = \llbracket \bigvee\{\varphi, \langle \tau \rangle\varphi\} \rrbracket and \llbracket ( a )\varphi \rrbracket = \llbracket \langle a \rangle\varphi \rrbracket.

On the other hand, note that our infinitary HML cannot express proper divergence p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}^\omega on infinitary systems. This would demand an “observation of infinite depth.” This clashes with the well-foundedness, which is implied by the recursive grammar of Definition 2.11. On systems with finite branching degree, however, the possibility of unbounded \tau-trees and infinite \tau-chains coincides, and divergence can be captured modally by \textstyle\bigwedge_{n \in \mathbb{N}} \langle \tau \rangle^n.

6.1.2 Weak Traces and Weak Bisimulation

It is quite straightforward how to lift traces from the strong setting of Definition 2.4 and Definition 2.5 to the weak setting: Allow internal \mathrel{\twoheadrightarrow}-behavior in between.

Definition 6.2 (Weak traces, preorder, and equivalence) The set of weak traces of a state \mathsf{WeakTraces}(p) \subseteq \mathit{Act}_👁^* is defined as \vec w \in \mathsf{WeakTraces}(p) iff there is p' such that p \xtwoheadrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\vec w}$}}} p'.⁴⁵

abbreviation LTS.LTS_Tau.weak_traces

⁵  The Isabelle theory has a slightly different definition that also allows \taus in the trace words, which do not necessarily stand for proper \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}-steps.

definition LTS.LTS_Tau.weakly_trace_preordered

Two states are weakly trace-preordered, p \preceq_\mathrm{WT} q, if \mathsf{WeakTraces}(p) ⊆ \mathsf{WeakTraces}(q).⁶ As before, if both directions are maintained, the states are called weakly trace-equivalent, p \sim_\mathrm{WT} q.

The blue groups of states in Figure 6.1 are weakly trace equivalent. Moreover, they also are related by the stronger notions of weak bisimulation and simulation.

Definition 6.3 (Weak simulation, preorder and equivalences) A relation, \mathcal{R} ⊆ \mathcal{P}× \mathcal{P}, is called a weak simulation if, for each (p, q) ∈ \mathcal{R},

• if p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{a}$}}} p' with a ∈ \mathit{Act}_👁, there is a q' with q \mathrel{\twoheadrightarrow}\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{a}$}}}\mathrel{\twoheadrightarrow}q' and (p', q') ∈ \mathcal{R}; and
• if p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau }$}}}p', there is a q' with q \mathrel{\twoheadrightarrow}q' and (p', q') ∈ \mathcal{R}.

Weak simulation preorder, weak simulation equivalence and weak bisimilarity follow analogously to Definition 2.7:

• p is weakly simulated by q, p \preceq_\mathrm{WS} q, iff there is a weak simulation \mathcal{R} with (p, q) ∈ \mathcal{R}.
• p is weakly similar to q, p \sim_\mathrm{WS} q, iff p \preceq_\mathrm{WS} q and q \preceq_\mathrm{WS} p.
• p is weakly bisimilar to q, p \sim_\mathrm{\mathcal{O}^{}_{\mathrm{WB}}} q, iff there is a symmetric weak simulation \mathcal{R} (i.e. \mathcal{R} = \mathcal{R}^{-1}) with (p, q) ∈ \mathcal{R}.

All three weak equivalences maintain that the small example processes of the introduction to Section 6.1 are equal.

Example 6.2 (Weakly simulated philosophers) For the processes of Example 2.1 (repeated in Figure 6.2), the weak traces would be \mathsf{WeakTraces}(\mathsf{P}) = \{\texttt{()}, \mathsf{a}, \mathsf{b}\} = \mathsf{WeakTraces}(\mathsf{Q}). Consequently, \mathsf{P} and \mathsf{Q} are weakly trace-equivalent, \mathsf{P} \sim_\mathrm{WT} \mathsf{Q}.

In Example 2.6, we have observed that the two processes are not (strongly) similar because \mathsf{Q} \not\preceq_\mathrm{S} \mathsf{P} due to \langle τ \rangle\textstyle\bigwedge \{\langle \mathsf{a} \rangle, \langle \mathsf{b} \rangle\}. Due to the weakening, however, there is a weak simulation for this direction, namely: \{(\mathsf{Q}, \mathsf{P}), (\mathsf{q_{ab}}, \mathsf{P}), (\mathsf{q_1}, \mathsf{p_1}), (\mathsf{q_2}, \mathsf{p_2})\}. Therefore, \mathsf{P} \sim_\mathrm{WS} \mathsf{Q}! A mutual weak simulation \mathcal{R}_{\mathsf{PQ}} to justify this is drawn in dashed blue in Figure 6.2.

Figure 6.2: A mutual weak simulation on the original philosopher example.

However, \mathsf{P} and \mathsf{Q} are not weakly bisimilar. The reason is that the left process can weakly \mathrel{\twoheadrightarrow}-transition to a position where \mathsf{b} is impossible, even if we would allow for some more internal \mathrel{\twoheadrightarrow}-behavior in between. In HML, this difference could be expressed by \langle \varepsilon \rangle\neg\langle \varepsilon \rangle\langle \mathsf{b} \rangle—we will turn to modal characterizations soon.

Definition 6.4 (Abstractions) We say that a weak notion of equivalence \mathrm{W}N abstracts a strong notion N iff {\preceq_{\mathrm{W}N}} = {\preceq_{N}} for all transition systems without \tau-transitions.

By this nomenclature, weak trace preorder, weak simulation preorder, and weak bisimilarity are abstractions of their strong counterparts from Chapter 2. But, as we will see in the next sections, there might be multiple abstractions of the same strong notion.

6.1.3 HML of Stability-Respecting Branching Bisimilarity

As noted in Remark 6.1, our HML notation for weak observations does not affect expressiveness—thus it still characterizes strong bisimilarity by Theorem 2.1. To characterize weak equivalences, we have to select appropriate subsets. We will use the following sublogic that, naturally, must be designed to correspond to the strongest weak notion we will be interested in.

Definition 6.5 (Branching Hennessy–Milner logic) We define stability-respecting branching Hennessy–Milner modal logic, \mathsf{HML}_{\mathsf{SRBB}}, over an alphabet of actions \mathit{Act} by the following context-free grammar starting with \varphi:⁷ \begin{array}{rllr} \varphi {} :≔ {} & \langle \varepsilon \rangle\chi & & \text{“delayed observation”} \\ | \quad & \textstyle\bigwedge \{\psi, \psi, ...\} & & \text{“immediate conjunction”} \\ \chi {} :≔ {} & \langle a \rangle\varphi & \text{with } a \in \mathit{Act}_👁& \text{“observation”} \\ | \quad & \textstyle\bigwedge \{\psi, \psi, ... \} & & \text{“standard conjunction”} \\ | \quad & \textstyle\bigwedge \{\neg\langle \tau \rangle\top, \psi, \psi, ...\} & & \text{“stable conjunction”} \\ | \quad & \textstyle\bigwedge \{( \alpha )\varphi, \psi, \psi, ...\} & \text{with } \alpha \in \mathit{Act}& \text{“branching conjunction”} \\ \psi {} :≔ {} & \neg\langle \varepsilon \rangle\chi \mid \langle \varepsilon \rangle\chi & & \text{“negative / positive conjuncts”} \end{array} We consider the semantics of \mathsf{HML}_{\mathsf{SRBB}} to be given by Definition 2.12 and Definition 6.1.

datatype HML_SRBB.hml_srbb

The name already alludes to \mathsf{HML}_{\mathsf{SRBB}} as a whole characterizing stability-respecting branching bisimilarity, which is a comparably strong abstraction of bisimilarity, a “strong weak bisimilarity,” so to speak.

Definition 6.6 (Stability) We call a relation \mathcal{R} stability-respecting iff, for each (p,q) \in \mathcal{R} with p \overset{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}{\nrightarrow}, there is some q' with q \mathrel{\twoheadrightarrow}q' \overset{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}{\nrightarrow} and (p, q') \in \mathcal{R}.⁸

definition LTS.LTS_Tau.stability_respecting

Definition 6.7 (Branching bisimilarity) A symmetric relation \mathcal{R} is a branching bisimulation if, for all (p,q) \in \mathcal{R}, a step p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\alpha}$}}} p' implies (1) \alpha = \tau and (p', q) \in \mathcal{R}, or (2) q \mathrel{\twoheadrightarrow}q' \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\alpha}$}}} q'' for some q' and q'' with (p, q') \in \mathcal{R} and (p', q'') \in \mathcal{R}.⁹

definition Branching_Bisimilarity.LTS_Tau.branching_simulation

If there is a stability-respecting branching bisimulation \mathcal{R}_{BB^{sr}} with (p_0, q_0) \in \mathcal{R}_{BB^{sr}}, then p_0 and q_0 are stability-respecting branching bisimilar.

The power of Definition 6.5 to distinguish mirrors exactly the power of Definition 6.7 to equate:

Theorem 6.1 (\mathsf{HML}_{\mathsf{SRBB}} Hennessy–Milner theorem) \mathsf{HML}_{\mathsf{SRBB}} characterizes stability-respecting branching bisimilarity, that is, there is a stability-respecting branching bisimulation \mathcal{R} with (p,q) \in \mathcal{R} precisely if there is no formula \varphi \in \mathsf{HML}_{\mathsf{SRBB}} with p \in \llbracket \varphi \rrbracket and q \notin \llbracket \varphi \rrbracket.¹⁰

lemma Branching_Bisimilarity.LTS_Tau.sr_branching_bisim_is_hmlsrbb

The paper proof in Bisping & Jansen (2025) proceeds quite similarly to other Hennessy–Milner theorems, as showcased in Theorem 2.1.

The example process groups of Figure 6.1 are stability-respecting branching bisimilar, as desired. But branching bisimilarity is more distinctive than weak bisimilarity:

Example 6.3 (The strength of branching) Compare \mathsf{P_{ab}} \mathrel{≔}\mathsf{a} +\tau\ldotp\! \mathsf{b} +\mathsf{b} and a subgraph-variant \mathsf{P}_{\mathsf{a}\tau\mathsf{b}} \mathrel{≔}\mathsf{a} +\tau\ldotp\! \mathsf{b}, where the \mathsf{b} is only possible after committing to its branch. The processes are not branching bisimilar as \langle \varepsilon \rangle\textstyle\bigwedge \{( \mathsf{b} ), \langle \varepsilon \rangle\langle \mathsf{a} \rangle\} distinguishes them. Intuitively, the formula expresses that, right at the moment when \mathsf{b} can happen, \mathsf{a} is still (weakly) possible.

But the processes are weakly bisimilar, as weak bisimilarity does not care about branching due to \tau-steps that can also be achieved by visible actions. A formal argument would be that \mathrm{id}_{\mathcal{P}} \cup \{(\mathsf{P_{ab}}, \mathsf{P}_{\mathsf{a}\tau\mathsf{b}}), (\mathsf{P}_{\mathsf{a}\tau\mathsf{b}}, \mathsf{P_{ab}})\} is a symmetric weak simulation.

Remark 6.2 (An equivalence indeed). It is a popular anecdote among those who know branching bisimilarity that, originally, a trivial proof of transitivity was “assumed,” but turned out not to exist. Six years after branching bisimilarity’s inception, “Branching bisimilarity is an equivalence indeed!” by Basten (1996) closed the gap with a proof that is surprisingly complex.

In our setting, the transitivity is an immediate corollary of having a modal characterization (Theorem 6.1).¹¹ This is one of the perks of modal characterizations, indeed (cf. Section 2.3.3).

lemma Branching_Bisimilarity.LTS_Tau.sr_branching_bisimulated_transitive

6.2 Case Studies—and the Need for Other Weak Equivalences

In the world of weak equivalences, many things are a little more complicated than in the strong spectrum. We have already observed that bisimulation equivalence can be abstracted to branching bisimulation and weak bisimulation.

In this section, we use two minimal case study examples to see how one can arrive at even more abstractions of bisimulation and of failure equivalence.

Next chapter’s Section 7.2 will pick up on the examples to test that the spectroscopy algorithm can indeed simplify a researcher’s life.

6.2.1 Parallelizing Compilers—and Contrasimulation

Most of computer speed up in the last two decades has been due to parallelization of computation. Compilers will usually drift and parallelize sequential commands of a program. The claim behind such optimizations is that the communication behavior of the program stays the same.¹² So, naturally, the original program and the optimized program should be equivalent with respect to some notion of equivalence.

¹²  In other regards, the program obviously differs. It is the intention to change aspects such as performance!

Bell (2014) ventures to prove that certain parallelizations of loops during compilation are sound. This runs into the problem that weak bisimilarity is too strong for this use case. The following example (adapted from Bell, 2013) shows why.

Example 6.4 (Parallelized execution) Consider the following sequential program \mathsf{P_{Seq}}, which computes x (with possible values A and B), prints a header (output:) and then the computed value:

Figure 6.3: Transition systems representing \mathsf{P_{Seq}} and \mathsf{P_{Para}}.

x = compute_A_or_B()
print("output:")
print(x)

A parallelization would find that the rendering of the header “output:” is independent of the computation of x and can thus be parallelized to \mathsf{P_{Para}}:

x = compute_A_or_B() || print("output:")
print(x)

The || connector is supposed to mean a parallel execution of commands that synchronizes the branches at the end. In real-world programming languages, this would happen through spawning and joining subprocesses, future objects, or async segments.

Figure 6.3 shows the transition systems of the two programs. The \tau-steps mark internal computation or synchronization. In particular, compute_A_or_B turns into a \tau-step. The action \mathsf{printO} stands for print("output:") announcing the coming output, and \mathsf{printA} and \mathsf{printB} are the values of x that are actually produced by print(x).

Clearly, \mathsf{P_{Seq}} and \mathsf{P_{Para}} have the same weak traces. But they do not weakly simulate each other: \mathsf{P_{Para}} can perform a \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\mathsf{printO}}$}}}-transition, immediately after which \mathsf{printA} and \mathsf{printB} are weakly possible at \mathsf{p_{ab}}. The sequential \mathsf{P_{Seq}} has no such states.

Bell (2013) proposes “eventual bisimilarity” as a one-off bisimulation-like notion to equate \mathsf{P_{Seq}} and \mathsf{P_{Para}}. In Bisping & Montanari (2024), we discuss how two more standard notions from the original spectrum neatly equate the processes: Stable bisimilarity and contrasimilarity.

Definition 6.8 (Stable bisimilarity) A stable bisimulation is a relation \mathcal{R} where, for all (p,q) \in \mathcal{R} with \vec w \in \mathit{Act}_👁 and p \xtwoheadrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\vec w}$}}} p', there is a q' with q \xtwoheadrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\vec w}$}}} q', and, in case p' is stable, moreover q' \overset{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}{\nrightarrow} and (p', q') \in \mathcal{R} \cap \mathcal{R}^{-1}. The stable bisimilarity \sim_\mathrm{SB} is defined as in Definition 6.3.

On the programs of Example 6.4, there is a stable bisimulation, connecting \mathsf{P_{Seq}} and \mathsf{P_{Para}} as well as the stable states with matching positions. Intuitively, stable bisimilarity is allowed to “skip” intermediate states that would break the bisimulation—such as \mathsf{p_{ab}} in our example.

As we argue in Bisping & Montanari (2024), stable bisimilarity, in many ways, is better understood not as a stable variant of bisimilarity, but of contrasimilarity:

Definition 6.9 (Contrasimilarity) A contrasimulation is a relation \mathcal{R} where, for all (p,q) \in \mathcal{R} with \vec w \in \mathit{Act}_👁 and p \xtwoheadrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\vec w}$}}} p', there is a q' with q \xtwoheadrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\vec w}$}}} q' and (q', p') \in \mathcal{R}.¹³ The contrasimulation preorder \preceq_\mathrm{C} and contrasimilarity \sim_\mathrm{C} are defined as in Definition 6.3.

¹³ Note that p' and q' swap sides in the consequent!

Contrasimilarity allows local asymmetry in matching internal transitions. A witness relation for Example 6.4 would also include (\mathsf{p_a}, \mathsf{p_{ab}}) and (\mathsf{p_b}, \mathsf{p_{ab}}). The intuition is that contrasimulation preorder allows states to slightly get ahead of their counterparts—\mathsf{p_a} is more committed than \mathsf{p_{ab}}—as long as the latter can catch up silently.

Contrasimilarity and stable bisimilarity, both are at the weak end of abstractions of bisimilarity, “weakest” bisimilarities, one could say. We discuss them and their characterizations in great detail in Bisping & Montanari (2024).

Contrasimilarity and stable bisimilarity are nice for proofs as they have coinductive characterizations. They also are more well-behaved than Bell’s “eventual bisimilarity,” which fails to be an equivalence if the transition system has divergent states (cf. Bell, 2014, Section 3.3).

As we will establish in Section 7.2.1, contrasimilarity and stable bisimilarity indeed are the finest equivalences from the standard spectrum to equate the sequential and the parallel program.

Remark 6.3 (Half a definition of stable bisimilarity). Sangiorgi (2012, Section 6.5) gives the following, simpler definition for stable bisimulation:¹⁴

¹⁴ Quote adapted to the notation of the present thesis.

A process relation \mathcal{R} is a stable bisimulation if, whenever (p,q) \in \mathcal{R}, for all \vec w we have:

• for all p' with p \xtwoheadrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\vec w}$}}} p' and p' is stable, there is q' such that q \xtwoheadrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\vec w}$}}} q' and (p', q') \in \mathcal{R},

and the converse on the actions from q.

Sangiorgi notes that the induced stable bisimilarity relation would not be transitive on transition systems with divergences. But the situation is even more severe!

Defined like this, stable bisimilarity would not even imply weak trace equivalence. Consider the processes \mathsf{A} and \mathsf{B} in the margin. As all their non-empty word transitions end in instable states, the variant from Sangiorgi (2012) ignores their differences altogether.

“Our” stable bisimilarity of Definition 6.8, however, does not suffer from this defect, for it demands matching of all word transitions. Our relational Definition 6.8 is informed by the upcoming modal characterizations of Section 6.3 (and of van Glabbeek (1993) and Bisping & Montanari (2024)). As discussed in Section 2.3.3, it is trivial to ensure that modally characterized relations are transitive and refine trace preorder. Such are the perks of modal characterizations!

6.2.2 Abstraction as Congruence—and Stable Failures

For trace-like equivalences, there commonly appear two kinds of abstractions in the literature: Ones where negation and conjunctive observations are only possible when processes have stabilized, that is, exhausted their possibilities of internal behavior, and ones where stability plays no role. We will illustrate these options using modal characterizations of stable and weak failure equivalence, abstracting Definition 3.2:

Definition 6.10 (Weak failure preorder and equivalence) Let weak failure preorder and equivalence be defined by the weak failure observations \mathcal{O}^{}_{\mathrm{WF}} produced by φ^\mathrm{WF} in the following grammar, and stable failure preorder and equivalence, by the products of φ^\mathrm{SF}. φ^\mathrm{WF} \;::=\; \langle \varepsilon \rangle\langle a \rangle φ^\mathrm{WF} \; \;\mid\;\; \langle \varepsilon \rangle\textstyle\bigwedge_{i \in I} \neg\langle \varepsilon \rangle\langle a_i \rangle\top φ^\mathrm{SF} \;::=\; \langle \varepsilon \rangle\langle a \rangle φ^\mathrm{SF} \; \;\mid\;\; \top \; \;\mid\;\; \langle \varepsilon \rangle\textstyle\bigwedge_{i \in I} \neg\langle α_i \rangle\top \text{ where } 0 \in I \land α_0=\tau

Weak failures are obtained by intermitting \langle \varepsilon \rangle-observations in between the steps. In comparison to the strong modal characterization of Definition 3.3, this just means prepending productions (and negated actions) by \langle \varepsilon \rangle.

Stable failures demand a \neg\langle \tau \rangle-conjunct in the conjunctions of refused actions. In one respect, this increases expressivity, as the possibility to stabilize into a state where p \overset{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}{\nrightarrow} becomes observable. In another respect, one loses the option to see failures in instable parts of the transition system. In particular, if all states of a transition system are divergent, stable failure preorder degenerates to weak trace preorder.

Often, weak and stable failures will coincide. For instance, philosopher process \mathsf{P} is distinguished from \mathsf{Q} by weak failure \langle \varepsilon \rangle\textstyle\bigwedge \{\neg\langle \varepsilon \rangle\langle \mathsf{a} \rangle\} and by stable failure \langle \varepsilon \rangle\textstyle\bigwedge \{\neg\langle \tau \rangle, \neg\langle \mathsf{a} \rangle\} alike. For the other direction, \mathsf{Q} is preordered to \mathsf{P} with respect to both, weak and stable failures.

But in general, weak and stable failure equivalence are incomparable. The following example to highlight their differences is due to van Glabbeek:

Example 6.5 (Congruence on \tau-abstraction) Figure 6.4 presents transition systems of four processes, given through their initial states: \mathsf{P}_e makes a nondeterministic choice \mathsf{op} between \mathsf{a} and \mathsf{b}, performing arbitrarily many \mathsf{idle}-actions in between. \mathsf{P}_\ell does the same but can change the choice while idling. \mathsf{P}^\tau_e and \mathsf{P}^\tau_\ell are variants of the two obtained by renaming \mathsf{idle} into \tau-actions. Many process algebras have an operator to perform such an abstraction of a process, for instance, hide in mCRL2 (Groote & Mousavi, 2014) or hiding “\mathbin{\backslash}” in CSP (Hoare, 1985).

Figure 6.4: A pair of processes \mathsf{P}_e and \mathsf{P}_\ell together with versions \mathsf{P}^\tau_e and \mathsf{P}^\tau_\ell of the two where \mathsf{idle} has been abstracted into internal \tau-behavior.

\mathsf{P}_e and \mathsf{P}_\ell allow the same weak failure and stable failure observations and are thus equivalent. For the abstracted variants, \mathsf{P}^\tau_e is distinguished from \mathsf{P}^\tau_\ell by the weak failure \langle \varepsilon \rangle\langle \mathsf{op} \rangle\langle \varepsilon \rangle\textstyle\bigwedge \{\neg\langle \varepsilon \rangle\langle \mathsf{b} \rangle\}, as \mathsf{b} becomes weakly impossible at \mathsf{A}^\tau_e but not at \mathsf{A}^\tau_\ell. Due to the \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}-loops, this difference is not expressible as a stable failure. Consequently, \mathsf{P}^\tau_e and \mathsf{P}^\tau_\ell are stable-failure-equivalent.

The example highlights one way in which weak failures might be stronger than stable failures. For most process algebras, weak failures are too strong in the following sense: Weak failures cannot be a congruence for hiding operators, as witnessed by Example 6.5!

Therefore, the standard models of CSP following Brookes et al. (1984) have used stable failures for their semantics. Van Glabbeek (1993) only includes variants of stable failures in his weak spectrum, disregarding weak failures. Other authors such as Gazda et al. (2020) work with weak failures. Therefore, our spectrum in Section 6.3 will treat both. Weak failures will be located in the part below weak bisimilarity; stable failures in that below stable bisimilarity.

Remark 6.4 (More on congruences). In general, congruence properties are harder to obtain in the weak spectrum. A classic example would be weak bisimilarity, not forming a congruence with respect to the choice operator +, because \mathsf{a} \sim_\mathrm{\mathcal{O}^{}_{\mathrm{WB}}} \tau\ldotp\!\mathsf{a}, but \mathsf{a} +\mathsf{b} \nsim_\mathrm{WB} \tau\ldotp\!\mathsf{a} +\mathsf{b}. We will not go into the particularities around this and point to Sangiorgi (2012, Section 4.4) for how to obtain a congruence through rooted weak bisimilarity.

6.3 Expressing the Weak Spectrum by Quantities

We can capture the weak spectrum in a lattice of vectors like the strong one in Chapter 3. But we need a few more dimensions.

6.3.1 Syntactic Expressiveness

We adapt the notions of Section 3.2.2 for the weak spectrum to distinguish the new kinds of conjunctions that appear in \mathsf{HML}_{\mathsf{SRBB}} of Definition 6.5:

1. Modal depth of observations (\langle a \rangle, ( \alpha )).
2. New: Nesting depth of branching conjunctions (with one ( \alpha )-observation conjunct, not starting with \langle \varepsilon \rangle).
3. New: Nesting depth of unstable conjunctions (that do not enforce stability by a \neg\langle \tau \rangle \top-conjunct).
4. New: Nesting depth of stable conjunctions (that do enforce stability by a \neg\langle \tau \rangle \top-conjunct).
5. Nesting depth of immediate conjunctions (that are not preceded by \langle \varepsilon \rangle).
6. Maximal modal depth of positive conjuncts in conjunctions.¹⁵
7. Maximal modal depth of negative conjuncts in conjunctions.
8. Nesting depth of negations.

¹⁵  To simplify matters, we drop the distinction of two kinds of positive conjunct depths of Section 3.2.2. Section 7.3.2 will hint how to add stable revivals back in.

To formalize our weak spectrum, we need to fix the observation languages \mathcal{O}^{\mathsf{weak}}_{N}. This time, we will do this by directly providing an expressiveness pricing metric.

Definition 6.11 (Weak notions) We define the weak notions of observability using vectors of extended naturals \mathbf{N}^\mathsf{weak} ≔ \mathbb{N}_\infty^8, ordered by pointwise comparison of vector components.

We capture the family of weak observation languages \mathcal{O}^{\mathsf{weak}}_{N \in \mathbf{N}^\mathsf{weak}} by providing an expressiveness price function \mathsf{expr}^{\mathsf{weak}} \colon \mathsf{HML}_{\mathsf{SRBB}}\rightarrow \mathbf{N}^\mathsf{weak} with \mathcal{O}^{\mathsf{weak}}_{N} = \{ \varphi \mid \mathsf{expr}^{\mathsf{weak}}(\varphi) \leq N\}.¹⁶ It is defined in mutual recursion with \mathsf{expr}^{\varepsilon} and \mathsf{expr}^{\wedge} as follows—if multiple rules apply, pick the first one: \begin{array}{rl} \mathsf{expr}^{\mathsf{weak}}\left(\top\right) \mathrel{≔} \mathsf{expr}^{\varepsilon}\left(\top\right) & \hspace{-2mm} \mathrel{≔} \mathbf{0} \\ \textstyle\mathsf{expr}^{\mathsf{weak}}\left(\langle \varepsilon \rangle\chi\right) & \hspace{-2mm} \mathrel{≔} \textstyle\mathsf{expr}^{\varepsilon}\left(\chi\right) \\ \textstyle\mathsf{expr}^{\mathsf{weak}}\left(\textstyle\bigwedge \Psi\right) & \hspace{-2mm} \mathrel{≔} \hat{\mathbf{e}}_{5} + \textstyle\mathsf{expr}^{\varepsilon}\left(\textstyle\bigwedge \Psi\right) \\ \mathsf{expr}^{\varepsilon}\left(\langle a \rangle\varphi\right) & \hspace{-2mm} \mathrel{≔} \hat{\mathbf{e}}_{1} + \mathsf{expr}^{\mathsf{weak}}\left(\varphi\right) \\ \textstyle\mathsf{expr}^{\varepsilon}\left(\textstyle\bigwedge \Psi\right) & \hspace{-2mm} \mathrel{≔} \sup\;\{ \mathsf{expr}^{\wedge}\left(\psi\right) \mid \psi \in \Psi \} + \begin{cases} \hat{\mathbf{e}}_{4} & \text{if } \neg\langle \tau \rangle\top\in \Psi\\ \hat{\mathbf{e}}_{2} + \hat{\mathbf{e}}_{3} & \text{if there is } ( \alpha )\varphi \in \Psi \\ \hat{\mathbf{e}}_{3} & \text{otherwise} \end{cases} \\ \mathsf{expr}^{\wedge}\left(\neg\langle \tau \rangle\top\right) & \hspace{-2mm} \mathrel{≔} (0,0,0,0,0,0,0,1) \\ \mathsf{expr}^{\wedge}\left(\neg\varphi\right) & \hspace{-2mm} \mathrel{≔} \sup\;\{ \hat{\mathbf{e}}_{8} + \mathsf{expr}^{\mathsf{weak}}\left(\varphi\right),\quad (0,0,0,0,0,0,\left(\mathsf{expr}^{\mathsf{weak}}\left(\varphi\right)\right)_1,0) \} \\ \mathsf{expr}^{\wedge}\left(( \alpha )\varphi\right) & \hspace{-2mm} \mathrel{≔} \sup\;\{ \hat{\mathbf{e}}_{1} + \mathsf{expr}^{\mathsf{weak}}\left(\varphi\right),\quad (0,0,0,0,0,1 + \left(\mathsf{expr}^{\mathsf{weak}}\left(\varphi\right)\right)_1,0,0) \} \\ \mathsf{expr}^{\wedge}\left(\varphi\right) & \hspace{-2mm} \mathrel{≔} \sup\;\{ \hphantom{\hat{\mathbf{e}}_{8} + {}} \mathsf{expr}^{\mathsf{weak}}\left(\varphi\right),\quad (0,0,0,0,0,\left(\mathsf{expr}^{\mathsf{weak}}\left(\varphi\right)\right)_1,0,0) \} \end{array}

fun Expressiveness_Price.expressiveness_price

6.3.2 Weak Spectrum

Using Definition 6.11, we can give coordinates to the common notions of weak behavioral equivalence in Figure 6.5. In this subsection, we take a deeper look into the observation languages characterized by the coordinates and argue for the correctness of exemplary cases.

Figure 6.5: Hierarchy of weak behavioral equivalences/preorders, by equivalence notion coordinates.

Linear-time notions.   Let us first see how trace-like notions are handled in our spectrum.

Lemma 6.1 (Characterization of weak trace equivalence) The subset \mathcal{O}^{\mathsf{weak}}_{\mathrm{WT}} = \mathcal{O}^{\mathsf{weak}}_{(\infty,0,0,0,0,0,0,0)} \subseteq \mathsf{HML}_{\mathsf{SRBB}} can be given by the following grammar: \begin{align*} \varphi_\mathrm{WT} \;::=\;& \; \langle \varepsilon \rangle\langle a \rangle\varphi_\mathrm{WT} \;\mid\;\langle \varepsilon \rangle\top \;\mid\;\top \qquad \text{with $a \in \mathit{Act}_👁$.} \end{align*} There is a formula \varphi \in \mathcal{O}^{\mathsf{weak}}_{\mathrm{WT}} distinguishing p from q precisely if p is not weakly trace-preordered to q.¹⁷

lemma Weak_Traces.LTS_Tau.trace_equals_trace_to_formula

Proof. For a word \vec{w} = a_1 \dots a_n \in \mathit{Act}_👁^*, the formula \langle \varepsilon \rangle\langle a_1 \rangle\dots\langle \varepsilon \rangle\langle a_n \rangle\langle \varepsilon \rangle\top\in \mathcal{O}^{\mathsf{weak}}_{\mathrm{WT}} is true for a state p precisely if there is a p' such that p \xtwoheadrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\vec{w}}$}}} p', that is, if \vec{w} \in \mathsf{WeakTraces}(p). As \mathsf{WeakTraces}(p) = \mathsf{WeakTraces}(q) for states p and q precisely if \mathsf{WeakTraces}(p) \cap \mathit{Act}_👁^* = \mathsf{WeakTraces}(q) \cap \mathit{Act}_👁^*, this completes the proof.

The whole list of logics for weak linear-time notions can be found in Figure 6.6. The interesting points are highlighted in \textcolor{RoyalBlue}{\textrm{blue}}. Productions that could be left out without affecting distinctiveness are set in \textcolor{gray}{\textrm{gray}}.

Figure 6.6: Grammars induced by coordinates for weak linear-time notions of equivalence.

The modal characterizations correspond to the ones one would expect, with some trivial ones appearing due to the language hierarchy approach.

Bisimulation-like notions.   For the abstractions of bisimilarity in Figure 6.7, some more interesting things happen.

Figure 6.7: Grammars induced by coordinates for weak bisimulation-like notions of equivalence.

Bisping & Jansen (2025, Section 3.3) prove in detail, for each of our abstractions of bisimilarity, that it corresponds to its respective relational characterization. The Isabelle theory (Barthel et al., 2025) features theorems for \eta-bisimilarity¹⁸ and for stability-respecting branching bisimilarity¹⁹.

theorem Eta_Bisimilarity.LTS_Tau.eta_bisim_coordinate

theorem Branching_Bisimilarity.LTS_Tau.sr_branching_bisim_coordinate

The first interesting feature of the weak hierarchy is an effect of some languages not enforcing top-level negation as observed in Bisping & Jansen (2024, Ex. 2.5).

Example 6.6 (Weak bisimulation logic) Let us contrast the logic of weak bisimulation observations \mathcal{O}^{}_{\mathrm{WB}} defined through (\infty,0,\infty,0,0,\infty,\infty,\infty) to the weak bisimulation observations \mathcal{O}^{}_{\mathrm{WB'}} from Gazda et al. (2020): \varphi_\mathsf{WB'} \;::=\;\langle \varepsilon \rangle\varphi_\mathsf{WB'} \;\mid\;\langle \varepsilon \rangle\langle a \rangle\langle \varepsilon \rangle\varphi_\mathsf{WB'} \;\mid\;\textstyle\bigwedge \{\varphi_\mathsf{WB'}, \varphi_\mathsf{WB'}, \ldots\} \;\mid\;\neg\varphi_\mathsf{WB'} Our \mathcal{O}^{}_{\mathrm{WB}} allows a few formulas that \mathcal{O}^{}_{\mathrm{WB'}} lacks, e.g. \langle \varepsilon \rangle\langle \mathsf{a} \rangle\langle \varepsilon \rangle\langle \mathsf{a} \rangle\langle \varepsilon \rangle\top. This does not add expressiveness as \mathcal{O}^{}_{\mathrm{WB'}} has \langle \varepsilon \rangle\langle \mathsf{a} \rangle\langle \varepsilon \rangle\langle \varepsilon \rangle\langle \mathsf{a} \rangle\langle \varepsilon \rangle\top and \llbracket \langle \varepsilon \rangle\langle \varepsilon \rangle\varphi \rrbracket = \llbracket \langle \varepsilon \rangle\varphi \rrbracket.

For the other direction, there is a bigger difference due to \mathcal{O}^{}_{\mathrm{WB'}} allowing more freedom in the placement of conjunction and negation. In particular, it permits top-level conjunctions and negated conjunctions without \langle \varepsilon \rangle in between. But these features do not add distinctive power. \mathcal{O}^{}_{\mathrm{WB'}} also allows top-level negation, and this adds distinctive power to the preorders, effectively turning them into equivalence relations. We do not enforce this and thus our \mathord{\preceq_{\mathcal{O}^{}_{\mathrm{WB}}}} \neq \mathord{\sim_\mathrm{\mathcal{O}^{}_{\mathrm{WB}}}}; for instance, \tau\ldotp\! \mathsf{a} \preceq_{\mathcal{O}^{}_{\mathrm{WB}}} \tau +\tau\ldotp\! \mathsf{a}, but \tau +\tau\ldotp\! \mathsf{a} \not\preceq_{\mathcal{O}^{}_{\mathrm{WB}}} \tau\ldotp\! \mathsf{a} due to \langle \varepsilon \rangle\textstyle\bigwedge \{\neg\langle \varepsilon \rangle\langle \mathsf{a} \rangle\top\}. However, as a distinction by \neg\varphi in one direction implies one by \varphi in the other, we know that this difference is ironed out once we consider the equivalence \sim_\mathrm{\mathcal{O}^{}_{\mathrm{WB}}}.

Another point of interest is the relationship of weak bisimilarity, contrasimilarity and stable bisimilarity. Remark 3.3 on synonymous coordinates has mentioned that (\infty, \infty, 0, 0, \infty, \infty) \in \mathbf{N}^\mathsf{strong}, which disallows positive conjuncts, already characterizes strong bisimilarity. Translating this coordinate to the weak spectrum, we hit (\infty, 0, \infty, 0, 0, 0, \infty, \infty) or (\infty, 0, 0, \infty, 0, 0, \infty, \infty) \in \mathbf{N}^\mathsf{weak}. In the weak spectrum, these coordinates correspond to differing notions! The first of the two is exactly the coordinate of contrasimilarity. The other one describes observations that are equally expressive to stable bisimulation observations, because stabilized positive conjuncts can be normalized away by ²⁰ \llbracket \langle \varepsilon \rangle\textstyle\bigwedge \{\neg\langle \tau \rangle, {\color{RoyalBlue}\varphi_1}, \neg\varphi_2,\ldots \} \rrbracket = \llbracket \langle \varepsilon \rangle\textstyle\bigwedge \{\neg\langle \tau \rangle, {\color{Gray}\neg\langle \varepsilon \rangle\textstyle\bigwedge \{\neg\langle \tau \rangle, \neg{\color{RoyalBlue}\varphi_1}\}}, \neg\varphi_2,\ldots \} \rrbracket. In this sense, contrasimulation and stable bisimilarity are sibling notions in the same manner as weak failures and stable failures of Section 6.2.2.²¹ We use the higher coordinate (\infty, 0, 0, \infty, 0, \infty, \infty, \infty) with positive conjuncts for stable bisimulation in Figure 6.5 to underscore that stable bisimulation preorder is finer than stable simulation preorder and its variants.

theorem HML_SRBB.LTS_Tau.srbb_stable_Neg_normalizable_set

²¹  This is also the topic of Bisping & Montanari (2024, Section 7.3)

Simulation-like notions.   Figure 6.8 adds the simulation-like notions for completeness. At this point, they are not particularly interesting.

Figure 6.8: Grammars induced by coordinates for weak simulation-like notions of equivalence.

Bisping & Jansen (2025) contains proofs that the observation languages for weak simulation and \eta-simulation correspond to their relational definitions (Definition 6.3).²²

theorem Eta_Bisimilarity.LTS_Tau.eta_sim_coordinate

Remark 6.5 (Spurious conjuncts and minimality). Several of our weak grammars allow bogus trivial conjuncts. The most severe case might be the trees of ultimately empty conjunctions of \chi_\mathrm{WU^x} for contrasimulation in Figure 6.7. A natural impulse might be to somehow change the grammar to optimize these parts away, ensuring a nicer output of distinguishing formulas in the spectroscopy.

But this optimization would be premature in our context! Spectroscopy strategy formulas will never contain trivial conjuncts, by design, because those can not be distinguishing. Even more, the minimal winning budgets in the spectroscopy game will only ever lead to witness formulas that are minimal with respect to syntactic expressiveness prices. Therefore, optimizing away superfluous conjuncts in the grammars would itself be superfluous.

On the other hand, shrinking the languages would call for additional contexts, that is, non-terminals in the grammar. But more non-terminals mean additional kinds of spectroscopy game positions and moves, thus making the spectroscopy game more complex—for nothing.

6.4 Discussion

With this chapter, we have explored the space of weak behavioral equivalences in concurrency theory, focusing on their modal characterizations and relationships within the weak spectrum, following van Glabbeek (1993). This adds the preliminaries to consider their decision procedures in Chapter 7.

The power of weakness.   In examples, we have seen how weak equivalences handle internal nondeterminism due to communication in different ways. Practical scenarios, such as parallelizing compilers and process abstraction of Section 6.2, reveal the possibilities and limitations of the different design decisions behind process equivalences.

Following Idea 6.1, our modal logic characterization through \mathsf{HML}_{\mathsf{SRBB}} captures a rich weak spectrum between stability-respecting branching bisimilarity and weak trace equivalence. This adds to the rich body of work on modal characterizations of branching bisimilarity by De Nicola & Vaandrager (1995), Fokkink et al. (2019), Geuvers (2022), and Geuvers & Golov (2023).

Our spectrum, however, leaves out some classical notions such as stable failure traces and coupled simulation, which would have called for even more dimensions in the already 8-dimensional pricing metric.²³ We will return to the topic of how such notions could be included in Section 7.3.2 and 7.3.3.

²³  Especially for coupled similarity, this gap is ironic, as my research into game characterizations of equivalences has been kicked off by an interest in decision procedures for coupled similarity in Bisping & Nestmann (2019) and Bisping et al. (2020). But it would just not have been economic to add a whole new dimension for this single darling of mine.

What's next?   Logic and pricing metric are designed in such a way that readers of preceding chapters might already be able to guess how they will translate to game moves for stable and branching conjunctions in the next chapter. Call this avenue for gamification yet another perk of modal characterizations—besides the benefits of built-in transitivity and consistency that we have noticed along the way of this chapter!

Barthel, L. A., Bisping, B., Hübner, L. M., Lemke, C., Mattes, K. P. P., & Mollenkopf, L. (2025). A weak spectroscopy game to characterize behavioral equivalences [Isabelle/HOL formalization]. https://equivio.github.io/silent-step-spectroscopy/AFP/Weak_Spectroscopy.

Basten, T. (1996). Branching bisimilarity is an equivalence indeed! Information Processing Letters, 58(3), 141–147. https://doi.org/10.1016/0020-0190(96)00034-8

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

Bell, C. J. (2014). A proof theory for loop-parallelizing transformations [PhD thesis, Princeton University]. https://people.csail.mit.edu/cj/thesis/thesis.pdf

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., & 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., & 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

Brookes, S. D., Hoare, C. A. R., & Roscoe, A. W. (1984). A theory of communicating sequential processes. J. ACM, 31(3), 560–599. https://doi.org/10.1145/828.833

De Nicola, R., & Vaandrager, F. (1995). Three logics for branching bisimulation. J. ACM, 42(2), 458–487. https://doi.org/10.1145/201019.201032

Fokkink, W., van Glabbeek, R., & Luttik, B. (2019). Divide and congruence III: From decomposition of modal formulas to preservation of stability and divergence. Information and Computation, 268, 104435. https://doi.org/10.1016/j.ic.2019.104435

Gazda, M., Fokkink, W., & Massaro, V. (2020). Congruence from the operator’s point of view: Syntactic requirements on modal characterizations. Acta Informatica, 57(3–5), 329–351. https://doi.org/10.1007/s00236-019-00355-5

Geuvers, H. (2022). Apartness and distinguishing formulas in Hennessy–Milner logic. 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. 266–282). Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-15629-8_14

Geuvers, H., & Golov, A. (2023). Positive Hennessy-Milner logic for branching bisimulation. https://arxiv.org/abs/2210.07380

Groote, J. F., & Mousavi, M. R. (2014). Modelling and analysis of communicating systems. MIT Press. https://doi.org/10.7551/mitpress/9946.001.0001

Hoare, C. A. R. (1985). Communicating sequential processes. Prentice-Hall, Inc.

Sangiorgi, D. (2012). Introduction to bisimulation and coinduction. Cambridge University Press. https://doi.org/10.1017/CBO9780511777110

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