7  Spectroscopy for the Weak Spectrum

By applying the ideas we have explored so far, we can derive a game for the weak spectrum of Chapter 6. The key new idea here is how to encode internal activity “\langle \varepsilon \rangle\dots” in game moves:

Idea 7.1: Weakening the attacker

In the game, the places where \langle \varepsilon \rangle appears in \mathsf{HML}_{\mathsf{SRBB}}-formulas mean that the attacker must allow the maximization of defender’s Q-options with respect to internal \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}-steps.

The basic schematics of how the weak game solves the spectroscopy problem are exactly the same as for the strong spectroscopy in Figure 5.1.

What is different this time around is that we have a full Isabelle/HOL formalization of game correctness in Section 7.1, and that we can apply the algorithm to real case studies that involve internal behavior in Section 7.2. In Section 7.3, we discuss how to use our method to check even more weak equivalences.

7.1 The Weak Spectroscopy Game

On the next pages, we upgrade the spectroscopy game of Section 5.1 to account for the weak spectrum of Chapter 6.

7.1.1 The Game

The weak spectroscopy game, in many respects, is just like the spectroscopy games we have already discussed: The attacker, trying to distinguish states, has different paths that move closely along the productions of the \mathsf{HML}_{\mathsf{SRBB}}-grammar (Definition 6.5). But this time, there are four different kinds of non-empty conjunctions! This makes the following schematic depiction in Figure 7.1 already look quite entangled.

Figure 7.1: Schematic weak spectroscopy game of Definition 7.1.

Formally, the game rules are defined as follows:

Definition 7.1 (Weak spectroscopy game) For a system \mathcal{S}=(\mathcal{P},\mathit{Act},\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}), the 8-dimensional weak spectroscopy game \mathcal{G}_{\nabla}^{\mathcal{S}}=(G,G_{{\mathrm{d}}},\mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}},w) consists of

  • attacker (immediate) positions \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \in G_{\mathrm{a}},
  • new: attacker delayed positions \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} \in G_{\mathrm{a}},
  • attacker conjunct positions \smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}} \in G_{\mathrm{a}},
  • new: attacker branching positions \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\eta}} \in G_{\mathrm{d}},
  • defender conjunction positions \smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} \in G_{\mathrm{d}},
  • new: defender stable conjunction positions \smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}} \in G_{\mathrm{d}},
  • new: defender branching positions \smash{\color{gray}(}p,\alpha,p',Q,Q_\alpha\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle\eta}} \in G_{\mathrm{d}},

where p, q \in \mathcal{P} and Q, Q_\alpha \in 2^{\mathcal{P}}, and the following sixteen kinds of moves.1

Moves to allow internal behavior “\langle \varepsilon \rangle\dots” between observations: \begin{array}{rrcll} \textit{delay} & \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;0,0,0,0,0,0,0,0\;}}{}\!\!›}} & \smash{\color{gray}[}p,Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} & \text{if $Q \mathrel{\twoheadrightarrow}Q'$,} \\ \textit{procrastination} & \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;0,0,0,0,0,0,0,0\;}}{}\!\!›}} & \smash{\color{gray}[}p',Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} & \text{if $p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}} p'$, $p \neq p'$,} \end{array} moves to represent the known \mathsf{HML} constructs “\langle a \rangle\dots”, “\textstyle\bigwedge \{\dots\}”, and “\neg\dots” in the now two contexts: \begin{array}{rrcll} \textit{observation} & \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;-1,0,0,0,0,0,0,0\;}}{}\!\!›}} & \smash{\color{gray}[}p',Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} & \text{if $p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{a}$}}} p'\!$, $Q \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{a}$}}} Q'\!$, $a \neq \tau$,} \\ \textit{finishing} & \smash{\color{gray}[}p,\varnothing\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;0,0,0,0,0,0,0,0\;}}{}\!\!›}} & \smash{\color{gray}(}p,\varnothing\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}, & \\ \textit{immediate conj.} & \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;0,0,0,0,-1,0,0,0\;}}{}\!\!›}} & \smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} & \text{if $Q \neq \varnothing$,} \\ \textit{late conj.} & \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;0,0,0,0,0,0,0,0\;}}{}\!\!›}} & \smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}, & \\ \textit{conj. answer} & \smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;0,0,-1,0,0,0,0,0\;}}{}\!\!›}} & \smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}} & \text{if $q \in Q$,} \\ \textit{positive conjunct} & \smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\mathtt{min}_{\{\!1,6\!\}},0,0,0,0,0,0,0\;}}{}\!\!›}} & \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} & \text{if $\{q\} \mathrel{\twoheadrightarrow}Q$,} \\ \textit{negative conjunct} & \smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\mathtt{min}_{\{\!1,7\!\}},0,0,0,0,0,0,-1\;}}{}\!\!›}} & \smash{\color{gray}[}q,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} & \text{if $\{p\} \mathrel{\twoheadrightarrow}Q$ and $p \neq q$,} \end{array} moves to encode stable conjunctions “\textstyle\bigwedge \{\neg\langle \tau \rangle\top, \psi, \psi, ...\}”: \begin{array}{rrcll} \textit{stable conj.}\vphantom{I^{I^I}} & \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;0,0,0,0,0,0,0,0\;}}{}\!\!›}} & \smash{\color{gray}(}p,Q'\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}} & \text{if } Q' = \{ q \in Q \mid q \overset{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}{\nrightarrow}\}, p \overset{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}{\nrightarrow}, \\ \textit{stable conj. answer} & \smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;0,0,0,-1,0,0,0,0\;}}{}\!\!›}} & \smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}} & \text{if $q \in Q$,} \\ \textit{stable finishing} & \smash{\color{gray}(}p,\varnothing\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;0,0,0,-1,0,0,0,-1\;}}{}\!\!›}} & \smash{\color{gray}(}p,\varnothing\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}, \end{array}

and moves to encode branching conjunctions “\textstyle\bigwedge \{( \alpha )\varphi, \psi, \psi, ...\}”: \begin{array}{rrcll} \textit{branching conj.}\vphantom{I^{I^I}} & \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;0,0,0,0,0,0,0,0\;}}{}\!\!›}} & \smash{\color{gray}(}p,\alpha,p'\!,Q \mathbin{\backslash}Q_\alpha,Q_\alpha\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle\eta}} & \text{if $p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{(\alpha)}$}}} p'\!$, $Q_\alpha \subseteq Q$,} \\ \textit{branch. answer} & \smash{\color{gray}(}p,\alpha,p'\!,Q,Q_\alpha\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle\eta}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;0,-1,-1,0,0,0,0,0\;}}{}\!\!›}} & \smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}} & \text{if $q \in Q$,} \\ \textit{branch. observation} & \smash{\color{gray}(}p,\alpha,p'\!,Q,Q_\alpha\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle\eta}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\mathtt{min}_{\{\!1,6\!\}},-1,-1,0,0,0,0,0\;}}{}\!\!›}} & \smash{\color{gray}[}p',Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\eta}} & \text{with $Q_\alpha \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{(\alpha)}$}}} Q'$,} \\ \textit{branch. accounting} & \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\eta}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;-1,0,0,0,0,0,0,0\;}}{}\!\!›}} & \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}. \end{array} Intuitively, the attacker is heavily weakened in the weak spectroscopy game due to the requirement to pass delay-moves in order to formulate observation attacks. Following Idea 7.1, these moves grow the right-hand-sets, which increases defender options. At the same time, there are several new tactical possibilities for the attacker that correspond to the special weak conjunctions, as can be seen in the following example.

Example 7.1 (Failures of philosophy) For our standard philosopher system of Figure 2.3, Example 6.2 has determined that \mathsf{P} and \mathsf{Q} are not weakly bisimilar, but weakly similar (and thus weakly trace-equivalent).

The stable failure \langle \varepsilon \rangle\textstyle\bigwedge \{\neg\langle \varepsilon \rangle\langle \mathsf{a} \rangle\} discussed in Section 6.2.2 corresponds to the following game moves, which need budget (1,0,0,1,0,0,1,1): \begin{array}{rlc} \smash{\color{gray}[}\mathsf{P}, \{\mathsf{Q}\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \; \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\;\mathbf{0}\;\;}}{}\!\!›}} & \smash{\color{gray}[}\mathsf{P}, \{\mathsf{Q}, \mathsf{q_{ab}}\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\epsilon}} & \text{(delay)} \\ \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\;\mathbf{0}\;\;}}{}\!\!›}} & \smash{\color{gray}[}\mathsf{p_b}, \{\mathsf{Q}, \mathsf{q_{ab}}\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\epsilon}} & \text{(procrastination)} \\ \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\;\mathbf{0}\;\;}}{}\!\!›}} & \smash{\color{gray}(}\mathsf{p_b}, \{\mathsf{q_{ab}}\}\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} & \text{(stable conj.)} \\ \mathrel{\smash{›\!\!\frac{\scriptstyle{\;-\hat{\mathbf{e}}_{4}\;}}{}\!\!›}} & \smash{\color{gray}[}\mathsf{p_b}, \mathsf{q_{ab}}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}} & \text{(stable conj. answer)} \\ \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\mathtt{min}_{\{\!1,7\!\}},0,0,0,0,0,0,-1\;}}{}\!\!›}} & \smash{\color{gray}[}\mathsf{q_{ab}}, \{\mathsf{p_b}\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\epsilon}} & \text{(negative conjunct)} \\ \mathrel{\smash{›\!\!\frac{\scriptstyle{\;-\hat{\mathbf{e}}_{1}\;}}{}\!\!›}} & \smash{\color{gray}[}\mathsf{q_1}, \varnothing\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} & \text{($\mathsf{a}$-observation)} \\ \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\;\mathbf{0}\;\;}}{}\!\!›}} & \smash{\color{gray}(}\mathsf{q_1}, \varnothing\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} \quad \mathrel{\smash{{›/\!\!\!\!\frac{\scriptstyle{\;\enspace\;}}{\;}\!\!›}}} & \text{(finishing)} \end{array} A similar sequence of moves works for weak failures. For weak simulation, we know that \mathsf{P} is strongly simulated by \mathsf{Q}, which transfers to the weak game in the sense that we also cannot find a weak simulation distinction in this direction. The attacker must pass through a negative-conjunct move to exploit that \mathsf{P} resolves the choice more quickly than \mathsf{Q}.

For the other direction, Example 6.2 has established that weak simulation, \mathsf{Q} \preceq_\mathrm{WS} \mathsf{P}, holds as well. But how does this go together with Example 5.3 mentioning that strong simulation is disproved by the \mathsf{HML} formula \langle \tau \rangle\textstyle\bigwedge \{\langle \mathsf{a} \rangle, \langle \mathsf{b} \rangle\}? In the weak game, there are no strong \tau-observation moves. The closest weak equivalent is to just use delay/procrastination, corresponding to the \mathsf{HML}_{\mathsf{SRBB}} formula {\color{RoyalBlue}\langle \varepsilon \rangle}\textstyle\bigwedge \{\langle \varepsilon \rangle\langle \mathsf{a} \rangle, \langle \varepsilon \rangle\langle \mathsf{b} \rangle\}. But this fails to be a distinction in the weak game as the defender can just stay at \mathsf{P} \in \{\mathsf{P}, \mathsf{p_a}, \mathsf{p_b}\}.

However, other forms of abstracted simulation can be used to force the defender out of \mathsf{P} without negations:

  • \eta-simulation allows branching conjunction moves: \smash{\color{gray}[}\mathsf{q_{ab}}, \{\mathsf{P}, \mathsf{p_a}, \mathsf{p_b}\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\epsilon}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\;\mathbf{0}\;\;}}{}\!\!›}} \smash{\color{gray}(}\mathsf{q_{ab}}, \mathsf{a}, \mathsf{q_1}, \{\mathsf{p_a}\}, \{\mathsf{P}, \mathsf{p_b}\}\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle\eta}}. After this, \mathsf{p_a} is discharged through a positive conjunct \mathsf{b}-observation, possible from \mathsf{q_{ab}}; and the \{\mathsf{P}, \mathsf{p_b}\}-option directly ends in \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}\smash{\color{gray}[}\mathsf{q_1}, \varnothing\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\eta}}\mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}\mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}\smash{\color{gray}(}\mathsf{q_1}, \varnothing\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}\mathrel{\smash{{›/\!\!\!\!\frac{\scriptstyle{\;\enspace\;}}{\;}\!\!›}}}, as neither \mathsf{P} nor \mathsf{p_b} allow immediate \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\mathsf{a}}$}}}-steps. These moves cost (1,1,1,0,0,1,0,0) and correspond to the distinguishing formula \langle \varepsilon \rangle\textstyle\bigwedge \{( \mathsf{a} ), \langle \varepsilon \rangle\langle \mathsf{b} \rangle\}.
  • Stable simulation allows stable conjunction moves: \smash{\color{gray}[}\mathsf{q_{ab}}, \{\mathsf{P}, \mathsf{p_a}, \mathsf{p_b}\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\epsilon}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\;\mathbf{0}\;\;}}{}\!\!›}} \smash{\color{gray}(}\mathsf{q_{ab}}, \{\cancel{\mathsf{P}}, \mathsf{p_a}, \mathsf{p_b}\}\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}}. After this, \mathsf{q_{ab}} can out-maneuver \mathsf{p_a} through positive conjunct \mathsf{b}-observation, and \mathsf{p_b} through positive conjunct \mathsf{a}-observation. The moves need (1,0,1,1,0,1,0,1) energy and match the distinguishing formula \langle \varepsilon \rangle\textstyle\bigwedge \{\neg\langle \tau \rangle, \langle \varepsilon \rangle\langle \mathsf{a} \rangle, \langle \varepsilon \rangle\langle \mathsf{b} \rangle\}.

In summary, the game moves show that \mathsf{P} and \mathsf{Q} are weakly similar, but no notion besides or above in the weak spectrum (Figure 6.5) can hold because weak failures, stable failures, \eta-simulation, and stable simulation can be disproven by attacker moves for at least one direction. This reasoning, of course, depends on the weak spectroscopy game being correct …

7.1.2 Correctness

Establishing correctness now proceeds mostly as we are used to from Section 4.2.3 and 5.1.2. This subsection limits itself to citing the lemma heads and the inductive predicates used in the full proofs of Bisping & Jansen (2025).

The following facts moreover have been fully formalized in Isabelle/HOL, which will be the topic of the following Section 7.1.3.

Definition 7.2 (Strategy formulas for \mathcal{G}_{\nabla}) The set of strategy formulas for a game position g and a budget e, \mathsf{Strat}_{\nabla}(g, e), in the context of a weak spectroscopy game \mathcal{G}_{\nabla}^{\mathcal{S}} is defined inductively by the rules in Figure 7.2.2

\mathrm{delay}\;\dfrac{\begin{matrix} \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u\;}}{}\!\!›}} \smash{\color{gray}[}p,Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} \quad e' = \mathsf{upd}(u, e) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}[}p,Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}}) \quad \chi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}}, e') \end{matrix}}{ \langle \varepsilon \rangle\chi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e) }\hphantom{\mathrm{delay}} \mathrm{procrastination}\;\dfrac{\begin{matrix} \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u\;}}{}\!\!›}} \smash{\color{gray}[}p',Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} \quad e' = \mathsf{upd}(u, e) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}[}p',Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}}) \quad \chi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p',Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}}, e') \end{matrix}}{ \chi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}}, e) }\hphantom{\mathrm{procrastination}} \mathrm{observation}\;\dfrac{\begin{matrix} \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u\;}}{}\!\!›}} \smash{\color{gray}[}p',Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \quad e' = \mathsf{upd}(u, e) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}[}p',Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}) \\ p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{a}$}}} p' \quad Q \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{a}$}}} Q' \quad \varphi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p',Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e') \end{matrix}}{ \langle a \rangle\varphi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}}, e) }\hphantom{\mathrm{observation}} \mathrm{immediate\, conj.}\;\dfrac{\begin{matrix} \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u\;}}{}\!\!›}} \smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} \quad e' = \mathsf{upd}(u, e) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}) \quad \varphi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}, e') \end{matrix}}{ \varphi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e) }\hphantom{\mathrm{immediate\, conj.}} \mathrm{late\, conj.}\;\dfrac{\begin{matrix} \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u\;}}{}\!\!›}} \smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} \quad e' = \mathsf{upd}(u, e) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}) \quad \chi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}, e') \end{matrix}}{ \chi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}}, e) }\hphantom{\mathrm{late\, conj.}} \mathrm{conj.\, answer}\;\dfrac{\begin{matrix} \smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u_q\;}}{}\!\!›}} \smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}} \\ \forall q \in Q \ldotp \; e_q = \mathsf{upd}(u_q, e) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}}) \; \land \; \psi_q \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}}, e_q) \end{matrix}}{ \textstyle\bigwedge \{ \psi_q \mid q \in Q\} \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}, e) }\hphantom{\mathrm{conj.\, answer}} \mathrm{positive\, conjunct}\;\dfrac{\begin{matrix} \smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u\;}}{}\!\!›}} \smash{\color{gray}[}p,Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} \quad e' = \mathsf{upd}(u, e) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}[}p,Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}}) \quad \chi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}}, e') \end{matrix}}{ \langle \varepsilon \rangle\chi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}}, e) }\hphantom{\mathrm{positive\, conjunct}} \mathrm{negative\, conjunct}\;\dfrac{\begin{matrix} \smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u\;}}{}\!\!›}} \smash{\color{gray}[}q,P'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} \quad e' = \mathsf{upd}(u, e) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}[}q,P'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}}) \quad \chi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}q,P'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}}, e') \end{matrix}}{ \neg\langle \varepsilon \rangle\chi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}}, e) }\hphantom{\mathrm{negative\, conjunct}} \mathrm{stable\, conj.}\;\dfrac{\begin{matrix} \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u\;}}{}\!\!›}} \smash{\color{gray}(}p,Q'\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}} \quad e' = \mathsf{upd}(u, e) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}(}p,Q'\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}}) \quad \chi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}(}p,Q'\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}}, e') \end{matrix}}{ \chi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}}, e) }\hphantom{\mathrm{stable\, conj.}} \mathrm{stable\, conj.\, answer}\;\dfrac{\begin{matrix} \smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u_q\;}}{}\!\!›}} \smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}} \quad Q \neq \varnothing \\ \forall q \in Q \ldotp \; e_q = \mathsf{upd}(u_q, e) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}}) \; \land \; \psi_q \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}}, e_q) \end{matrix}}{ \textstyle\bigwedge \left(\{\neg\langle \tau \rangle\top\} \cup \{ \psi_q \mid q \in Q \}\right) \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}}, e) }\hphantom{\mathrm{stable\, conj.\, answer}} \mathrm{stable\, finishing}\;\dfrac{\begin{matrix} \smash{\color{gray}(}p,\varnothing\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u\;}}{}\!\!›}} \smash{\color{gray}(}p,\varnothing\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} \quad e' = \mathsf{upd}(u, e) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}(}p,\varnothing\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}) \end{matrix}}{ \textstyle\bigwedge \{\neg\langle \tau \rangle\top\} \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}}, e) }\hphantom{\mathrm{stable\, finishing}} \mathrm{branching\, conj.}\;\dfrac{\begin{matrix} \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u\;}}{}\!\!›}} \smash{\color{gray}(}p,\alpha,p',Q',Q_\alpha\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle\eta}} \quad e' = \mathsf{upd}(u, e) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}(}p,\alpha,p',Q',Q_\alpha\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle\eta}}) \\ \chi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}(}p,\alpha,p',Q',Q_\alpha\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle\eta}}, e') \end{matrix}}{ \chi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}}, e) }\hphantom{\mathrm{branching\, conj.}} \mathrm{branch.\, answer}\;\dfrac{\begin{matrix} g_\mathrm{d} = \smash{\color{gray}(}p,\alpha,p',Q,Q_\alpha\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle\eta}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u_\alpha\;}}{}\!\!›}} \smash{\color{gray}[}p',Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\eta}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u'_\alpha\;}}{}\!\!›}} \smash{\color{gray}[}p',Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \\ e_\alpha = \mathsf{upd}(u'_\alpha, \mathsf{upd}(u_\alpha, e)) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}[}p',Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}) \quad \varphi_\alpha \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p',Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e_\alpha)\\ \forall q \in Q \ldotp \; g_\mathrm{d} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u_q\;}}{}\!\!›}} \smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}} \; \land \; e_q = \mathsf{upd}(u_q, e) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}}) \; \land \; \psi_q \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}}, e_q) \end{matrix}}{ \textstyle\bigwedge \left(\{( \alpha ) \varphi_\alpha \} \cup \{ \psi_q \mid q \in Q \}\right) \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}(}p,\alpha,p',Q,Q_\alpha\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle\eta}}, e) }\hphantom{\mathrm{branch.\, answer}}

Figure 7.2: Strategy formulas for the weak spectroscopy.

Attacker winning budgets can be translated into strategy formulas of matching price, as illustrated in Example 7.1.

Lemma 7.1 (Distinction formulatability) If e \in \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\nabla}}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}), then there is \varphi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e) with \mathsf{expr}^{\mathsf{weak}}(\varphi) \leq e.3

Proof (Approach). By induction over game positions g and energies e according to the inductive characterization of attacker winning budgets Proposition 4.3 and with respect to the following property:

  1. If e \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}), then there is \varphi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e) with \mathsf{expr}^{\mathsf{weak}}(\varphi) \leq e;
  2. If e \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}}), then there is \chi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}}, e) with \mathsf{expr}^{\varepsilon}(\chi) \leq e;
  3. If e \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}}), then there is \psi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}}, e) with \mathsf{expr}^{\land}(\psi) \leq e;
  4. If e \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}), then there is \textstyle\bigwedge \Psi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}, e) with \mathsf{expr}^{\varepsilon}(\textstyle\bigwedge \Psi) \leq e;
  5. If e \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}}), then there is \textstyle\bigwedge \left(\{\neg\langle \tau \rangle\top\} \cup \Psi\right) \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}}, e) with \mathsf{expr}^{\varepsilon}(\textstyle\bigwedge \left(\{\neg\langle \tau \rangle\top\} \cup \Psi\right)) \leq e;
  6. If e \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}(}p,\alpha,p',Q \mathbin{\backslash}Q_\alpha,Q_\alpha\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle\eta}}), then there is \textstyle\bigwedge \left(\{( \alpha )\varphi' \} \cup \Psi\right) \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}(}p,\alpha,p',Q \mathbin{\backslash}Q_\alpha,Q_\alpha\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle\eta}}, e) with \mathsf{expr}^{\varepsilon}(\textstyle\bigwedge \left(\{( \alpha )\varphi' \} \cup \Psi\right)) \leq e.

Weak strategy formulas distinguish the left state from the set of states on the right, where we lift Definition 2.13 to sets as follows:

Definition 7.3 (Distinguishes from set) We say a formula \varphi distinguishes a state p \in \mathcal{P} from a set of states Q \subseteq \mathcal{P} iff p \in \llbracket \varphi \rrbracket and Q \cap \llbracket \varphi \rrbracket = \varnothing.

Lemma 7.2 (Distinction soundness) If \varphi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e), then \varphi distinguishes p from Q.4

Proof (Approach). By induction over the derivation of ~\cdots \in \mathsf{Strat}_{\nabla}(g, e) according to Definition 7.2 on the following inductive property:

  1. If \varphi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e), then \varphi distinguishes p from Q;
  2. If \chi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}}, e) and Q \mathrel{\twoheadrightarrow}Q, then \langle \varepsilon \rangle\chi distinguishes p from Q;
  3. If \psi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}}, e), then \psi distinguishes p from \{ q \};
  4. If \textstyle\bigwedge \Psi \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}, e), then \textstyle\bigwedge \Psi distinguishes p from Q;
  5. If \textstyle\bigwedge \left(\{\neg\langle \tau \rangle\top\} \cup \Psi\right) \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}}, e) and p is stable, then the stable conjunction \textstyle\bigwedge \left(\{\neg\langle \tau \rangle\top\} \cup \Psi\right) distinguishes p from Q;
  6. If \textstyle\bigwedge \left(\{( \alpha )\varphi' \} \cup \Psi\right) \in \mathsf{Strat}_{\nabla}(\smash{\color{gray}(}p,\alpha,p',Q \mathbin{\backslash}Q_\alpha,Q_\alpha\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle\eta}}, e), p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{(\alpha)}$}}} p' and Q_\alpha \subseteq Q, then the branching conjunction \textstyle\bigwedge \left(\{( \alpha )\varphi' \} \cup \Psi\right) distinguishes p from Q.

Distinguishing formulas certify the existence of equally cheap ways for the attacker to win.

Lemma 7.3 (Distinction completeness) If \varphi \in \mathsf{HML}_{\mathsf{SRBB}} distinguishes p from Q, then \mathsf{expr}^{\mathsf{weak}}(\varphi) \in \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\nabla}}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}).5

Proof (Approach). By mutual structural induction on \varphi, \chi, and \psi with respect to the following claims:

  1. If \varphi \in \mathsf{HML}_{\mathsf{SRBB}} distinguishes p from Q \neq \varnothing, then \mathsf{expr}^{\mathsf{weak}}(\varphi) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}});
  2. If \chi distinguishes p from Q \neq \varnothing and Q is closed under \mathrel{\twoheadrightarrow} (that is Q \mathrel{\twoheadrightarrow}Q), then \mathsf{expr}^{\varepsilon}(\chi) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}});
  3. If \psi distinguishes p from q, then \mathsf{expr}^{\land}(\psi) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}});
  4. If \textstyle\bigwedge \Psi distinguishes p from Q \neq \varnothing, then \mathsf{expr}^{\varepsilon}(\textstyle\bigwedge \Psi) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}});
  5. If \textstyle\bigwedge \{ \neg\langle \tau \rangle\top\} \cup \Psi distinguishes p from Q \neq \varnothing and the processes in Q are stable, then \mathsf{expr}^{\varepsilon}(\textstyle\bigwedge \{ \neg\langle \tau \rangle\top\} \cup \Psi) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}(}p,Q\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}});
  6. If \textstyle\bigwedge \{ ( \alpha )\varphi' \} \cup \Psi distinguishes p from Q, then, for any p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{(\alpha)}$}}} p' \in \llbracket \varphi' \rrbracket and Q_\alpha = Q \mathbin{\backslash}\llbracket \langle \alpha \rangle\varphi' \rrbracket{}{}, \mathsf{expr}^{\varepsilon}(\textstyle\bigwedge \{ ( \alpha )\varphi'\! \} \cup \Psi) \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}(}p,\alpha,p'\!,Q \mathbin{\backslash}Q_\alpha, Q_\alpha\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle\eta}}).

Theorem 7.1 (\mathbf{N}^\mathsf{weak}-characterization) For all N \in \mathbf{N}^\mathsf{weak}, p \in \mathcal{P}, Q \in 2^{\mathcal{P}}\!, the following are equivalent:6

  • There exists a formula \varphi \in \mathsf{HML}_{\mathsf{SRBB}} with price \mathsf{expr}^{\mathsf{weak}}(\varphi) \leq N that distinguishes p from Q.
  • Attacker wins \mathcal{G}_{\nabla}^{\mathcal{S}} from \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} with energy N.

7.1.3 Isabelle/HOL Formalization

Barthel et al. (2025) formalize the correctness result for the weak spectroscopy game in the interactive proof assistant Isabelle/HOL. The preceding definitions and facts have already linked to their respective Isabelle/HOL counterparts. This subsection is devoted to providing some insights into the formalization.7 We take a tour through roughly a hundred of the most interesting lines of the 6500 line theory development.

7  For questions on the Isabelle/Isar language, consult The Isabelle/Isar reference manual (Wenzel, 2025).

8  To be precise: “Partial function” here means that it returns option-values, which might either be Some x with an output or None otherwise. All functions in higher-order logic are total.

The weak spectroscopy game (Definition 7.1) is modelled through a parametric datatype ('s, 'a) spectroscopy_position for its positions and a partial function spectroscopy_moves to determine the moves connecting them.8 The parameter types 's and 'a capture the states \mathcal{P} and actions \mathit{Act} of the transition system on which we operate.9

datatype ('s, 'a) spectroscopy_position =
  Attacker_Immediate
    (attacker_state: ‹'s›) (defender_states: ‹'s set›)
| Attacker_Delayed
    (attacker_state: ‹'s›) (defender_states: ‹'s set›)
  [...]
| Defender_Branch
    (attacker_state: ‹'s›) (attack_action: ‹'a›)
    (attacker_state_succ: ‹'s›)
    (defender_states: ‹'s set›)
    (defender_branch_states: ‹'s set›)

fun spectroscopy_moves (in LTS_Tau) ::
  ‹('s, 'a) spectroscopy_position ⇒ ('s, 'a) spectroscopy_position
    ⇒ energy update option›
where
  delay: ‹spectroscopy_moves
    (Attacker_Immediate p Q) (Attacker_Delayed p' Q')
  = (if p' = p ∧ Q ↠S Q' then id_up else None)›
| [...]

The game itself is then built as a combination of the locale for transition systems with internal actions LTS_Tau (with a transition relation step) and an energy_game locale. The latter is instantiated with the moves, a predicate spectroscopy_defender singling out defender positions, and the \leq-relation on 8-dimensional energies.10

locale weak_spectroscopy_game =
  LTS_Tau step τ
  + energy_game ‹spectroscopy_moves› ‹spectroscopy_defender› ‹(≤)›
  for step :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› (‹_ ↦_ _› [70, 70, 70] 80)
    and  τ :: 'a

Within the locale, we can establish our correctness results.

The strategy formulas \mathsf{Strat}_{\nabla} appear as three mutually inductive predicates, because the grammar of \mathsf{HML}_{\mathsf{SRBB}} (Definition 6.5) is implemented as three mutually recursive data types (one per non-terminal).11

inductive
  strategy_formula :: ‹('s, 'a) spectroscopy_position
    ⇒ energy ⇒ ('a, 's) hml_srbb ⇒ bool›
and
  strategy_formula_inner :: ‹('s, 'a) spectroscopy_position
    ⇒ energy ⇒ ('a, 's) hml_srbb_inner ⇒ bool›
and
  strategy_formula_conjunct :: ‹('s, 'a) spectroscopy_position
    ⇒ energy ⇒ ('a, 's) hml_srbb_conjunct ⇒ bool›
where
  delay: ‹strategy_formula (Attacker_Immediate p Q) e (Internal χ)›
  if ‹∃Q'. spectroscopy_moves
        (Attacker_Immediate p Q) (Attacker_Delayed p Q') = id_up
      ∧ attacker_wins e (Attacker_Delayed p Q')
      ∧ strategy_formula_inner (Attacker_Delayed p Q') e χ›
| [...]

We then reproduce the induction of Lemma 7.1 on attacker winning budgets in the following lemma. For this, the theory uses the inductive characterization of \mathsf{Win}_\mathrm{a} in Proposition 4.3 as definition for attacker_wins.12

lemma winning_budget_implies_strategy_formula:
  assumes ‹attacker_wins e g›
  shows
    ‹case g of
        Attacker_Immediate p Q ⇒
        ∃φ. strategy_formula g e φ ∧ expressiveness_price φ ≤ e
      | Attacker_Delayed p Q ⇒
        ∃χ. strategy_formula_inner g e χ ∧ expr_pr_inner χ ≤ e
      | Attacker_Conjunct p q ⇒
        ∃ψ. strategy_formula_conjunct g e ψ
          ∧ expr_pr_conjunct ψ ≤ e
      | Defender_Conj p Q ⇒
        ∃χ. strategy_formula_inner g e χ ∧ expr_pr_inner χ ≤ e
      | Defender_Stable_Conj p Q ⇒
        ∃χ. strategy_formula_inner g e χ  ∧ expr_pr_inner χ ≤ e
      | Defender_Branch p α p' Q Qa ⇒
        ∃χ. strategy_formula_inner g e χ ∧ expr_pr_inner χ ≤ e
      | Attacker_Branch p Q ⇒
        ∃φ. strategy_formula
              (Attacker_Immediate p Q) (e - E 1 0 0 0 0 0 0 0) φ
          ∧ expressiveness_price φ ≤ e - E 1 0 0 0 0 0 0 0›
  using assms
proof (induction rule: attacker_wins.induct)
  [...]

There are superficial differences due to the different medium. For instance, note that the inductive predicate in the Isabelle theory has a seventh case for Attacker_Branch / \smash{\color{gray}[}\dots\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\eta}} that does not exist in the “paper version” of Lemma 7.1. This is more natural for the “case ... of ...” formulation in the formalization, and addresses a technicality that Bisping & Jansen (2025) handle in the proof body.

The (mutual) induction on the formula structure to establish the distinctiveness of \mathsf{Strat}_{\nabla}-formulas of Lemma 7.2 begins:13

lemma strategy_formulas_distinguish:
  ‹(strategy_formula g e φ ⟶
      (case g of
        Attacker_Immediate p Q ⇒
          distinguishes_from φ p Q
      | Defender_Conj p Q ⇒
          distinguishes_from φ p Q
      | _ ⇒ True))
    ∧
    (strategy_formula_inner g e χ ⟶
      (case g of
        Attacker_Delayed p Q ⇒
          (Q ↠S Q) ⟶ distinguishes_from (Internal χ) p Q
      | Defender_Conj p Q ⇒
          hml_srbb_inner.distinguishes_from χ p Q
      | Defender_Stable_Conj p Q ⇒
          (∀q. ¬ p ↦ τ q)
          ⟶ hml_srbb_inner.distinguishes_from χ p Q
      | Defender_Branch p α p' Q Qa ⇒
          (p ↦a α p')
          ⟶ hml_srbb_inner.distinguishes_from χ p (Q∪Qa)
      | _ ⇒ True))
    ∧
    (strategy_formula_conjunct g e ψ ⟶
      (case g of
        Attacker_Conjunct p q ⇒
          hml_srbb_conj.distinguishes ψ p q
      | _ ⇒ True))›
proof (induction rule:
  strategy_formula_strategy_formula_inner_[...].induct)
  [...]

For the other direction, the following expresses distinction completeness (Lemma 7.3) that attacks exist for formulas.14

lemma distinction_implies_winning_budgets:
  assumes ‹distinguishes_from φ p Q›
  shows ‹attacker_wins (expressiveness_price φ)
                       (Attacker_Immediate p Q)›

The main theorem Theorem 7.1 combines the previous facts and the upward-closedness of attacker winning budgets win_a_upwards_closure. This is quite straightforward. The following listing reproduces it in full to convey an idea of what Isar proofs look like.15

theorem spectroscopy_game_correctness:
  shows
    ‹(∃φ. distinguishes_from φ p Q ∧ expressiveness_price φ ≤ e)
    ⟷ attacker_wins e (Attacker_Immediate p Q)›
proof
  assume
    ‹∃φ. distinguishes_from φ p Q ∧ expressiveness_price φ ≤ e›
  then obtain φ where φ_spec:
    ‹distinguishes_from φ p Q› ‹expressiveness_price φ ≤ e›
    by blast
  from distinction_implies_winning_budgets φ_spec(1) have
    ‹attacker_wins
      (expressiveness_price φ) (Attacker_Immediate p Q)› .
  thus ‹attacker_wins e (Attacker_Immediate p Q)›
    using win_a_upwards_closure φ_spec(2) by simp
next
  assume ‹attacker_wins e (Attacker_Immediate p Q)›
  with winning_budget_implies_strategy_formula have
    ‹∃φ. strategy_formula (Attacker_Immediate p Q) e φ
       ∧ expressiveness_price φ ≤ e›
    by force
  hence
    ‹∃φ. strategy_formula (Attacker_Immediate p Q) e φ
       ∧ expressiveness_price φ ≤ e›
    by blast
  thus ‹∃φ. distinguishes_from φ p Q ∧ expressiveness_price φ ≤ e›
    using strategy_formulas_distinguish by fastforce
qed

In Chapter 2, we started our journey of connecting attacker strategies and distinguishing formulas in Theorem 2.3. In retrospect, it is just a corollary of this formalized theorem.

7.1.4 Complexity

The complexity of spectroscopy using the weak game is quite comparable to the strong spectroscopy (Theorem 5.2).

Theorem 7.2 (Weak spectroscopy complexity) Given a transition system \mathcal{S}, the spectroscopy problem for the \mathbf{N}^\mathsf{weak}-spectrum can be solved by the game approach in exponential time and space with respect to the state space size \smash{|{\mathcal{P}}|}.

Proof. According to Theorem 7.1, we can solve the spectroscopy problem for the \mathbf{N}^\mathsf{weak}-spectrum by deciding the winning budgets of the weak spectroscopy game \mathcal{G}_{\nabla}^{\mathcal{S}} on \mathcal{S}=(\mathcal{P},\mathit{Act},\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}). We instantiate the winning budget complexity of Lemma 4.5 for the case d=8 with the size of \mathcal{G}_{\nabla} according to Definition 7.1.

The number of attacker positions \smash{\color{gray}[}\dots\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} (and their delayed \smash{\color{gray}[}\dots\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\varepsilon}} and branching \smash{\color{gray}[}\dots\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\eta}} variants) is bounded by \mathit{O}(\smash{|{\mathcal{P}}|} \cdot 2^{\smash{|{\mathcal{P}}|}}). The number of conjunction moves and defender conjunction positions \smash{\color{gray}(}\dots\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} is bounded by \smash{|{\mathcal{P}}|} \cdot 2^{\smash{|{\mathcal{P}}|}}, also for the stable variant \smash{\color{gray}(}\dots\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle s}}.

However, for the branching conjunction moves, we find a bound of \mathit{O}(\smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \cdot 2^{\smash{|{\mathcal{P}}|}}) per attacker delayed position (which is a slight over-approximation). Collectively, these moves reach \mathit{O}(\smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \cdot 3^{\smash{|{\mathcal{P}}|}}) defender branching positions \smash{\color{gray}(}p, \alpha, p', Q \mathbin{\backslash}Q_\alpha, Q_\alpha\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle\eta}}, due the three-coloring of states into Q \mathbin{\backslash}Q_\alpha, Q_\alpha and \mathcal{P}\mathbin{\backslash}Q.

The maximal out-degree for attacker delayed positions of \mathit{O}(\smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \cdot 2^{\smash{|{\mathcal{P}}|}}) dominates that of other positions, in particular, of defender conjunction, stable conjunction, and branching positions with \mathit{O}(\smash{|{\mathcal{P}}|}) outgoing options.

This amounts to o_{\mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}_\nabla} in \mathit{O}(\smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \cdot 2^{\smash{|{\mathcal{P}}|}}) and to \smash{|{G_{\nabla}}|} in \mathit{O}(\smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \cdot 3^{\smash{|{\mathcal{P}}|}}). Inserting the parameters in the time bounds of Lemma 4.5 yields: \begin{array}{rlccccccc} & O( & o_{\mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}} & \cdot & \smash{|{G}|}^{2 \cdot d} & \cdot & (\smash{d}^2 + \smash{|{G}|}^{d-1} \cdot d) & ) \\ = & O( & (\smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \cdot 2^{\smash{|{\mathcal{P}}|}}) & \cdot & (\smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \cdot 3^{\smash{|{\mathcal{P}}|}})^{2 \cdot 8} & \cdot & (8^2 + (\smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \cdot 3^{\smash{|{\mathcal{P}}|}})^{8-1} \cdot 8) & ) \\ = & O( & \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \cdot 2^{\smash{|{\mathcal{P}}|}} & \cdot & \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|}^{16} \cdot 3^{16\smash{|{\mathcal{P}}|}} & \cdot & \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|}^7 \cdot 3^{7\smash{|{\mathcal{P}}|}} & ) \\ ⊆ & O( & \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|}^{24} & \cdot & 3^{24\smash{|{\mathcal{P}}|}} & ). \end{array} For space complexity, we arrive at \mathit{O}( \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|}^8 \cdot 3^{8\smash{|{\mathcal{P}}|}}).

The exponential out-degree is due to branching conjunction moves. That these would need exponentially many outgoing moves seems off: These moves are for \eta- and branching bisimilarity, which are known to be at the less expensive end of equivalence problems in the spectrum (sub-cubic by Groote et al., 2017). Frutos Escrig et al.’s (2017) branching bisimulation game is polynomially-sized. Thus, a derived reachability game of the weak spectroscopy game for branching bisimilarity in the spirit of Section 5.3.1 should, too, be polynomial in size if we apply clever optimizations. Section 7.3.1 will later show how to simplify the spectroscopy game to achieve this reduction of size around branching conjunctions.

7.2 Tackling Our Case Studies

We now return to our examples from Section 6.2, and see how the spectroscopy approach can handle the two, and thus support research in concurrency theory. For this project, we will use the equiv.io CCS dialect.

7.2.1 Parallelizing Compilers

In Example 6.4, we have discussed the example of parallelizing compilation. Bell (2013) reports on the search for a fitting notion of equivalence to prove the equivalence of sequential and parallelized program, \mathsf{P_{Seq}} and \mathsf{P_{Para}}.

We model the computation of \mathsf{A} / \mathsf{B} as a parallel process Compute that outputs one of the two options (computeA/computeB). In P_Seq, the computation has to happen before the visible output action printOutput! starts, followed by the printing of the computed value, printA! or printB!. In P_Para, the printOutput! happens in parallel, and the two processes synchronize on join before continuing to print the computed value. For both processes, the synchronizing actions, that is, computeA, computeB, and join, are restricted to internal use.

Compute = computeA!Compute + computeB!Compute

P_Seq = (
    Compute 
  | computeA.printOutput!printA!
    + computeB.printOutput!printB!
) \ {computeA, computeB}

P_Para = (
    Compute
  | printOutput!join!
  | computeA.join.printA!
    + computeB.join.printB!
) \ {computeA, computeB, join}

@compareSilent P_Para, P_Seq

The statement @compareSilent P_Para, P_Seq invokes the weak spectroscopy on the pair of processes.

As a cheapest distinguishing formula of P_Para from P_Seq, the spectroscopy reports ⟨ϵ⟩⟨printOutput!⟩⟨ϵ⟩⋀{⟨ϵ⟩⟨printA!⟩⊤,⟨ϵ⟩⟨printB!⟩⊤}. This formula disproves weak simulation plus weak readiness and everything above in the weak spectrum. The minimality means that all other notions must hold. These are the equivalences of contrasimilarity and stable bisimilarity, and below.

This nicely shows that our spectroscopy algorithm allows to survey the whole spectrum of possible equivalences between such small processes in milliseconds. Such a mechanized survey would certainly have facilitated the research behind Bell (2013).

7.2.2 \tau-Abstraction and Failures

Section 6.2.2 has introduced a transition system with two states \mathsf{P}_e and \mathsf{P}_\ell that perform a nondeterministic \mathsf{op}-step. Only \mathsf{P}_\ell can correct the choice while \mathsf{idle}-ing. Though both processes are weak-failure-equivalent, their variants \mathsf{P}^\tau_e and \mathsf{P}^\tau_\ell where \mathsf{idle}-steps are relabelled to \tau-steps are not.

To reconstruct this result on equiv.io, we first have to translate the processes of Figure 6.4 to CCS. We express \mathsf{P}_e and \mathsf{P}_\ell as P_e and P_t through mutual recursion in the following model:

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

P_e = op.Ae + op.Be
P_l = op.Al + op.Bl

To implement the hiding of idle in CCS, we use a parallel process that provides unlimited idle!-actions to synchronize instead of the environment. Hence, \mathsf{P}^\tau_e and \mathsf{P}^\tau_\ell are expressed as P_te and P_tl:

Idle = idle!Idle
P_te = (P_e | Idle) \ {idle}
P_tl = (P_l | Idle) \ {idle}

We can now use the derived equivalence checkers (along the lines of Section 5.3) to establish that P_e and P_l are weak-failure-equivalent, but P_te and P_tl are not:

@check weak-failure, P_e, P_l
  > "States are equivalent."
@check weak-failure, P_te, P_tl
  > "States are inversely preordered (only from right to left)."

How does this influence research in concurrency theory? Gazda et al. (2020, Corollary 9) claim that weak failure equivalence would be a congruence for the hiding operator. In light of our finding, this cannot be right.16

16  The bug in the otherwise intriguing paper (Gazda et al., 2020) is that the modal logic of weak failures is not closed under adding of weak observation sequences at \langle \varepsilon \rangle-operators: \langle \varepsilon \rangle\langle \mathsf{a} \rangle\langle \varepsilon \rangle\textstyle\bigwedge \{\neg\langle \varepsilon \rangle\langle \mathsf{a} \rangle\} \in \mathcal{O}^{}_{\mathrm{WF}}, but \langle \varepsilon \rangle\langle \mathsf{a} \rangle\langle \varepsilon \rangle\textstyle\bigwedge \{\neg{\color{RoyalBlue}\langle \varepsilon \rangle\langle \mathsf{a} \rangle}\langle \varepsilon \rangle\langle \mathsf{a} \rangle\} is too strong for weak failure equivalence. Their requirement (ABS) together with the definition of \mathcal{T}^{-1}_H would prescribe that the greatest logic to characterize weak failures contains both, for hiding to be a congruence. Their Corollary 9 assumes in error that this kind of pumping were sound for weak failures.

We can go even further and decide all weak equivalences of our spectrum:

@compareSilent P_e, P_l
  > "Equated by:
     weak-readiness
     stable-readiness"
@compareSilent P_te, P_tl
  > "Equated by:
     stable-bisimulation"

This provides us with the general answer that notions can only be congruences for hiding if they are not below weak/stable readiness, or if they moreover fall into the hierarchy below stable bisimulation.

7.3 Variants

At this point in the thesis, it hopefully has become quite apparent how our approach can be varied with respect to game moves and HML hierarchies in order to add more equivalences or to cut resolution.

This section mainly presents two tricks that are used in the implementation of equiv.io: Section 7.3.1 shows how to get rid of the subset construction in branching conjunctions. Section 7.3.2 presents a modification to add stable revivals, stable failure traces and stable ready traces as notions. In Section 7.3.3, we close with some hints how even more nuances in weak equivalences could be covered.

7.3.1 Optimizing Branching Conjunctions

Bisping & Jansen (2025) show how to reduce the out-degree o_{\mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}} of the weak spectroscopy game to be linear. For this, we reformulate the branching conjunction part of the game to be closer to the operational Definition 6.7 of branching bisimilarity. We can still solve the main spectroscopy problem, but lose some resolution about the number of nested conjunctions.

If we read Definition 6.7 directly as a game, it differs from the branching conjunction moves in Definition 7.1, because the latter require the attacker to name as Q_\alpha ex-ante which q' to challenge directly and which ones only after the \alpha step, and to have one continuation for the whole Q_\alpha group. The simplified weak spectroscopy game \mathcal{G}_{\widehat{\nabla}} in Figure 7.3 rephrases this part to match the operational characterization. (This might not be “simpler” conceptionally, but it will be for the algorithm.)

Figure 7.3: Schematic simplified weak spectroscopy game \mathcal{G}_{\widehat{\nabla}} with adapted branching conjunction section (the teal part).

Intuitively, the simplified game part encodes nested conjunctions of the form \textstyle\bigwedge \{ ( \alpha ) {\color{RoyalBlue}\textstyle\bigwedge \Psi'}, \psi_1, \ldots\} or the cheaper form \textstyle\bigwedge \{ ( \alpha ) {\color{RoyalBlue}\langle \varepsilon \rangle\textstyle\bigwedge \Psi'}, \psi_1, \ldots\}. The \Psi' are the formulas from after branching observation moves \smash{\color{gray}[}p,\alpha,p',q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\eta}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}\smash{\color{gray}[}p', Q_\alpha'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\eta}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}\smash{\color{gray}[}p', Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, while the \psi_i come from the resets \smash{\color{gray}[}p,\alpha,p',q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\eta}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}\smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\wedge}}. In Bisping & Jansen (2025), we discuss this game’s strategy formulas in detail and prove its correctness, resulting in the following theorem.17

17  Credit for the proof details goes to Jansen.

Theorem 7.3 (\widehat{\mathbf{N}}^\mathsf{weak} characterization) Let the simplified weak notions \widehat{\mathbf{N}}^\mathsf{weak} be the union of \mathbb{N}\times \{ 0 \} \times \mathbb{N}^6 and \mathbb{N}\times \{ \infty \} \times \{ 0, \infty\} \times \mathbb{N}\times \{ 0, \infty\} \times \mathbb{N}^3. Let simplified expressiveness prices be defined by rounding up the prices of Definition 6.11: \widehat{\mathsf{expr}}^{\mathsf{weak}} = \min \{ N \in \widehat{\mathbf{N}}^\mathsf{weak} \mid \mathsf{expr}^{\mathsf{weak}}(\varphi) \leq N \}. Then, on the simplified weak game \mathcal{G}_{\widehat{\nabla}} of Figure 7.3:

For all N \in \widehat{\mathbf{N}}^\mathsf{weak}, p \in \mathcal{P}, Q \in 2^{\mathcal{P}}, the following are equivalent:

  • There exists a formula \varphi \in \mathsf{HML}_{\mathsf{SRBB}} with price \widehat{\mathsf{expr}}^{\mathsf{weak}}(\varphi) \leq N that distinguishes p from Q.
  • Attacker wins \mathcal{G}_{\widehat{\nabla}}^{\mathcal{S}} from \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} with energy N.

Complexity-wise, for the simplified game, \mathcal{G}_{\widehat{\nabla}}, we have just \smash{|{G_{\widehat{\nabla}}}|} \in \mathit{O}( \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \cdot 2^{\smash{|{\mathcal{P}}|}}) and also o_{\widehat{\nabla}} \in \mathit{O}( \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|}). Following the same argument as in Theorem 7.2, deciding the whole game still has exponential time complexity of \mathit{O}(\smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \cdot (\smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \cdot 2^{\smash{|{\mathcal{P}}|}})^{16} \cdot (\smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \cdot 2^{\smash{|{\mathcal{P}}|}})^{7}) = \mathit{O}( \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|}^{24} \cdot 2^{23 \smash{|{\mathcal{P}}|}} ), and space complexity \mathit{O}( \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|}^8 \cdot 2^{8 \smash{|{\mathcal{P}}|}} ). But these are much lower bounds than in the original game \mathcal{G}_{\nabla}, where we found \mathit{O}( \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|}^{24} \cdot 3^{24\smash{|{\mathcal{P}}|}} ) for time and \mathit{O}( \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|}^8 \cdot 3^{8\smash{|{\mathcal{P}}|}}) for space.

The practical difference is huge on transition systems exposing relevant branching-degree with respect to internal behavior such as the initial Peterson system of Figure 1.2: With the optimization, the tool solves it in fractions of a second, as reported in Table 8.4. Without it, the exponential conjunctions lead to a game with 121,773 moves, taking 90 seconds.

Moreover, we can again use the trick to work with flattened energies, according to Lemma 4.6. After all, \mathcal{G}_{\widehat{\nabla}} itself is only correct with respect to a simplified spectrum according to Theorem 7.3. If we bound the energy lattice to \{0, 1, \infty\}^8 the size of Pareto fronts is decoupled from the game size. This further improves space complexity to \mathit{O}( \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \cdot 2^{\smash{|{\mathcal{P}}|}} ) and overall time complexity to \mathit{O}( \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \cdot (\smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} \cdot 2^{\smash{|{\mathcal{P}}|}})^{16} ) = \mathit{O}( \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|}^{17} \cdot 2^{16 \smash{|{\mathcal{P}}|}} ).

7.3.2 Covering Revivals and Decorated Traces

In the weak spectrum of Section 6.3, we left out the notions of revivals, failure traces, and ready traces, which we had included in the strong spectrum of Section 3.2.2. Their stable variants are relevant to the CSP community (see Roscoe, 2009).

As discussed in Example 3.5, these notions need to differentiate between a deepest “revival” conjunct and other positive conjuncts. Thus, these equivalences need an additional dimension for \mathsf{expr}^{}-measurements, and an even more sophisticated handling of conjunctions in the game.

Figure 7.4 illustrates how one could incorporate revivals into stable conjunctions, analogously to Chapter 5. Note, that we now have two kinds of conjunct positions: for the stable non-revival context and for the other contexts. The maximal depth of conjuncts is still managed by dimension 6. But stable non-revival conjuncts receive a new dedicated dimension 7 to bound their depth. The previous dimensions 7 and 8 now come 8th and 9th.

Figure 7.4: Modifying stable conjunction moves to include revivals (teal part). The branching bisimulation part is left out.

In this game, stable revivals end up at (\infty, 0, 0, {\color{RoyalBlue}1}, 0, {\color{RoyalBlue}1}, {\color{RoyalBlue}0}, 1, 1), stable failure traces at (\infty, 0, 0, 1, 0, {\color{RoyalBlue}\infty}, 0, 1, 1), and stable ready traces at (\infty, 0, 0, 1, 0, {\color{RoyalBlue}\infty}, {\color{RoyalBlue}1}, 1, 1), analogously to their strong counterparts in Figure 3.8. Of course, one could again use the “look-ahead trick” of Section 5.2.2 to reduce the number of partitions to consider.

In fact, the implementation on equiv.io does employ this formulation, thereby actually using a 9-dimensional game with richer stable conjunctions. Although this thesis remains short on providing a theorem for the game that contains the stable revival move, tests in the tool (and the theorems for the strong spectrum) suggest correctness of the variant in Figure 7.4.

7.3.3 Extending to Other Equivalences

At this point, we have covered most interesting parts of strong and weak spectrum. But there are still more notions one could reach for.

Divergence and completed observations.   Logic and game, as we have presented them, are blind to divergence and completed observations. Van Glabbeek (1993) uses additional modalities: \Delta for divergence with \llbracket \Delta \rrbracket \mathrel{≔}\{p \mid p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}^\omega\}; 0 for completed observations with \llbracket 0 \rrbracket \mathrel{≔}\{p \mid \forall \alpha \in \mathit{Act}. \overset{\smash{\raisebox{-2pt}{$\scriptstyle{\alpha}$}}}{\nrightarrow} \} (and \lambda \mathrel{≔}0 \lor \Delta).

Bisping & Jansen (2024) decide against including these modalities in the game. At least on finite-state systems, they may be understood to be special action observations. Divergence and completion can be added through pre-processing into a system \mathcal{S} before turning to our game of equivalence questions on \mathcal{S}'.

For 0, the transformation from \mathcal{S} to \mathcal{S}' is obvious: Add a p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\checkmark}$}}} \bot to the transition system for each p \in \mathcal{P} where p \overset{\smash{\raisebox{-2pt}{$\scriptstyle{a}$}}}{\nrightarrow} for every a \in \mathit{Act}_👁 (with \checkmark and \bot fresh). Then \llbracket \langle \checkmark \rangle\top \rrbracket^{\smash{\mathcal{S}'}} = \llbracket 0 \rrbracket^{\smash{\mathcal{S}}}.

For divergence on finite-state systems, one may use an argument from Groote et al. (2017): Add a state \bot, an action \delta \notin \mathit{Act} and transitions p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\delta}$}}} \bot to the transition system for each p \in \mathcal{P} that lives on a \tau-cycle p \mathrel{\smash{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}}^+} p. Then \llbracket \langle \varepsilon \rangle\langle \delta \rangle\top \rrbracket^{\smash{\mathcal{S}'}} = \llbracket \Delta \rrbracket^{\smash{\mathcal{S}}}. Fokkink et al. (2019) define a unary diverges-while operator \Delta \varphi to characterize divergence-preserving branching bisimilarity; this operator is then naturally expressed as branching conjunction \langle \varepsilon \rangle\textstyle\bigwedge \{( \delta )\top, \varphi\}.

For infinite systems, divergence is more tricky. Just like infinite traces, it depends on the possibility of characterizing infinite-duration attacks.18 On the game level, for infinite plays to be winnable by the attacker, the game must have a parity-game winning condition: The attacker wins a subgame about divergence-distinction if they can make infinitely much \tau-progress, but the defender cannot. Such a richer game model is the route taken by Frutos Escrig et al. (2017) to characterize various divergence-aware bisimilarities.

18 And not just unbounded attack strategies as we support them now.

Behavioral congruences.   Famously, many of the unstable weak equivalences need to be refined in order to be congruences for CCS with choice “+” (cf. Gazda et al., 2020; Sangiorgi, 2012). For instance, rooted weak bisimulation congruence is achieved by allowing an \langle \varepsilon \rangle\langle \tau \rangle...-observation at the outermost level of the HML characterization. Otherwise, weak bisimulation formulas have no \langle \tau \rangle-parts (see Figure 6.7).

This thesis is not going deeper into congruences. But let us note that, clearly, the weak spectroscopy game could be extended by some prefix to enable such special observations for the attacker at the beginning if rootedness is desired.

Coupled simulation.   As mentioned in Section 6.4, we have glimpsed over coupled similarity. It can be thought of as the syntactic combination of weak similarity and contrasimilarity in the sense that each weak conjunction must either contain purely positive or purely negative conjuncts, as outlined in Bisping & Montanari (2024). This possibility does not align nicely with our game formulation because it means that the attacker has to dedicate a conjunction to positivity or negativity before entering, and not make up their mind on the fly whether q \in Q are addressed positively or negatively. If desired, this could be treated by a new dimension in modal conjunctions and game positions. Who urgently needs to compute coupled similarity relations, may otherwise fall back to the coupled simulation game by Bisping & Nestmann (2019).

7.4 Discussion

This chapter has shown that the spectroscopy approach can readily be extended to handle weak behavioral equivalences as well.

The weak spectrum, gamified.   With the weak spectroscopy game, Bisping & Jansen (2024) provide the first generalized game characterization of the silent-step spectrum.

Previously, there have only been partial characterizations of individual equivalences: Frutos Escrig et al. (2017) treat the diamond of weak, delay, \eta and branching bisimilarity. Bisping et al. (2020) and Bisping & Montanari (2021, 2024) cover the area of coupled notions and contrasimilarity. Tan (2002) describes subset-construction variants of the bisimulation game for weak trace equivalence and stable failure equivalence. With the weak spectroscopy game, we have moved beyond such individual equivalence games in order to achieve genericity, covering both linear-time and branching-time as well as stable and unstable notions.

In principle, this chapter only executes Idea 2.2 to translate modal constructions to game moves appearing in \mathsf{HML}_{\mathsf{SRBB}}, which follows Idea 6.1. The important trick is to weaken the attacker according to Idea 7.1, but this departs from prior approaches in weakened games and involves many technicalities. Therefore, it is relieving to have the Isabelle formalization of Section 7.1.3 by Barthel et al. (2025) to verify the construction.

Analyzing systems.   The mini case studies of Section 7.2 show how the spectroscopy automates away the tedious kind of work of finding out the precise relationship between transformed processes that went, for instance, into Bell (2013). Similar searches for weak bisimilarities have happened around Parrow & Sjödin (1992) and Nestmann & Pierce (2000), where coupled similarity turned out to be the most fitting for encodings between models of differing synchronicity.19

19  Nice accounts of Nestmann’s search can be found in Barwell et al. (2022) and in the historical remarks of Bisping et al. (2020).

Concise distinguishing formulas can be interesting diagnostic information to compare models. Like Martens & Groote (2024), we find minimal-depth distinguishing formulas for branching bisimilarity without the need for a special until operator, but we solve the problem for all weak notions at once. Horne et al. (2023) report how inequivalence with respect to more distinctive modal logics can reveal privacy vulnerabilities in ePassports, which have been overlooked in a purely trace-based view. For a full understanding of a system’s relationship to its specification, it is often helpful to pinpoint exactly how difficult it would be for an attacker to tell the two apart.

To be continued.   Some applications would demand more specialized modal logics. As outlined in Section 7.3.3, matching adaptions in game and semantic model are usually straightforward thanks to the clear connection of productions in the modal grammar and mechanics in the spectroscopy game.

But we have assembled enough theory to perform generalized equivalence checking on common models of concurrent systems. Time for Part IV to move beyond theory! In the next chapter, we will return to the initial Example 1.1 of Peterson’s mutex and explain how the prototype implementation of the weak spectroscopy algorithm handles it.