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. At the heart, we aim 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.

We will reframe a big chunk of “The Linear Time–Branching Time Spectrum II: The Semantics of Sequential Systems with Silent Movea” (Glabbeek, 1993) to fit our modal framework. In particular, we try to be much more restricted in the use of special modalities than the presentation in Glabbeek (1993).

Idea 6.1: A Weak Subset

We can use a subset of \mathsf{HML} to characterize most interesting weak equivalences.

Section 6.1 will provide some preliminaries and define the \mathsf{HML} subset, which will correspond to the notion of stability-respecting branching bisimilarity. We illustrate the use of some oft the weak notions through small examples in Section 6.2. In Section 6.3, we unfold the modal characterization for the weak spectrum.

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 we would like to equate in weak equivalences.

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

Definition 6.1 For transition systems \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 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 \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}^* p', where \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'.

Optional 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 optional step 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 p_i \mathrel{\twoheadrightarrow}\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{w_i}$}}} p_{n+1} for i < n with p_0 = p and p_n \mathrel{\twoheadrightarrow}p'.

Stable state

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

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\}.

Remark 6.1. 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 \mathsf{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 finite systems, 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 necessary 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 usual, 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 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{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.1 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.5, 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 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.

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 \mathsf{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 & \quad\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, ...\} & \quad \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 We call a \mathcal{R} stability-respecting iff, for each (p,q) \in \mathcal{R} with p \cancel{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}}, there is some q' with q \mathrel{\twoheadrightarrow}q' \cancel{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}} and (p, q') \in \mathcal{R}.⁸

definition LTS.LTS_Tau.stability_respecting

Definition 6.7 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', 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}} 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.2 Compare \mathsf{P_{ab}} \mathrel{:=}\mathsf{a} +\tau\ldotp\! \mathsf{b} +\mathsf{b} and a subgraph-variant \mathsf{P_{a\tau 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_{a\tau b}}), (\mathsf{P_{a\tau 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 the proof of its transitivity “assumed” originally does not exist. Six years after branching bisimilarity’s inception, Basten (1996) closes the gap by 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 Equivalences

6.2.1 Parallelizing Compiler Optimization

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 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 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.3 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. The action \mathsf{ao} stands for print("output:") announcing the coming output, and \mathsf{A} and \mathsf{B} 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{ao}}$}}}-transition, immediately after which \mathsf{A} and \mathsf{B} are weakly possible at \mathsf{p_{ab}}. The sequential \mathsf{P_{Seq}} has no such states.

Bell (2013) proposes “eventual bisimilarity” as a new 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 Bisimulation) 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', p') \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.3, 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 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 (Contrasimulation) 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.3 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 mor 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 coninductive 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.3.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. 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 [sic!] from q.

Sangiorgi notes that the induced stable bisimilarity relation would not be transitive on transition sysstems 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 alltogether.

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 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 Congruence Properties of Abstraction

Example on equiv.io

Ae = (idle.Ae + a)
Be = (idle.Be + b)
Al = (idle.Bl + idle.Al + a)
Bl = (idle.Al + idle.Bl + b)

Pe = (op.Ae + op.Be)
Pl = (op.Al + op.Bl)
@compareSilent Pe, Pl

Pte = Pe \csp {idle}
Ptl = Pl \csp {idle}
@compareSilent Pte, Ptl

@comment "Pe/Pl should be (unstable&stable) readiness equivalent"
@comment "Pte/Ptl are stable, but not unstable (!) failure (and readiness) equivalent"

Pe(x=200, y=10)
Pl(x=500, y=10)
Pte(x=200, y=450)
Ptl(x=500, y=450)
"0"(x=365, y=304)
"0 \csp {idle}"(x=411, y=786)

… Closing hint: congruence even messier in the weak spectrum, e.g. weak bisim not congruence for +.

6.3 Expressing the Weak Spectrum with Quantities

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:

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 two kinds of positive conjunct depths.

Definition 6.10 (Weak Spectrum) 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) & \mathrel{:=} \mathbf{0} \\ \textstyle\mathsf{expr}^{\mathsf{weak}}\left(\langle \varepsilon \rangle\chi\right) & \mathrel{:=} \textstyle\mathsf{expr}^{\varepsilon}\left(\chi\right) \\ \textstyle\mathsf{expr}^{\mathsf{weak}}\left(\textstyle\bigwedge \Psi\right) & \mathrel{:=} \hat{\mathbf{e}}_{5} + \textstyle\mathsf{expr}^{\varepsilon}\left(\textstyle\bigwedge \Psi\right) \\ \mathsf{expr}^{\varepsilon}\left(\langle a \rangle\varphi\right) & \mathrel{:=} \hat{\mathbf{e}}_{1} + \mathsf{expr}^{\mathsf{weak}}\left(\varphi\right) \\ \textstyle\mathsf{expr}^{\varepsilon}\left(\textstyle\bigwedge \Psi\right) & \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) & \mathrel{:=} (0,0,0,0,0,0,0,1) \\ \mathsf{expr}^{\wedge}\left(\neg\varphi\right) & \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) & \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) & \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.10, we can give coordinates to the common notions of the weak behavioral equivalence in Figure 6.4.

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

Lemma 6.1 The subset \mathcal{O}^{\mathsf{weak}}_{\mathrm{T}} = \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{T} \;::=\;& \; \langle \varepsilon \rangle\langle a \rangle\varphi_\mathrm{T} \;\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}}_{T} distinguishing p from q precisely if p is not 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}}_{T} 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 weak linear-time notions can be found in Figure 6.5. The interesting points are highlighted in \textcolor{RoyalBlue}{blue}. Productions that could be left out without affecting distinctiveness are set in \textcolor{gray}{gray}.

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

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

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

TODO: Remark on Stable Bisimilarity equaling stable contrasimilarity in expressiveness; Coordinate choice to show that stable bisim implies e.g. stable ready sim.

6.4 Discussion

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. (2025). Deciding all behavioral equivalences at once II: The silent-step spectrum. 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

Glabbeek, R. J. van. (1993). The linear time–branching time spectrum II: The semantics of sequential systems with silent moves; extended abstract. In E. Best (Ed.), CONCUR’93 (Vol. 715, pp. 66–81). Springer. https://doi.org/10.1007/3-540-57208-2_6

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