5  Spectroscopy of the Strong Equivalence Spectrum

The energy game approach can, in fact, be leveraged to solve the spectroscopy problem for the whole of the strong equivalence spectrum.

The core ingredient of this chapter is a richer energy game, we dub “spectroscopy game,” to be presented in Section 5.1. The bisimulation energy game of Chapter 4 is not complex enough to capture all strong equivalences of Chapter 3. It is “too easy” for the attacker in the sense that they can use unbounded conjunctions to account for every transition the defender might choose after each observation. But the weaker notions of the spectrum heavily limit how many conjunctions may be used to name a distinction!

Our core trick will be to break the link between conjunctions and observation sequences in the game, analogously to the subset construction on finite automata.

Idea 5.1: Subsets to separate observations and conjunctions

Trace-like notions can be addressed in the spectroscopy game by interjecting a subset construction on defender-controlled states between moves that correspond to observations and to conjunctions.

This will lead to exponential blow-up. Some of it can be alleviated, as we will see in Section 5.2, but most is necessary when deciding strong notions collectively. In Section 5.3, we discuss how to get rid of the blow-up where possible when instantiating the game to decide equivalences individually.

Idea 5.2: Generating equivalence checkers

By instantiating the spectroscopy game with known initial energies and exploiting the supply of conjunction moves, we can derive efficient decision procedures for individual equivalences.

Figure 5.1 gives an overview of the two routes to decide equivalences collectively and individually that we will explore.

Figure 5.1: How we apply the spectroscopy approach to the full strong spectrum.

5.1 The Strong Spectroscopy Game

In this section, we examine a game that does not “overlook” trace observations, as the bisimulation energy game (Definition 4.8) does.

Example 5.1 (Without a trace) Consider the \textsf{CCS} processes \mathsf{a}\ldotp\! \mathsf{b}\ldotp\! \mathsf{a} and \mathsf{a}\ldotp\! (\mathsf{a} +\mathsf{b}). Clearly, only the first one allows the trace observation \langle \mathsf{a} \rangle\langle \mathsf{b} \rangle\langle \mathsf{a} \rangle. Thus, the processes are not bisimilar and can be distinguished in the bisimulation game. But the bisimulation game formula (cf. Lemma 2.9) derivable from the game would be \langle \mathsf{a} \rangle\textstyle\bigwedge \{ \langle \mathsf{b} \rangle, \langle \mathsf{b} \rangle \textstyle\bigwedge \{\langle \mathsf{a} \rangle \}\}, which is not part of trace observations \mathcal{O}^{\mathsf{strong}}_{(\infty,0,0,0,0,0)}.

It might be possible to reconstruct trace observations from such tree-like observations as the one of Example 5.1. But by the closing arguments of Section 4.4, and also according to Martens & Groote (2023), this must inherently be \textsf{NP}-hard. What we will do instead is adapt the bisimulation game such that it also expresses trace-like distinctions, and precisely counts conjunctions.

5.1.1 The Game

The strong spectroscopy game is played not on pairs of states, but on a pair of a state and a set of states! Figure 5.2 gives a graphical representation. The intuition is that the attacker shows how to construct formulas that distinguish a process p from every q in a set of processes Q. As long as observations happen, the defender is moved to the set Q of states that are reachable through nondeterminism; only at conjunction moves does the defender have to choose a q \in Q. Treating conjunctions more explicitly allows us to track the depth of positive conjuncts in sufficient detail.

Figure 5.2: Schematic spectroscopy game \mathcal{G}_{\triangle} of Definition 5.1.

Again, energies limit the syntactic expressiveness of the formulas.

  • The first dimension bounds for how many turns the attacker may challenge observations of actions.
  • The second dimension limits how often they may use conjunctions to resolve nondeterminism.
  • The third, fourth, and fifth dimensions limit how deeply observations may nest underneath a conjunction, for which they do not need to change themselves. The third stands for one of the deepest positive conjuncts and the fourth for the other positive conjuncts; the fifth stands for negative conjuncts.
  • The last dimension limits how often the attacker may use negations to enforce symmetry by swapping sides.

The moves of the following definition closely match productions in the grammar of observations for the strong spectrum of Definition 3.7.

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

  • attacker (main) positions \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \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}},
  • defender conjunction positions \smash{\color{gray}(}p,Q,Q_*\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} \in G_{\mathrm{d}},

where p, q \in \mathcal{P} and Q, Q_* \in 2^{\mathcal{P}}, and six kinds of moves: \begin{array}{rrcll} \textit{observation} & \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;-1,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{\alpha}$}}} p^\prime$\!, $Q \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\alpha}$}}} Q'$,} \\ \textit{conjunction} & \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;0,0,0,0,0,0\;}}{}\!\!›}} & \smash{\color{gray}(}p,Q \mathbin{\backslash}Q_*, Q_*\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} & \text{if $Q_* \subseteq Q$,} \\ \textit{conj.~revival} & \smash{\color{gray}(}p,Q,Q_*\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\mathtt{min}_{\{\!1,3\!\}},-1,0,0,0,0\;}}{}\!\!›}} & \smash{\color{gray}[}p,Q_*\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} & \text{if $Q_* \neq \varnothing$,} \\ \textit{conj.~answer} & \smash{\color{gray}(}p,Q,Q_*\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;0,-1,0,\mathtt{min}_{\{\!3,4\!\}},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,4\!\}},0,0,0,0,0\;}}{}\!\!›}} & \smash{\color{gray}[}p,\{q\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, & \text{and} \\ \textit{negative conjunct} & \smash{\color{gray}[}p,q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\land}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\mathtt{min}_{\{\!1,5\!\}},0,0,0,0,-1\;}}{}\!\!›}} & \smash{\color{gray}[}q,\{p\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} & \text{if $p \neq q$.} \\ \end{array}

On the processes of Example 5.1, the attacker would move: \begin{array}{rcl} \smash{\color{gray}[}\mathsf{a}\ldotp\! \mathsf{b}\ldotp\! \mathsf{a}, \{\mathsf{a}\ldotp\! (\mathsf{a} +\mathsf{b})\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;-\hat{\mathbf{e}}_{1}\;}}{}\!\!›}} & \smash{\color{gray}[}\mathsf{b}\ldotp\! \mathsf{a}, \{\mathsf{a}, \mathsf{b}\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \\ & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;-\hat{\mathbf{e}}_{1}\;}}{}\!\!›}} & \smash{\color{gray}[}\mathsf{a}, \{\mathbf{0}\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \\ & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;-\hat{\mathbf{e}}_{1}\;}}{}\!\!›}} & \smash{\color{gray}[}\mathbf{0}, \varnothing\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \\ & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\;\mathbf{0}\;\;}}{}\!\!›}} & \smash{\color{gray}(}\mathbf{0}, \varnothing, \varnothing\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} \; \mathrel{\smash{{›/\!\!\!\!\frac{\scriptstyle{\;\enspace\;}}{\;}\!\!›}}} \end{array} Thereby, the attacker would get the defender stuck on a trace budget of (3,0,0,0,0,0) \leq (\infty,0,0,0,0,0) = \mathrm{T}.

The handling of conjunctions can be a little more intricate.

Example 5.2 (Failure traces enter the game) Let us think back to Example 3.5, that is, to \mathsf{Q'} ≔ \tau\ldotp\! (\mathsf{a}\ldotp\! \mathsf{a} +\mathsf{b}\ldotp\! \mathsf{b}), \mathsf{T'_{\tau a a}} ≔ \mathsf{Q'} +\tau\ldotp\!\mathsf{a}\ldotp\! \mathsf{a}, and \mathsf{T'_{\tau a}} ≔ \mathsf{Q'} +\tau\ldotp\!\mathsf{a}, where \mathsf{T'_{\tau a a}} is distinguished from \mathsf{T'_{\tau a}} by the failure-trace observation \langle \tau \rangle \textstyle\bigwedge \{\langle \mathsf{a} \rangle\langle \mathsf{a} \rangle, \neg\langle \mathsf{b} \rangle\} \in \mathcal{O}^{\mathsf{strong}}_{(3,1,2,0,1,1)} \subseteq \mathcal{O}^{\mathsf{strong}}_{\mathrm{\mathsf{FT}}}.

To point out a similar distinction in the spectroscopy game, the attacker moves via \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\tau}$}}}: \begin{array}{rcl} \smash{\color{gray}[}\mathsf{T'_{\tau a a}}, \{\mathsf{T'_{\tau a}}\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;-\hat{\mathbf{e}}_{1}\;}}{}\!\!›}} & \smash{\color{gray}[}\mathsf{a}\ldotp\! \mathsf{a}, \{\mathsf{a}, \mathsf{a}\ldotp\! \mathsf{a} +\mathsf{b}\ldotp\! \mathsf{b}\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \\ & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\;\mathbf{0}\;\;}}{}\!\!›}} & \smash{\color{gray}(}\mathsf{a}\ldotp\! \mathsf{a}, \{\mathsf{a}\ldotp\! \mathsf{a} +\mathsf{b}\ldotp\! \mathsf{b}\}, \{\mathsf{a}\}\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} \end{array} Now, the defender has two options.

  • If defender chooses conjunction answer \dots \mathrel{\smash{›\!\!\frac{\scriptstyle{\;0,-1,0,\mathtt{min}_{\{\!3,4\!\}},0,0\;}}{}\!\!›}} \smash{\color{gray}[}\mathsf{a}\ldotp\! \mathsf{a}, \mathsf{a}\ldotp\! \mathsf{a} +\mathsf{b}\ldotp\! \mathsf{b}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\wedge}}, then attacker points out that \mathsf{b} is not possible for the left process: \begin{array}{rcl} \smash{\color{gray}[}\mathsf{a}\ldotp\! \mathsf{a}, \mathsf{a}\ldotp\! \mathsf{a} +\mathsf{b}\ldotp\! \mathsf{b}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\wedge}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\mathtt{min}_{\{\!1,5\!\}},0,0,0,0,-1\;}}{}\!\!›}} & \smash{\color{gray}[} \mathsf{a}\ldotp\! \mathsf{a} +\mathsf{b}\ldotp\! \mathsf{b}, \{\mathsf{a}\ldotp\! \mathsf{a}\} \smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}\\ & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;-\hat{\mathbf{e}}_{1}\;}}{}\!\!›}} & \smash{\color{gray}[} \mathsf{b}, \varnothing \smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \\ & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\;\mathbf{0}\;\;}}{}\!\!›}} & \smash{\color{gray}(}\mathsf{b}, \varnothing, \varnothing\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} \; \mathrel{\smash{{›/\!\!\!\!\frac{\scriptstyle{\;\enspace\;}}{\;}\!\!›}}} \end{array}
  • If defender opts for a conjunction revival \dots \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\mathtt{min}_{\{\!1,3\!\}},-1,0,0,0,0\;}}{}\!\!›}} \smash{\color{gray}[}\mathsf{a}\ldotp\! \mathsf{a}, \{\mathsf{a}\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, then attacker highlights that the left process can do \mathsf{a} \mathsf{a}: \begin{array}{rcl} \smash{\color{gray}[}\mathsf{a}\ldotp\! \mathsf{a}, \{\mathsf{a}\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;-\hat{\mathbf{e}}_{1}\;}}{}\!\!›}} & \smash{\color{gray}[} \mathsf{a}, \{\mathbf{0}\} \smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \\ & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;-\hat{\mathbf{e}}_{1}\;}}{}\!\!›}} & \smash{\color{gray}[} \mathbf{0}, \varnothing \smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \\ & \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\;\mathbf{0}\;\;}}{}\!\!›}} & \smash{\color{gray}(}\mathbf{0}, \varnothing, \varnothing\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} \; \mathrel{\smash{{›/\!\!\!\!\frac{\scriptstyle{\;\enspace\;}}{\;}\!\!›}}} \end{array}

To win in both cases, the attacker must start with an energy budget of at least (3,1,2,0,1,1).

The game also allows an alternative through nested negations that the attacker wins at (3,2,0,0,2,2), but this is not interesting for specific equivalences below bisimilarity.

Example 5.3 (Half-simulated philosophers) Let us see what our prototype implementation on equiv.io reports about our original example processes \mathsf{P} and \mathsf{Q} of Chapter 2. We can input the philosopher processes of Example 2.2 and Example 2.3,1 obtaining a transition system matching Example 2.1:

1  A usage guide on the syntax can be found in Section 8.1.1.

PA = fork.a
PB = fork.b
P  = (fork! | PA | PB) \ {fork}

Q  = (fork! | fork.(a + b)) \ {fork}

@compare P, Q

Starting @compare (on equiv.io) triggers a spectroscopy along the lines we have discussed, leading to the output:2

2  A spectroscopy game on this example can also be played through in the computer game The Spectroscopy Invaders, see Section 8.2.1.

• Preordered by:
    simulation
• Left-right-distinguished by:
    ⟨τ⟩⋀{¬⟨b⟩⊤} (failure)
    ⟨τ⟩⋀{¬⟨a⟩⊤} (failure)
• Equated by:
    trace

That P is simulated by Q matches our finding from Example 2.6. Internally this is established by building the spectroscopy game and computing that \mathsf{Win}^{\mathrm{min}}_\mathrm{a}(\smash{\color{gray}[}\mathsf{P}, \{\mathsf{Q}\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}) = \{(2,1,0,0,1,1)\}.

That no equivalence besides or above simulation can hold, is justified to the user by the failure ⟨τ⟩⋀{¬⟨a⟩⊤}, which we also discussed in Section 3.1.2. In the upcoming Section 5.1.2, we will also give the rules that the tool uses to construct this witness in \mathsf{Strat}_{\triangle}.

Invoking @compare Q, P for the other direction, equiv.io reports ⟨τ⟩⋀{⟨b⟩⊤,⟨a⟩⊤} as a distinguishing formula disproving simulation (as we have found in Example 2.12).

The spectroscopy game still is a bisimulation game in the following sense.

Proposition 5.1 (Defender bisimilarity) States p_0 and q_0 are bisimilar precisely if the defender wins \mathcal{G}_{\triangle} from \smash{\color{gray}[}p_0, \{q_0\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} for every initial energy budget e_0, that is, if (\infty, \infty, \infty, \infty, \infty, \infty) \in \mathsf{Win}_\mathrm{d}(\smash{\color{gray}[}p_0, \{q_0\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}).3

3  Proof in Lemma 1 of Bisping (2023b).

Remark 5.1 (The \triangle-symbol). We use the \triangle in \mathcal{G}_{\triangle} with a double meaning: To symbolize a prism, which reveals the spectrum of light, and to mean difference, as the game expresses an abstract form of subtraction in the sense of Section 3.3.2.

5.1.2 Correctness

To prove correctness, we proceed as with the bisimulation energy game in Section 4.2.3: On the one hand, we show that game moves correspond to formulas of similar prices and that the attacker winning implies the formulas to be distinguishing. On the other hand, we establish that formulas of certain expressiveness prices certify winning attacks of matching budgets.

Definition 5.2 (Strategy formulas for \mathcal{G}_{\triangle}) In the context of a strong spectroscopy game \mathcal{G}_{\triangle}^{\mathcal{S}}, the set of strategy formulas \mathsf{Strat}_{\triangle}(g, e) for a game position g and a budget e is defined inductively by the following rules in Figure 5.3.

\mathrm{observation}\;\dfrac{\begin{matrix} \begin{matrix} \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;-\hat{\mathbf{e}}_{1}\;}}{}\!\!›}} \smash{\color{gray}[}p', Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \quad e' = \mathsf{upd}(-\hat{\mathbf{e}}_{1}, e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\triangle}}(\smash{\color{gray}[}p', Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}) \\ p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\alpha}$}}} p' \quad Q \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\alpha}$}}} Q' \quad φ ∈ \mathsf{Strat}_{\triangle}(\smash{\color{gray}[}p', Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e') \end{matrix} \end{matrix}}{ \langle α \rangle φ ∈ \mathsf{Strat}_{\triangle}(\smash{\color{gray}[}p, Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e) }\hphantom{\mathrm{observation}} \mathrm{conjunction}\;\dfrac{\begin{matrix} \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\;\mathbf{0}\;\;}}{}\!\!›}} \smash{\color{gray}(}p, Q', Q_*\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} \quad e ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\triangle}}(\smash{\color{gray}(}p, Q', Q_*\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}) \quad φ ∈ \mathsf{Strat}_{\triangle}(\smash{\color{gray}(}p, Q', Q_*\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}, e) \end{matrix}}{ φ ∈ \mathsf{Strat}_{\triangle}(\smash{\color{gray}[}p, Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e) }\hphantom{\mathrm{conjunction}} \mathrm{conj.~answer}\;\dfrac{\begin{matrix} \begin{matrix} \forall q ∈ Q \ldotp \; \smash{\color{gray}(}p, Q, \varnothing\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\wedge}} \; \land \; e_q = \mathsf{upd}(u_q, e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\triangle}}(\smash{\color{gray}[}p, q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\wedge}}) \; \land \; \psi_q ∈ \mathsf{Strat}_{\triangle}(\smash{\color{gray}[}p, q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\wedge}}, e_q) \end{matrix} \end{matrix}}{ \textstyle\bigwedge_{q \in Q} \psi_q ∈ \mathsf{Strat}_{\triangle}(\smash{\color{gray}(}p, Q, \varnothing\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}, e) }\hphantom{\mathrm{conj.~answer}} \mathrm{conj.~revival}\;\dfrac{\begin{matrix} \begin{matrix} \forall q ∈ Q \ldotp \; \smash{\color{gray}(}p, Q, 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\wedge}} \; \land \; e_q = \mathsf{upd}(u_q, e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\triangle}}(\smash{\color{gray}[}p, q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\wedge}}) \; \land \; \psi_q ∈ \mathsf{Strat}_{\triangle}(\smash{\color{gray}[}p, q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\wedge}}, e_q) \\ \smash{\color{gray}(}p, Q, Q_*\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u_*\;}}{}\!\!›}} \smash{\color{gray}[}p, Q_*\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \quad e_* = \mathsf{upd}(u_*, e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\triangle}}(\smash{\color{gray}[}p, Q_*\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}) \\ \psi_* = \langle α \rangle φ ∈ \mathsf{Strat}_{\triangle}(\smash{\color{gray}[}p, Q_*\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e_*) \end{matrix} \end{matrix}}{ \textstyle\bigwedge_{q \in Q \cup \{*\}} \psi_q ∈ \mathsf{Strat}_{\triangle}(\smash{\color{gray}(}p, Q, Q_*\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}, e) }\hphantom{\mathrm{conj.~revival}} \mathrm{positive~conjunct}\;\dfrac{\begin{matrix} \begin{matrix} \smash{\color{gray}[}p, q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\wedge}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u\;}}{}\!\!›}} \smash{\color{gray}[}p, \{q\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \quad e' = \mathsf{upd}(u, e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\triangle}}(\smash{\color{gray}[}p, \{q\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}) \\ \langle α \rangle φ ∈ \mathsf{Strat}_{\triangle}(\smash{\color{gray}[}p, \{q\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e') \end{matrix} \end{matrix}}{ \langle α \rangle φ ∈ \mathsf{Strat}_{\triangle}(\smash{\color{gray}[}p, q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\wedge}}, e) }\hphantom{\mathrm{positive~conjunct}} \mathrm{negative~conjunct}\;\dfrac{\begin{matrix} \begin{matrix} \smash{\color{gray}[}p, q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\wedge}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u\;}}{}\!\!›}} \smash{\color{gray}[}q, \{p\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \quad e' = \mathsf{upd}(u, e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\triangle}}(\smash{\color{gray}[}q, \{p\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}) \\ p \neq q \quad \langle α \rangle φ ∈ \mathsf{Strat}_{\triangle}(\smash{\color{gray}[}q, \{p\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e') \end{matrix} \end{matrix}}{ \neg\langle α \rangle φ ∈ \mathsf{Strat}_{\triangle}(\smash{\color{gray}[}p, q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\wedge}}, e) }\hphantom{\mathrm{negative~conjunct}}

Figure 5.3: Rules to derive distinguishing formulas from winning attack strategies.

The base case of the definition is the rule for conjunction answers at \smash{\color{gray}(}p, \varnothing, \varnothing\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} It yields the strategy formula \top, which trivially distinguishes any p from the empty set.

The correctness proof for \mathcal{G}_{\triangle} proceeds basically as with the bisimulation energy game \mathcal{G}^{🗲}_{\mathrm{B}}, establishing soundness as in Lemma 4.1 and completeness as in Lemma 4.2. Proofs can be found in Bisping (2023b). There are two minor definitional nuances between the presentation here and there, upon which we will comment in Remark 5.2.

Lemma 5.1 (Distinction soundness) If e ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\triangle}}(\smash{\color{gray}[}p, Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}), then there is φ ∈ \mathsf{Strat}_{\triangle}(\smash{\color{gray}[}p, Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e) with φ ∈ \mathcal{O}^{\mathsf{strong}}_{e}, p ∈ \llbracket φ \rrbracket and Q \cap \llbracket φ \rrbracket = \varnothing.4

4  Proof in Lemma 2, 3, and 4 of Bisping (2023b).

Lemma 5.2 (Distinction completeness) If there is φ ∈ \mathcal{O}^{\mathsf{strong}}_{N} with p ∈ \llbracket φ \rrbracket and Q \cap \llbracket φ \rrbracket = \varnothing, then N ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\triangle}}(\smash{\color{gray}[}p, Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}).5

5  Proof in Lemma 5 of Bisping (2023b).

Taken together, Lemma 5.1 and Lemma 5.2 prove that the strong spectroscopy game \mathcal{G}_{\triangle} precisely characterizes the strong equivalence spectrum \mathbf{N}^\mathsf{strong}.

Theorem 5.1 (\mathbf{N}^\mathsf{strong}-characterization) p \preceq_{\mathcal{O}^{}_{N}} q for N ∈ \mathbf{N}^\mathsf{strong} precisely if the defender wins \mathcal{G}_{\triangle} for the attacker starting from \smash{\color{gray}[}p,\{q\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} with budget N.

Thus, we can solve the spectroscopy problem (Problem 3.1) by computing \mathbf{N}^\mathsf{strong}_{p,q} = \mathbf{N}^\mathsf{strong}_{\vphantom{p}} \mathbin{\backslash}\mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\triangle}}(\smash{\color{gray}[}p, \{q\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}).

Remark 5.2 (Differences to conference version). As mentioned in Remark 3.1, Bisping (2023a) uses a slightly different pricing, where \mathsf{expr}^{}(\top) = \hat{\mathbf{e}}_{2}. This difference is reflected in the game by Definition 5.1 charging -\hat{\mathbf{e}}_{2} for conjunctions after the defender conjunction positions instead of before. With this, the attacker wins \smash{\color{gray}[}p, \varnothing\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\;\mathbf{0}\;\;}}{}\!\!›}} \smash{\color{gray}(}p, \varnothing, \varnothing\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} with budget \mathbf{0}, while the original definition in Bisping (2023a) would cost them \hat{\mathbf{e}}_{2} for \smash{\color{gray}[}p, \varnothing\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \mathrel{\smash{›\!\!\frac{\scriptstyle{\;-\hat{\mathbf{e}}_{2}\;}}{}\!\!›}} \smash{\color{gray}(}p, \varnothing, \varnothing\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}.

Also, Bisping (2023a) defines the spectrum coordinates by giving the \mathsf{expr}^{} function instead of an \mathcal{O}^{}_{N \in \mathbf{N}} hierarchy.

The conference paper results apply to the present presentation mutatis mutandis. However, we will achieve better complexity results in the next section, thanks to Lemke (2024).

5.1.3 Complexity

As expected, the bigger spectroscopy game leads to exponential runtimes. This comes as no surprise, for we have already discussed in Section 3.3.3 that the spectroscopy problem on the whole strong spectrum is \textsf{PSPACE}-hard.

Theorem 5.2 (Strong spectroscopy complexity) Given a transition system \mathcal{S}, the spectroscopy problem for the \mathbf{N}^\mathsf{strong}-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 5.1, we can solve the spectroscopy problem for the \mathbf{N}^\mathsf{strong}-spectrum by deciding the winning budgets of the strong spectroscopy game \mathcal{G}_{\triangle}^{\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=6 with the size of \mathcal{G}_{\triangle} according to Definition 5.1.

The number of attacker main positions is bounded by \smash{|{\mathcal{P}}|} \cdot 2^{\smash{|{\mathcal{P}}|}}. The number of conjunction moves and defender conjunction positions is bounded by \smash{|{\mathcal{P}}|} \cdot 3^{\smash{|{\mathcal{P}}|}}.

The maximal out-degree for attacker positions is in \mathit{O}(2^{\smash{|{\mathcal{P}}|}}), which dominates that of defender conjunction positions of \mathit{O}(\smash{|{\mathcal{P}}|}),

This leads to o_{\mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}} in \mathit{O}(2^{\smash{|{\mathcal{P}}|}}) and to \smash{|{G_{\triangle}}|} in \mathit{O}(\smash{|{\mathcal{P}}|} \cdot 3^{\smash{|{\mathcal{P}}|}}). Filling 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 & (d^2 + \smash{|{G}|}^{d-1} \cdot d) & ) \\ = & O( & (2^{\smash{|{\mathcal{P}}|}}) & \cdot & (\smash{|{\mathcal{P}}|} \cdot 3^{\smash{|{\mathcal{P}}|}})^{2 \cdot 6} & \cdot & (6^2 + (\smash{|{\mathcal{P}}|} \cdot 3^{\smash{|{\mathcal{P}}|}})^{6-1} \cdot 6) & ) \\ = & O( & 2^{\smash{|{\mathcal{P}}|}} & \cdot & \smash{|{\mathcal{P}}|}^{12} \cdot 3^{12\smash{|{\mathcal{P}}|}} & \cdot & \smash{|{\mathcal{P}}|}^5 \cdot 3^{5\smash{|{\mathcal{P}}|}} & ) \\ = & O( & \smash{|{\mathcal{P}}|}^{17} & \cdot & 2^{\smash{|{\mathcal{P}}|}} \cdot 3^{17\smash{|{\mathcal{P}}|}} & ). \end{array} For space complexity, the approach arrives at \mathit{O}( \smash{|{\mathcal{P}}|}^6 \cdot 3^{6\smash{|{\mathcal{P}}|}}).

Still, there are ways to decrease the complexity of the algorithm and thus increase applicability. We will explore these in the next section.

5.2 Clever Games on Subgraphs

We can exploit properties of the equivalences to focus on simpler variants of the spectroscopy game.

  1. Properties of bisimilarity allow to reduce the game graph size without losing information.
  2. Since the specific coordinates in Figure 3.8 only use 0, 1, and ∞ in components, we can employ Lemma 4.6 to slightly improve complexity bounds.
  3. With more specific equivalences in mind, we can also focus on subgraphs of the spectroscopy game \mathcal{G}_{\triangle} in order to obtain better bounds.

Section 5.2.1 will first discuss how parts of the game graph can be pruned thanks to properties of bisimilarity. Then, we will use all listed tricks in the “clever” strong spectroscopy game in Section 5.2.2. In the subsequent Section 5.3, we will take the last point to the extreme by instantiating the spectroscopy game down to only decide single equivalences.

5.2.1 Pruning with Logic

We can exploit that the spectroscopy game is a bisimulation game by Proposition 5.1 to reduce game graph size. In particular, we will profit from the properties of bisimilarity being symmetric and transitive.

Lemma 5.3 (Symmetry defense) On a strong spectroscopy game, p \in Q implies \mathsf{Win}_\mathrm{a}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}) = \varnothing.

Proof. This is a contrapositive consequence of Lemma 5.1: As soon as Q contains a state bisimilar to p, there cannot be a distinguishing formula for them by Theorem 2.1. This is the case here because p \in Q and p \sim_\mathrm{B} p by Lemma 2.1. Thus, there cannot be e \in \mathsf{Win}_\mathrm{a}(\smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}).

For the game graph, this means that we do not need to consider any outgoing moves of \smash{\color{gray}[}p,\{p\} \cup Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}-positions. They will not lead to attacker wins anyway. All game graph parts that are only reached through such positions can be disregarded.

Another important trick to reduce game size is to first apply bisimulation-minimization to the transition system and then solely construct the spectroscopy game for the minimized system, \mathcal{G}_{\triangle}^{{\mathcal{S} \! / \!\! \sim_\mathrm{B}}}. This approach is sound by the following lemma.

Lemma 5.4 (Quotienting by bisimilarity) The attacker wins \smash{\color{gray}[}p, \{q\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} on \mathcal{G}_{\triangle}^{\mathcal{S}} with e precisely if they win \smash{\color{gray}[}[p]_{\sim_\mathrm{B}}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, \{[q]_{\sim_\mathrm{B}}\} on \mathcal{G}_{\triangle}^{\smash{{\mathcal{S} \! / \!\! \sim_\mathrm{B}}}}.

Proof. By Proposition 2.4, p \sim_\mathrm{B} [p]_{\sim_\mathrm{B}} and q \sim_\mathrm{B} [q]_{\sim_\mathrm{B}} on the merger of \mathcal{S} and {\mathcal{S} \! / \!\! \sim_\mathrm{B}}. Therefore, the pairs each fulfill the same HML formulas by Theorem 2.1, which implies equal distinguishing formula sets. We can use Lemma 5.1 and Lemma 5.2 to translate these sets to and from the winning budgets.

Example 5.4 (Some measurements) Both tricks of pruning “symmetric” parts (Lemma 5.3) and pre-minimization by bisimilarity (Lemma 5.4) make an effective difference for the applicability of the spectroscopy approach:

scalatool.benchmark.Sizemark uses a small example system from Bisping (2023a) modelling Peterson’s mutual exclusion algorithm.6 The system has only \smash{|{\mathcal{P}}|} = 20 states, but a lot of nondeterminism due to saturation with internal behavior.

6  The reported numbers are produced by sbt "shared/run sizemark --strong-game".

Figure 5.4: Example sizes of a spectroscopy game with and without pruning on Peterson’s mutex system.

Figure 5.4 lists the sizes of game graphs on this system. The default spectroscopy game at the top has roughly 1200 thousand game positions.

Pruning symmetric parts removes roughly four fifths of the graph (leaving 241 thousand positions).

Only applying the bisimulation minimization roughly halves the graph (leaving 661 thousand positions). The bisimulation reduction is surprisingly effective, given that the bisimulation minimized Peterson system still has 19 states, that is, only one fewer than the original system. On the other hand, bisimilar states are precisely those that allow the biggest space of distinctions, blowing up the game.

Interestingly, the combination of both tricks reduces the game graph to 67 thousand positions, roughly 5 % of the original size. (If the effects of both minimizations were only multiplicative, the number would be around 133 thousand states.) This over-proportionate effect on the one hand has to do with the general exponentialities of the game graph, but also with the fact that bisimulation minimization increases the instances where pruning is applicable.7

7  This interplay can already be seen on the bisimulation game. Figure 2.15 contains a big region after [\mathsf{t_{ab}}, \mathsf{q_{ab}}] and [\mathsf{t_{ab}}, \mathsf{q_{ab}}]. Bisimulation minimization of the input system would shrink this region as \mathsf{t_{ab}} \sim_\mathrm{B} \mathsf{q_{ab}}. The two positions would be merged into [\{\mathsf{t_{ab}}, \mathsf{q_{ab}}\}, \{\mathsf{t_{ab}}, \mathsf{q_{ab}}\}]. But this is a symmetric position! Therefore, we can drop this part altogether.

The implementations (Chapter 8) sometimes use small additional tricks for pruning. For instance, one can leave out observation moves behind \smash{\color{gray}[}p, \varnothing\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} positions and finish the game optimally by conjunction.

So far, the optimizations have been lossless in the sense that we do not lose any information on the distinguishability of processes. If we are willing to lose precision, additional reductions of the game graph are possible.

5.2.2 The Clever Game

We can become more clever by looking one step ahead.

The spectroscopy game \mathcal{G}_{\triangle} of Definition 5.1 may branch exponentially with respect to \smash{|{Q}|} at conjunction challenges after \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}. For an efficient implementation, it is desirable to not do that.

Given the spectrum we are interested in, we can drastically limit the sensible attacker moves to four options by a little lookahead into the enabled actions \operatorname{Ini}(q) of q \in Q and \operatorname{Ini}(p).

In the following, we will focus on the lower-resolution sub-spectrum \widehat{\mathbf{N}}^\mathsf{strong} \subseteq \{0, 1, \infty\}^6 \subseteq \mathbf{N}^\mathsf{strong}, where dimensions 3, 4, and 5 of modal depth for revivals, positive and negative conjuncts can only appear in certain combinations.

Definition 5.3 (Simpler strong spectrum) The simpler strong spectrum, \widehat{\mathbf{N}}^\mathsf{strong}, is defined as \widehat{\mathbf{N}}^\mathsf{strong} ≔ \{N \in \{0, 1, \infty\}^6 \mid N_4 \leq N_3 \land (N_5 = \infty \longrightarrow N_3 = N_4)\}.

Observe that all the coordinates of the strong linear-time–branching-time spectrum (Figure 3.8) are still covered by the simpler spectrum.

Definition 5.4 (Clever spectroscopy game) The clever spectroscopy game \mathcal{G}_{\blacktriangle}, is defined exactly like the previous spectroscopy game of Definition 5.1, with the restriction of the conjunction challenges \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} \quad \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\;\mathbf{0}\;\;}}{}\!\!›}}_\blacktriangle \quad \smash{\color{gray}(}p,Q \mathbin{\backslash}Q_*, Q_*\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}} \quad \text{with } Q_* \subseteq Q, to situations where Q_* is one of the four choices

  • \varnothing – no revivals,
  • \{ q \in Q \mid \operatorname{Ini}(q) \subseteq \operatorname{Ini}(p) \} – enabledness-dominated revivals,
  • \{ q \in Q \mid \operatorname{Ini}(p) \subseteq \operatorname{Ini}(q) \} – enabledness-dominating revivals, or
  • \{ q \in Q \mid \operatorname{Ini}(p) = \operatorname{Ini}(q)\} – enabledness-matching revivals.

The idea here is that the attacker only thinks about certain partitionings: Those where the Q_*-revival deals with parts of Q that cannot be discharged through failure or readiness observations. The usage of \operatorname{Ini}(\cdot) is comparable to a small look-ahead into the possibilities to win through observations inside the conjunction.

Theorem 5.3 (Correctness of cleverness) For N \in \widehat{\mathbf{N}}^\mathsf{strong}, the attacker wins \mathcal{G}_{\blacktriangle} from \smash{\color{gray}[}p_0,Q_0\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} with energy N precisely if they win \mathcal{G}_{\triangle} from \smash{\color{gray}[}p_0,Q_0\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} with energy N.8

8  Proof in Theorem 2 of Bisping (2023b).

Theorem 5.4 (Complexity of cleverness) Given a transition system \mathcal{S}=(\mathcal{P},\mathit{Act},\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}), the spectroscopy problem for the simpler \widehat{\mathbf{N}}^\mathsf{strong}-spectrum is solved by the game approach in O( \smash{|{\mathcal{P}}|}^{13} \cdot 2^{12\smash{|{\mathcal{P}}|}} ) time and O( \smash{|{\mathcal{P}}|} \cdot 2^{\smash{|{\mathcal{P}}|}} ) space,

Proof. We instantiate the “flattened” winning budget complexity of Lemma 4.6 for the case d=6 with the size of \mathcal{G}_{\blacktriangle} according to Definition 5.4.

Now, the number of all game positions is bounded by \smash{|{G_{\blacktriangle}}|} \in \mathit{O}(\smash{|{\mathcal{P}}|} \cdot 2^{\smash{|{\mathcal{P}}|}}).

Concerning the maximal out-degree, now, defender conjunction positions are dominant, o_{\mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}_\blacktriangle} \in \mathit{O}(\smash{|{\mathcal{P}}|}). Inserting the parameters in the time bounds of Lemma 4.6 yields: \begin{array}{rlccccccc} & O( & o_{\mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}_\blacktriangle} & \cdot & \smash{|{G_\blacktriangle}|}^{2 \cdot d} & \cdot & (d^2 + 3^{d-1} \cdot d)) \\ = & O( & (\smash{|{\mathcal{P}}|}) & \cdot & (\smash{|{\mathcal{P}}|} \cdot 2^{\smash{|{\mathcal{P}}|}})^{12} & \cdot & (6^2 + 3^{5} \cdot 6) & ) \\ = & O( & \smash{|{\mathcal{P}}|}^{13} \cdot 2^{12\smash{|{\mathcal{P}}|}} & ). \end{array} For space complexity, only game positions are relevant, \mathit{O}( \smash{|{G_\blacktriangle}|} \cdot 3^{d-1} \cdot d ) = \mathit{O}( \smash{|{\mathcal{P}}|} \cdot 2^{\smash{|{\mathcal{P}}|}} ).

Example 5.5 (More measurements) Let us see how the “clever game” adds up with the pruning effects on the Peterson example of Example 5.4.

Figure 5.5: Sizes of clever spectroscopy games with and without pruning on Peterson’s mutex system.

Figure 5.5 is the lower part of a cube of possible game graph optimizations, where Figure 5.4 has already provided the upper part.

We can directly observe that \mathcal{G}_{\blacktriangle} is smaller than \mathcal{G}_{\triangle} by a factor of more than 1000, with 1020 positions instead of 1\,199\,904. This is due to the high nondeterminism of the Peterson system, which leads to big Q-sets in \smash{\color{gray}[}p,Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}-positions. These entail exponentially many conjunction moves in \mathcal{G}_{\triangle}, which are absent in the \mathcal{G}_{\blacktriangle} subgraph.

The tricks of bisimulation minimization and pruning still pay off, reducing the game positions to 65 % of the unpruned game. This is way less effective than in Example 5.4 (where this factor has been 5 %), because the savings are not boosted by exponentialities.

Still, it makes sense to combine all three optimizations. All in all, we have reduced the number of positions by a factor of 1800, and the number of moves by factor 2700.

Especially, the cleverness has paid off. Without these tricks, the approach would not be applicable to systems with relevant nondeterminism due to communication.9

9  The blow-up on Peterson’s mutex is precisely the argument I made in the introduction of Bisping (2023a) for why one has to move beyond the original spectroscopy algorithm of Bisping et al. (2022). Therefore, the original/deprecated approach also is not present in this thesis.

5.3 Deciding Individual Equivalences

As we have seen, the strong spectroscopy characterizes the spectroscopy problem and each individual equivalence (and preorder). This section is about the feasibility to decide individual preorders using the spectroscopy game.

The core idea behind Section 5.3.1 is to derive a reachability game according to Definition 4.4, starting with an energy level from the strong spectrum, Definition 3.8. Then, Algorithm 2.1 can be employed to decide player winning regions of the game and thus the equivalence.

Of course, in this situation, one wants to avoid complexities that are part of the spectroscopy game only to capture other equivalences. Section 5.3.2 will regain polynomiality for the \textsf{P}-easy portion of equivalence problems.

5.3.1 Deriving Equivalence Games

Let us first explicate how to characterize equivalences through reachability games derived according to Definition 4.4.

Definition 5.5 (Derived strong equivalence games) Given a system \mathcal{S}=(\mathcal{P},\mathit{Act},\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}), a strong notion of equivalence N \in \mathbf{N}^\mathsf{strong}, and a pair of states p,q, the derived N-preorder game \mathcal{G}_{\triangle N}^{\mathcal{S},p,q} is defined as the part of the reachability game (\mathcal{G}_{\triangle}^{\mathcal{S}})^R derived from the spectroscopy game under starting position (\smash{\color{gray}[}p,\{q\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, N).

We thus receive a game characterization for every equivalence, generalizing Stirling’s result of the bisimulation game from Theorem 2.2.

Theorem 5.5 (Parametric characterizations) p \preceq_\mathrm{\mathcal{O}^{}_{\mathrm{N}}} q precisely if the defender wins the N-preorder game {\mathcal{G}_{\triangle N}^{\mathcal{S},p,q}} from (\smash{\color{gray}[}p,\{q\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, N).

Proof. By Theorem 5.1, p \preceq_{\mathcal{O}^{}_{N}} q implies that the defender wins \mathcal{G}_{\triangle}^{\mathcal{S}} from \smash{\color{gray}[}p,\{q\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} when the attacker starts at energy N. In other words, N \notin \mathsf{Win}_\mathrm{a}(\smash{\color{gray}[}p, \{q\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}) for \mathcal{G}_{\triangle}^{\mathcal{S}}. Lifted via Proposition 4.4, this implies (\smash{\color{gray}[}p, \{q\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, N) \notin \mathsf{Win}_\mathrm{a} for the derived reachability game (\mathcal{G}_{\triangle}^{\mathcal{S}})^R. By Definition 5.5, the defender thus wins \smash{\mathcal{G}_{\triangle N}^{\mathcal{S},p,q}}. As the proof steps work in both directions, this completes the proof.

The same reasoning works with the clever game version \mathcal{G}_{\blacktriangle}, restricted to the \widehat{\mathbf{N}}^\mathsf{strong}-spectrum used in Theorem 5.3.

Using Algorithm 2.1, our results entail decision procedures for each individual equivalence of the strong spectrum. Of course, it makes sense for algorithms to employ the clever game and pruning.

Example 5.6 (Checking equivalences) The following processes are two of the more complex ones of the separating examples by van Glabbeek (2001, p. 59). They are equal with respect to ready traces, but not for simulation-like and possible-future-like equivalences.

ABCACB = a.(b.d + c.e) + a.(c.f + b.g)
ABC    = a.(b.d + c.e + c.f + b.g)

@check trace,             ABCACB, ABC
@check ready-trace,       ABCACB, ABC
@check simulation,        ABCACB, ABC
@check impossible-future, ABCACB, ABC
@check bisimulation,      ABCACB, ABC

The @check keyword performs individual comparisons on equiv.io. Invoking the check for traces, for instance, yields the following output:

@check trace, ABCACB, ABC
  - "States are equivalent."

The \mathrm{T}-preorder game derived from the (pruned clever) spectroscopy game under \smash{\color{gray}[}\mathsf{ABCACB}, \{\mathsf{ABC}\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} is depicted in Figure 5.6. Each position is won by the defender (hinted at by the positions being colored in blue).

rel -1531522041 ABCACB, {ABC}, {} (∞,0,0,0,0,0) 1655621242 ABCACB, ABC (∞,-1,0,0,0,0) -1531522041->1655621242 (0,-1,0,min{3,4},0,0) -1478041764 ABCACB, {ABC} (∞,0,0,0,0,0) -1478041764->-1531522041 (0,0,0,0,0,0) -58372795 c.f + b.g, {b.d + c.e + c.f + b.g} (∞,0,0,0,0,0) -1478041764->-58372795 (-1,0,0,0,0,0) 11287976 b.d + c.e, {b.d + c.e + c.f + b.g} (∞,0,0,0,0,0) -1478041764->11287976 (-1,0,0,0,0,0) 1890643406 c.f + b.g, b.d + c.e + c.f + b.g (∞,-1,0,0,0,0) -407584024 b.d + c.e, b.d + c.e + c.f + b.g (∞,-1,0,0,0,0) -1030115238 c.f + b.g, {b.d + c.e + c.f + b.g}, {} (∞,0,0,0,0,0) -1030115238->1890643406 (0,-1,0,min{3,4},0,0) 490779022 b.d + c.e, {b.d + c.e + c.f + b.g}, {} (∞,0,0,0,0,0) 490779022->-407584024 (0,-1,0,min{3,4},0,0) 695410661 e, {e,f} (∞,0,0,0,0,0) 945131307 g, {d,g} (∞,0,0,0,0,0) -58372795->-1030115238 (0,0,0,0,0,0) -58372795->945131307 (-1,0,0,0,0,0) -1092705565 f, {e,f} (∞,0,0,0,0,0) -58372795->-1092705565 (-1,0,0,0,0,0) 1777001188 d, {d,g} (∞,0,0,0,0,0) 11287976->490779022 (0,0,0,,0,0) 11287976->695410661 (-1,0,0,0,0,0) 11287976->1777001188 (-1,0,0,0,0,0)
Figure 5.6: Pruned clever strong spectroscopy game below position \smash{\color{gray}[}\mathsf{ABCACB}, \{\mathsf{ABC}\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} instantiated to starting energy \mathrm{T} = (\infty, 0,0,0,0,0) to decide trace equivalence.

Interestingly, the derived reachability game of Figure 5.6 has fewer positions than the pruned clever spectroscopy game below \smash{\color{gray}[}\mathsf{ABCACB}, \{\mathsf{ABC}\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} would have.10

10  Incidentally, the answer to the question how many positions this spectroscopy game would have is 42.

As the derived game positions are obtained through products of original positions and energies, one might assume the derived preorder games to be way bigger than the pure spectroscopy game. But for the named notions, this is usually not the case because of two aspects:

The first important fine point is that many notions have \infty-entries and that \infty - 1 = \infty. For instance, in the derived bisimulation game, starting at (\infty, \infty, \infty, \infty, \infty, \infty), all positions will remain at this energy level. Thus, the derived bisimulation game \mathcal{G}_{\triangle B}^{\mathcal{S},p,q} has isomorphic positions to \mathcal{G}_{\triangle} under \smash{\color{gray}[}p, \{q\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}.

The other point to consider is that the game is cut off at exhausted energies. Therefore, 0-entries in components lead to smaller games, only using subgraphs of the spectroscopy game.

Only 1-components grow the derived game graph. In principle, each component that starts at 1 instead of \infty or 0 might roughly double the graph size.

The equiv.io implementation does prune some attacker moves that cannot be winning, in particular non-empty conjunctions if the conjunction budget is at 0. Therefore, the subgraph used by the tool for Example 5.6 in reality is the one in Figure 5.7.

rel 695410661 e, {e,f} (∞,0,0,0,0,0) 945131307 g, {d,g} (∞,0,0,0,0,0) 11287976 b.d + c.e, {b.d + c.e + c.f + b.g} (∞,0,0,0,0,0) 11287976->695410661 (-1,0,0,0,0,0) 1777001188 d, {d,g} (∞,0,0,0,0,0) 11287976->1777001188 (-1,0,0,0,0,0) -58372795 c.f + b.g, {b.d + c.e + c.f + b.g} (∞,0,0,0,0,0) -58372795->945131307 (-1,0,0,0,0,0) -1092705565 f, {e,f} (∞,0,0,0,0,0) -58372795->-1092705565 (-1,0,0,0,0,0) -1478041764 ABCACB, {ABC} (∞,0,0,0,0,0) -1478041764->11287976 (-1,0,0,0,0,0) -1478041764->-58372795 (-1,0,0,0,0,0)
Figure 5.7: The subgraph of Figure 5.6 that actually is used in equiv.io, disregarding some attacker options.

Still, nondeterminism in the transition system might lead to exponentially-sized derived games. Especially in the case of bisimilarity and similarity, such a blow-up is not necessary. As Chapter 4 has shown, they should be \textsf{P}-easy.

5.3.2 Regaining Polynomiality in Derived Games

So far, the derived games include the exponentiality due to the subset construction. But often, we can restrict the attacker to only use a polynomially-sized portion of the game. If they have energy for unbounded conjunctions, this restriction will not affect their wins.

Proposition 5.2 (Defender restriction) If the attacker wins (\smash{\color{gray}[}p, Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e) in a derived preorder game \mathcal{G}_{\triangle N} or \mathcal{G}_{\blacktriangle N}, they also win (\smash{\color{gray}[}p, Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e) for all Q' \subseteq Q.

Proof. If the attacker wins \smash{\color{gray}[}p, Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} with e in a spectroscopy game, they also win \smash{\color{gray}[}p, Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} with e for all Q' \subseteq Q. This is a side benefit of the spectroscopy characterization (Lemma 5.1 and 5.2) through distinctions, as Q \cap \llbracket \varphi \rrbracket = \varnothing implies Q' \cap \llbracket \varphi \rrbracket = \varnothing for any \varphi. We can lift this result immediately to the derived preorder games as in Theorem 5.5.

Lemma 5.5 (Conjunctive attacks) If the attacker wins (\smash{\color{gray}[}p, Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e) with \smash{|{Q}|} > 1 in a derived preorder game with e \geq (0,\infty,\infty,\infty,0,0), then they can also win without using any observation moves of the form (\smash{\color{gray}[}p, Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e) \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}(\smash{\color{gray}[}p', Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e').

Proof. Any observation move (\smash{\color{gray}[}p, Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e) \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}(\smash{\color{gray}[}p', Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e') must be due to a transition p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{α}$}}} p' with Q \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{α}$}}} Q'. Instead of the observation, the attacker can move to a conjunction (\smash{\color{gray}[}p, Q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e) \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}(\smash{\color{gray}(}p, Q, \varnothing\smash{{\color{gray})}_\mathtt{d}^{\color{gray}\scriptscriptstyle}}, e). After the defender choice of q \in Q, the game continues with the same energy \dots \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}(\smash{\color{gray}[}p, q\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle\wedge}}, {\color{RoyalBlue}e}) \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}(\smash{\color{gray}[}p, \{q\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e) \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}(\smash{\color{gray}[}p', \operatorname{Der}(q, α)\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}, e'), thanks to the sufficient energy budget. As \operatorname{Der}(q, α) \subseteq Q', we can use Proposition 5.2.

Thus the closure of a logic under conjunctions allows us to use a game that, practically, leaves out many formulas, without losing distinctiveness. This trick is basically the same as in the crucial \langle \alpha \rangle-case of Lemma 2.7 that “game HML” \mathcal{O}^{}_{\mathrm{\lfloor B \rfloor}} and \mathsf{HML} are equally distinctive.

As a consequence, we can obtain a polynomial complexity bound for notions that do not restrict conjunctions and positive conjuncts.

Lemma 5.6 (Polynomial equivalence checking) For a strong notion N \in \{0, 1, \infty\}^6 with N \geq (0,\infty,\infty,\infty,0,0), and a system (\mathcal{P},\mathit{Act},\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}), one can decide p \preceq_{\mathcal{O}^{}_{N}} q in polynomial time, by computing who wins the N-preorder game in \mathit{O}(\smash{|{\mathcal{P}}|} \cdot \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|}) time and space.

Proof. We can use the clever version of the strong spectroscopy game \mathcal{G}_{\blacktriangle} to decide individual equivalences for these coordinates by Theorem 5.5 and Theorem 5.3. For N \geq (0,\infty,\infty,\infty,0,0), this also works on the subgraph where nondeterminism is resolved immediately thanks to Lemma 5.5.

We want to use that, according to Proposition 2.9, deciding a reachability game (G,G_{\mathrm{d}},\mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}) takes \mathit{O}(\smash{|{\mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}}|}) time and \mathit{O}(\smash{|{G}|}) space.

We observe that the \{0,1,\infty\}-valued energy components in the game might only create a constant-factor increase in the size of \mathcal{G}_{\blacktriangle N}, compared to the underlying game \mathcal{G}_{\blacktriangle}.11 Therefore, the following arguments focus on the latter.

11  If we were to allow k-step equivalences as in Figure 4.5, k would also become a factor.

There are at most \smash{|{\mathcal{P}}|}^2 positions of the form \smash{\color{gray}[}p,\{q\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}. Whenever they reach \smash{\color{gray}[}p',Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} with \smash{|{Q'}|} > 1, Lemma 5.5 allows us to prune away all observation moves deriving from there, and return to an attacker main position with \smash{|{Q''}|} \leq 1. The intermediate \smash{\color{gray}[}p',Q'\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}-positions are a function of initial q and the transitions from p, and thus collectively bounded by \mathit{O}(\smash{|{\mathcal{P}}|} \cdot \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|}), which bounds attacker positions as a whole.

In the clever spectroscopy game \mathcal{G}_{\blacktriangle}, there is a maximum of only five defender positions per such attacker position. Also, the subsequent attacker conjunct positions, bounded by \smash{|{\mathcal{P}}|}^2, do not affect the bound.

For the moves, only observation moves and conjunct answers can impact complexity. The observations are bounded in \mathit{O}(\smash{|{\mathcal{P}}|} \cdot \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|}), and the conjunct answers in \mathit{O}(\smash{|{\mathcal{P}}|}), which is dominated by the first.

Inserting our bounds in Proposition 2.9, we obtain time and space complexity of \mathit{O}(\smash{|{\mathcal{P}}|} \cdot \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|}).12

12  This is with the understanding that one can ignore storage space for the positions: One can use pointers to Q'-sets in the attacker and defender positions, and not store them verbatim. This saves the bound as there can only be \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|} such sets of size \smash{|{Q'}|} > 1. So, overall, these sets also will take up \mathit{O}(\smash{|{\mathcal{P}}|} \cdot \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|}) space.

Example 5.7 (Measurements of derived games) Let us examine how the instance game sizes behave on the games of Example 5.6! Figure 5.8 maps out the sizes of game instantiations for the preorders of the strong spectrum as in Figure 3.8.13 Each game is derived from the clever spectroscopy game, with pruning and with capped nondeterminism where possible; to enable equivalence checks, the games combine the parts under \smash{\color{gray}[}\mathsf{ABCACB}, \{\mathsf{ABC}\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}} and under \smash{\color{gray}[}\mathsf{ABC}, \{\mathsf{ABCACB}\}\smash{{\color{gray}]}_\mathtt{a}^{\color{gray} \scriptscriptstyle}}. The game size is defined as the sum of positions and moves, \smash{|{\mathcal{G}}|} = \smash{|{G}|} + \smash{|{\mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}}}|}. Red parts symbolize bigger game graphs.

13  The reported numbers are produced via sbt "shared/run eqchecks --strong-game" for the pair L50/R50 by scalatool.benchmark.LTBTSEquivalenceChecks.

Figure 5.8: Instance game sizes of Example 5.7.

The data match our thoughts on game sizes in Section 5.3.1. For instance, around the trace game \mathcal{G}_{\blacktriangle \mathrm{T}}, we can observe that zero-components usually reduce the game graph size. Between mutual simulation \mathcal{G}_{\blacktriangle \mathrm{1S}} and bisimulation \mathcal{G}_{\blacktriangle \mathrm{B}}, one can see that \infty-components and 0-components are usually better than 1-components. The game for ready traces \mathcal{G}_{\blacktriangle \mathrm{RT}}, where all dimensions play a role, is the most costly.

5.4 Discussion

With this chapter, we have broadened the spectroscopy game approach of Chapter 4 to account for the full strong spectrum of Chapter 3, thereby solving its spectroscopy problem (Problem 3.1).

One game, many notions.   The critical ingredient has been to cover trace-like observations through a subset construction on states (Idea 5.1). This construction can also be viewed game-theoretically as a way to model an attacker with imperfect information about the exact choices the defender makes in simulating steps. The conjunction and negation points then describe moves where the attacker can obtain this information. Fahrenberg & Legay (2014) employ this alternative view in their game description for quantitative variants of strong equivalences.

All prior publications with generalized game characterizations of the spectrum describe a hierarchy of reachability games—as opposed to our view of one energy game per system.

The general idea of giving generalized games for the strong spectrum first appears in Shukla et al. (1996). It receives a fuller treatment by Chen & Deng (2008). Both publications, however, use word-transition moves for trace-like equivalences. In algorithms, this is unfortunate, since most interesting systems allow infinitely long transition sequences: For finite-state systems, this infinity appears as soon as there is a transition cycle. Therefore, the subset construction (or imperfect-information view) is technologically superior. On the side of theory, the link between moves in the game and conjunctions in modal logics adds clarity to our construction. It reinforces the idea of Section 3.3.2 that equivalence checking is, in a way, subtraction of satisfied formulas.

Difference to original formulation.   This chapter’s presentation improves in several ways on my original spectroscopy games. The idea to alternate state subsets for nondeterministic words and conjunction moves to eliminate the blow-up is introduced by Bisping & Nestmann (2021). Our initial 2021 game is unable to correctly handle failure-traces and similar observations, which has been corrected in Bisping et al. (2022), thanks to Jansen’s input. With respect to Bisping et al. (2022), the presentation in this chapter has three advantages:

  1. Bisping et al. (2022) uses a reachability game, on which we construct distinguishing formulas. The formulas are then pruned on-the-fly to select those with minimal syntactic prices. Introduced by Bisping (2023a), we now can perform the whole spectroscopy on energy vectors, thereby making costly explicit formula construction optional.
  2. Bisping et al. (2022)’s game has super-exponential out-degree for conjunction moves. With the present formulation (from Bisping, 2023a), we can achieve constant degree, using the cleverness of Section 5.2.2.
  3. On a pure reachability game, one cannot easily instantiate to select the subgraphs for individual equivalences as in Section 5.3.

Back to many games.   The point of deriving equivalence games from the energy game (Idea 5.2) connects the one-energy-game approach back to the hierarchy-of-games approach of prior publications. With Section 5.3, the present chapter has moved beyond the scope of Bisping (2023a). Interestingly, Section 5.3.2 shows that, by prioritizing conjunctions in derived simulation-like games, one obtains \mathit{O}(\smash{|{\mathcal{P}}|} \cdot \smash{|{\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}}|}) complexity, restoring the \textsf{P}-easiness of the preceding chapter. For strong similarity, this matches the best known time bound, as discussed in Section 3.3.3. For bisimilarity, however, partition refinement outperforms the game approach.

We could go a step further in the polynomially-sized derivatives of the spectroscopy game, and “bake together” the attacker main positions after observations with the following defender positions. This would (almost) arrive at the game structure of last chapter’s bisimulation energy game! Conceptionally, the following relation emerges: The bisimulation game \mathcal{G}_{\mathrm{B}} of Chapter 2 is a shadow of the bisimulation energy game \mathcal{G}_{\mathrm{B}}^{\smash{🗲 }} of Chapter 4, which in turn is a shadow of the strong spectroscopy game \mathcal{G}_{\triangle} of the present chapter.

The dimensions of energy games allow us to encode different games within one game. This is analogous to stereoscopic pictures, decodable by 3D glasses (Figure 5.9).

What's next?   Continuing the trajectory of shadows, Part III of the thesis will abstract further what we have been doing. The strong spectrum of equivalences is usually too strong for the analysis of concurrent systems. Therefore, we will extend our approach to the weak spectrum of equivalences, accounting for the nuances of silent \tau-steps. This is of double relevance: Practical applications of concurrency theory tend to call for weak semantics, and nobody has previously proposed generalized game characterizations for the weak spectrum, at all.