7  Spectroscopy for the Weak Spectrum

7.1 The Weak Spectroscopy Game

7.1.1 The Game

The weak spectroscopy game, in many respects, is just like the spectroscopy games we have already discussed: The attacker 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 kidns 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 For a system \mathcal{S}=(\mathcal{P},\mathit{Act},\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}), the 8-dimensional weak spectroscopy energy game \mathcal{G}_{\nabla}^{\mathcal{S}}=(G,G_{{\mathrm{d}}},\mathrel{\smash{›\!\!\frac{\;\enspace\;}{}\!\!›}},w) consists of

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

where p, q \in \mathcal{P} and Q, Q_\alpha \in 2^{\mathcal{P}}, and sixteen kinds of moves:1 \begin{array}{rrcll} \textit{delay} & {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} & \mathrel{\smash{›\!\!\frac{\;0,0,0,0,0,0,0,0\;}{}\!\!›}} & {{\color{gray}[}p,Q'{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\varepsilon}} & \text{if $Q \mathrel{\twoheadrightarrow}Q'$,} \\ \textit{procrastination} & {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\varepsilon}} & \mathrel{\smash{›\!\!\frac{\;0,0,0,0,0,0,0,0\;}{}\!\!›}} & {{\color{gray}[}p',Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\varepsilon}} & \text{if $p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}} p'$, $p \neq p'$,} \\ \textit{observation} & {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\varepsilon}} & \mathrel{\smash{›\!\!\frac{\;-1,0,0,0,0,0,0,0\;}{}\!\!›}} & {{\color{gray}[}p',Q'{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} & \text{if $p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{a}$}}} p'$, $Q \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{a}$}}} Q'$, $a \neq \tau$,} \\ \textit{finishing} & {{\color{gray}[}p,\varnothing{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} & \mathrel{\smash{›\!\!\frac{\;0,0,0,0,0,0,0,0\;}{}\!\!›}} & {{\color{gray}(}p,\varnothing{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle}}, & \\ \textit{immediate conj.} & {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} & \mathrel{\smash{›\!\!\frac{\;0,0,0,0,-1,0,0,0\;}{}\!\!›}} & {{\color{gray}(}p,Q{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle}} & \text{if $Q \neq \varnothing$,} \\ \textit{late conj.} & {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\varepsilon}} & \mathrel{\smash{›\!\!\frac{\;0,0,0,0,0,0,0,0\;}{}\!\!›}} & {{\color{gray}(}p,Q{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle}}, & \\ \textit{conj. answer} & {{\color{gray}(}p,Q{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle}} & \mathrel{\smash{›\!\!\frac{\;0,0,-1,0,0,0,0,0\;}{}\!\!›}} & {{\color{gray}[}p,q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\land}} & \text{if $q \in Q$,} \\ \textit{positive conjunct} & {{\color{gray}[}p,q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\land}} & \mathrel{\smash{›\!\!\frac{\;\mathtt{min}_{\{\!1,6\!\}},0,0,0,0,0,0,0\;}{}\!\!›}} & {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\varepsilon}} & \text{if $\{q\} \mathrel{\twoheadrightarrow}Q$,} \\ \textit{negative conjunct} & {{\color{gray}[}p,q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\land}} & \mathrel{\smash{›\!\!\frac{\;\mathtt{min}_{\{\!1,7\!\}},0,0,0,0,0,0,-1\;}{}\!\!›}} & {{\color{gray}[}q,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\varepsilon}} & \text{if $\{p\} \mathrel{\twoheadrightarrow}Q$ and $p \neq q$,} \\ \hline \textit{branching conj.}\vphantom{I^{I^I}} & {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\varepsilon}} & \mathrel{\smash{›\!\!\frac{\;0,0,0,0,0,0,0,0\;}{}\!\!›}} & {{\color{gray}(}p,\alpha,p',Q \mathbin{\backslash}Q_\alpha,Q_\alpha{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle\eta}} & \text{if $p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{( \alpha )}$}}} p'$, $Q_\alpha \subseteq Q$,} \\ \textit{branch. answer} & {{\color{gray}(}p,\alpha,p',Q,Q_\alpha{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle\eta}} & \mathrel{\smash{›\!\!\frac{\;0,-1,-1,0,0,0,0,0\;}{}\!\!›}} & {{\color{gray}[}p,q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\land}} & \text{if $q \in Q$,} \\ \textit{branch. observation} & {{\color{gray}(}p,\alpha,p',Q,Q_\alpha{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle\eta}} & \mathrel{\smash{›\!\!\frac{\;\mathtt{min}_{\{\!1,6\!\}},-1,-1,0,0,0,0,0\;}{}\!\!›}} & {{\color{gray}[}p',Q'{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\eta}} & \text{with $Q_\alpha \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{( \alpha )}$}}} Q'$,} \\ \textit{branch. accounting} & {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\eta}} & \mathrel{\smash{›\!\!\frac{\;-1,0,0,0,0,0,0,0\;}{}\!\!›}} & {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}, \\ \hline \textit{stable conj.}\vphantom{I^{I^I}} & {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\varepsilon}} & \mathrel{\smash{›\!\!\frac{\;0,0,0,0,0,0,0,0\;}{}\!\!›}} & {{\color{gray}(}p,Q'{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle s}} & \text{if } Q' = \{ q \in Q \mid q \cancel{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}}\}, p \cancel{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}}, \\ \textit{conj. stable answer} & {{\color{gray}(}p,Q{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle s}} & \mathrel{\smash{›\!\!\frac{\;0,0,0,-1,0,0,0,0\;}{}\!\!›}} & {{\color{gray}[}p,q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\land}} & \text{if $q \in Q$,} \\ \textit{stable finishing} & {{\color{gray}(}p,\varnothing{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle s}} & \mathrel{\smash{›\!\!\frac{\;0,0,0,-1,0,0,0,-1\;}{}\!\!›}} & {{\color{gray}(}p,\varnothing{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle}}. \end{array}

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

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

Figure 7.2: Strategy formulas for the weak spectroscopy.

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

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

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

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

Proof. 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}({{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}, e), then \varphi distinguishes p from Q;
  2. If \chi \in \mathsf{Strat}_{\nabla}({{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\varepsilon}}, e) and Q \mathrel{\twoheadrightarrow}Q, then \langle \varepsilon \rangle\chi distinguishes p from Q;
  3. If \psi \in \mathsf{Strat}_{\nabla}({{\color{gray}[}p,q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\land}}, e), then \psi distinguishes p from \{ q \};
  4. If \textstyle\bigwedge \Psi \in \mathsf{Strat}_{\nabla}({{\color{gray}(}p,Q{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\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}({{\color{gray}(}p,Q{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\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}({{\color{gray}(}p,\alpha,p',Q \mathbin{\backslash}Q_\alpha,Q_\alpha{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\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.

Lemma 7.3 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}}({{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}).5

Proof. 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}({{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\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}({{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\varepsilon}});
  3. If \psi distinguishes p from q, then \mathsf{expr}^{\land}(\psi) \in \mathsf{Win}_\mathrm{a}({{\color{gray}[}p,q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\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}({{\color{gray}(}p,Q{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\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}({{\color{gray}(}p,Q{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\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}({{\color{gray}(}p,\alpha,p'\!,Q \mathbin{\backslash}Q_\alpha, Q_\alpha{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle\eta}}).

Theorem 7.1 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 {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} with N (that is, N \in \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\nabla}^{\mathcal{S}}}({{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}})).

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 hundred of the most interesting lines of the 6500 line theory development.

7  For questsions on the Isabelle/Isar language, consult “The Isabelle/Isar Reference Manual” (Wenzel, 2025).

TODO: Maybe overview figure.

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

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.

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 tranistion relation step) and an energy_game, instantiated with the moves, a predicate spectroscopy_defender singling out defender positions, and the \leq-relation on 8-dimensional energies.

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 datatypes (one per nonterminal).

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.2 as definition for attacker_wins.

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)
  [...]

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

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 Lemma 7.3 that attacks for formulas.

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 is built by combining the previous facts and the upward-closedness of attacker winning budgets win_a_upwards_closure. This is quite straightforward. I reproduce it here in full to provide some idea of what Isar proofs look like.

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

7.1.4 Complexity

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

Theorem 7.2 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 \left|\mathcal{P}\right|.

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.6 for the case d=8 with the size of \mathcal{G}_{\nabla} according to Definition 7.1.

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

However, for the branching conjunction moves, we find a bound of \mathit{O}(\left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right| \cdot 2^{\left|\mathcal{P}\right|}) per attacker delayed position (which is a slight over-approximation). Collectively, these moves reach \mathit{O}(\left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right| \cdot 3^{\left|\mathcal{P}\right|}) defender branching positions {{\color{gray}(}p, \alpha, p', Q \mathbin{\backslash}Q_\alpha, Q_\alpha{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\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}(\left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right| \cdot 2^{\left|\mathcal{P}\right|}) dominates that of other positions, in particular, of defender conjunction, stable conjunction, and branching positions with \mathit{O}(\left|\mathcal{P}\right|) outgoing options.

This amounts to o_{\mathrel{\smash{›\!\!\frac{\;\enspace\;}{}\!\!›}}_\nabla} in \mathit{O}(\left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right| \cdot 2^{\left|\mathcal{P}\right|}) and to \left|G_{\nabla}\right| in \mathit{O}(\left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right| \cdot 3^{\left|\mathcal{P}\right|}).

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

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 (sub-cubic Groote et al. (2017)) end of equivalence problems in the spectrum. De 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. The upcoming Section 7.2.1 will show how to simplify the spectroscopy game to achieve this reduction of size around branching conjunctions.

7.2 Variants

7.2.1 Optimization of Branching Conjunctions

Bisping & Jansen (2025) show how to reduce the out-degree 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.

Figure 7.3: Schematic simplified weak spectroscopy game \mathcal{G}_{\widehat{\nabla}}.

Note that the immediate branching accounting/finishing moves lead to defender conjunction positions, while the late branching accounting move skips it, but still charges for the conjunction by an additional energy update of -\hat{\mathbf{e}}_{3}.

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, while the \psi_i come from the resets.

In Bisping & Jansen (2025) we discuss this game’s strategy formulas in detail and prove its correctness, resulting in the following theorem.9

9  Credit for the proof details goes to David Jansen.

Theorem 7.3 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.10: \widehat{\mathsf{expr}}^{\mathsf{weak}} = \min \{ N \in \widehat{\mathbf{N}}^\mathsf{weak} \mid N \geq \mathsf{expr}^{\mathsf{weak}}(\varphi) \}. 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 {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} with N (that is, N \in \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\widehat{\nabla}}^{\mathcal{S}}}({{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}})).

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

Moreover, we can again use the trick to work with flattened energies, according to Lemma 4.7. 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}( \left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right| \cdot 2^{\left|\mathcal{P}\right|} ) and overall time complexity to \mathit{O}( \left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right| \cdot (\left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right| \cdot 2^{\left|\mathcal{P}\right|})^{16} ) = \mathit{O}( \left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right|^{17} \cdot 2^{16 \left|\mathcal{P}\right|} ).

7.2.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, we had included in the strong spectrum of Section 3.2.2. Their stable variants are relevant to the CSP community (see Roscoe, 2009).

These notions need to differentiate heights 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 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 (brick red part). The branching bisimulation part is left out.

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 trick, thereby actually using a 9-dimensional game with richer stable conjunctions.

7.2.3 Extending to Other Equivalences

7.2.3.1 Divergence and Completed Obervations

Logic and game, as we have presented them, are blind to divergence and to completed observations. 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 \rrbracket \mathrel{:=}\{p \mid \forall a. \cancel{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{a}$}}}} \} (and \lambda \mathrel{:=}0 \lor \Delta).

Bisping & Jansen (2024) have decided against including these in the game. At least on finite-state systems, they may be understood to be special action observations, as follows. In this view, divergence and completion are something to be modelled (or 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 \cancel{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{a}$}}}} for every a \in \mathit{Act}\mathbin{\backslash}\{\tau\} (with \checkmark and \bot fresh). Then \llbracket \langle \checkmark \rangle\top \rrbracket^{\smash{\mathcal{S}'}} = \llbracket 0 \rrbracket^{\smash0{\mathcal{S}}}.

For finite-state systems, divergence can be addressed by 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 \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 \{\langle \delta \rangle\top, \varphi\}.

For infinite systems, divergence is more tricky. Just like infinite traces, it depends on the possibility of characterizing infinite-duration attacks.10 On the game level, for infinite plays to be winnable by the attacker, the game must have a Büchi winning condition. Such a richer game model is the route taken by Frutos Escrig et al. (2017) to characterize various divergence-aware bisimilarities.

10 And not just unbounded attacks as we support them now.

  • Handling Congruences
  • Coupled simulation

7.3 Tackling Our Case Studies

7.3.1 Parallelizing Compilers

Compute = computeA!Compute + computeB!Compute

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

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

@compareSilent PSeq, PPara

7.3.2 Peterson’s Mutual Exclusion

ready = {"A": false, "B": false}
turn  = "A"

def process(ownId, otherId):
  while true:
    ready[ownId] = true
    turn = otherId
    
    do # wait...
    until (ready[otherId] == false || turn == ownId)
      
    print "enter critical #{ownId}"
    # critical section goes here.
    print "leave critical #{ownId}"
    ready[ownId] = false

process("A", otherId = "B") || process("B", otherId = "A")

7.4 Discussion

  • Mention to add back in strong observations