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, 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: Breaking up observations and conjunctions

Linear-time notions can be addressed in the spectroscopy game by interjecting a subset-construction on defender 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. In Section 5.3, we will discuss how to get rid of the blowup 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 we will explore.

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

Related publications.   This chapter showcases the main result of my paper “Process Equivalence Problems as Energy Games” (Bisping, 2023a).

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 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 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 Spectroscopy 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 of states Q reachable through non-determinism; only at conjunction moves does the defender have to choose a q \in Q. Treating conjunctions more explicitly, will also allow 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, where the fifth stands for negated conjuncts, the third for one of the deepest positive conjuncts and the fourth for the other positive 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 Definition 3.7.

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

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

On the processes of Example 5.1, the attacker would move: \begin{array}{rcl} {{\color{gray}[}\mathsf{a}\ldotp\! \mathsf{b}\ldotp\! \mathsf{a}, \{\mathsf{a}\ldotp\! (\mathsf{a} +\mathsf{b})\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} & \mathrel{\smash{›\!\!\frac{\;-\hat{\mathbf{e}}_{1}\;}{}\!\!›}} & {{\color{gray}[}\mathsf{b}\ldotp\! \mathsf{a}, \{\mathsf{a}, \mathsf{b}\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} \\ & \mathrel{\smash{›\!\!\frac{\;-\hat{\mathbf{e}}_{1}\;}{}\!\!›}} & {{\color{gray}[}\mathsf{a}, \{\mathbf{0}\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} \\ & \mathrel{\smash{›\!\!\frac{\;-\hat{\mathbf{e}}_{1}\;}{}\!\!›}} & {{\color{gray}[}\mathbf{0}, \varnothing{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} \\ & \mathrel{\smash{›\!\!\frac{\;\mathbf{0}\;}{}\!\!›}} & {{\color{gray}(}\mathbf{0}, \varnothing, \varnothing{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle}} \; \mathrel{\smash{{›/\!\!\!\!\frac{\;\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 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 spetroscopy game, the attacker moves: \begin{array}{rcl} {{\color{gray}[}\mathsf{T'_{\tau a a}}, \{\mathsf{T'_{\tau a}}\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} & \mathrel{\smash{›\!\!\frac{\;-\hat{\mathbf{e}}_{1}\;}{}\!\!›}} & {{\color{gray}[}\mathsf{a}\ldotp\! \mathsf{a}, \{\mathsf{a}, \mathsf{a}\ldotp\! \mathsf{a} +\mathsf{b}\ldotp\! \mathsf{b}\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} \\ & \mathrel{\smash{›\!\!\frac{\;\mathbf{0}\;}{}\!\!›}} & {{\color{gray}(}\mathsf{a}\ldotp\! \mathsf{a}, \{\mathsf{a}\ldotp\! \mathsf{a} +\mathsf{b}\ldotp\! \mathsf{b}\}, \{\mathsf{a}\}{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle}} \end{array} Now, the defender has two options.

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

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

The game also allows another path 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 Let us see what our prototype implementation on equiv.io reports about our original example processes of Chapter 2. We can input the philosopher processes of Example 2.2 and Example 2.3, obtaining a tranistion system matching Example 2.1:

Example on equiv.io

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:

- 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.5. Internally this is established by building the spectroscopy game and computing that \mathsf{Win}^{\mathrm{min}}_\mathrm{a}({{\color{gray}[}\mathsf{P}, \{\mathsf{Q}\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\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 updcoming Section 5.1.2 we will also give the rules that the tool uses to construct this witness.

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.11).

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

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

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

TODO: Example graph (just the old one?)

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}) The set of strategy formulas for a game position g and a budget e, \mathsf{Strat}_{\triangle}(g, e), in the context of a strong spectroscopy game \mathcal{G}_{\triangle}^{\mathcal{S}} is defined inductively by the following rules: \dfrac{ \begin{matrix} {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} \mathrel{\smash{›\!\!\frac{\;-\hat{\mathbf{e}}_{1}\;}{}\!\!›}} {{\color{gray}[}p', Q'{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} \quad e' = \mathsf{upd}(-\hat{\mathbf{e}}_{1}, e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\triangle}}({{\color{gray}[}p', Q'{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}) \\ p \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\alpha}$}}} p' \quad Q \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\alpha}$}}} Q' \quad φ ∈ \mathsf{Strat}_{\triangle}({{\color{gray}[}p', Q'{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}, e') \end{matrix} }{ \langle α \rangle φ ∈ \mathsf{Strat}_{\triangle}({{\color{gray}[}p, q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}, e) } \dfrac{ {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} \mathrel{\smash{›\!\!\frac{\;\mathbf{0}\;}{}\!\!›}} {{\color{gray}(}p, Q', Q_*{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle}} \quad e ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\triangle}}({{\color{gray}(}p, Q', Q_*{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle}}) \quad φ ∈ \mathsf{Strat}_{\triangle}({{\color{gray}(}p, Q', Q_*{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle}}, e) }{ φ ∈ \mathsf{Strat}_{\triangle}({{\color{gray}[}p, Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}, e) } \dfrac{ \begin{matrix} {{\color{gray}(}p, Q, \varnothing{\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\wedge}} \quad e_q = \mathsf{upd}(u_q, e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\triangle}}({{\color{gray}[}p, q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\wedge}}) \\ \psi_q ∈ \mathsf{Strat}_{\triangle}({{\color{gray}[}p, q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\wedge}}, e_q) \quad \text{for each } q ∈ Q \end{matrix} }{ \textstyle\bigwedge_{q \in Q} \psi_q ∈ \mathsf{Strat}_{\triangle}({{\color{gray}(}p, Q, \varnothing{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle}}, e) } \dfrac{ \begin{matrix} {{\color{gray}(}p, Q, 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\wedge}} \quad e_q = \mathsf{upd}(u_q, e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\triangle}}({{\color{gray}[}p, q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\wedge}}) \\ \psi_q ∈ \mathsf{Strat}_{\triangle}({{\color{gray}[}p, q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\wedge}}, e_q) \quad \text{for each } q ∈ Q \text{ and } \\ {{\color{gray}(}p, Q, Q_*{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle}} \mathrel{\smash{›\!\!\frac{\;u_*\;}{}\!\!›}} {{\color{gray}[}p, Q_*{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} \quad e_* = \mathsf{upd}(u_*, e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\triangle}}({{\color{gray}[}p, Q_*{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}) \\ \psi_* = \langle α \rangle φ ∈ \mathsf{Strat}_{\triangle}({{\color{gray}[}p, Q_*{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}, e_*) \end{matrix} }{ \textstyle\bigwedge_{q \in Q \cup \{*\}} \psi_q ∈ \mathsf{Strat}_{\triangle}({{\color{gray}(}p, Q, Q_*{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle}}, e) } \dfrac{ \begin{matrix} {{\color{gray}[}p, q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\wedge}} \mathrel{\smash{›\!\!\frac{\;u\;}{}\!\!›}} {{\color{gray}[}p, \{q\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} \quad e' = \mathsf{upd}(u, e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\triangle}}({{\color{gray}[}p, \{q\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}) \\ \langle α \rangle φ ∈ \mathsf{Strat}_{\triangle}({{\color{gray}[}p, \{q\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}, e') \end{matrix} }{ \langle α \rangle φ ∈ \mathsf{Strat}_{\triangle}({{\color{gray}[}p, q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\wedge}}, e) }

\dfrac{ \begin{matrix} {{\color{gray}[}p, q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\wedge}} \mathrel{\smash{›\!\!\frac{\;u\;}{}\!\!›}} {{\color{gray}[}q, \{p\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} \quad e' = \mathsf{upd}(u, e) ∈ \mathsf{Win}_\mathrm{a}^{\mathcal{G}_{\triangle}}({{\color{gray}[}q, \{p\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}) \\ p \neq q \quad \langle α \rangle φ ∈ \mathsf{Strat}_{\triangle}({{\color{gray}[}q, \{p\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}, e') \end{matrix} }{ \neg\langle α \rangle φ ∈ \mathsf{Strat}_{\triangle}({{\color{gray}[}p, q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\wedge}}, e) }

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

The correctness proof proceeds basically as with the bisimulation energy game, 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.1.

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

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

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

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

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

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

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

Remark 5.1 (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 {{\color{gray}[}p, \varnothing{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} \mathrel{\smash{›\!\!\frac{\;\mathbf{0}\;}{}\!\!›}} {{\color{gray}(}p, \varnothing, \varnothing{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle}} with budget \mathbf{0}, while the original definition in Bisping (2023a) would cost them \hat{\mathbf{e}}_{2} for {{\color{gray}[}p, \varnothing{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} \mathrel{\smash{›\!\!\frac{\;-\hat{\mathbf{e}}_{2}\;}{}\!\!›}} {{\color{gray}(}p, \varnothing, \varnothing{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle}}.

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

Still, we can be confident that the conference paper results apply to the present presentation mutatis mutandis.

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 complexity problem on the whole strong spectrum is PSPACE-hard.

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

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

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

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

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

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 of the strong spectrum in Figure 3.7 we actually care about 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.7 only use 0, 1, and ∞ in components, we can employ Lemma 4.7 to slighlty 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.

In this section, 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 following 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 Approximations

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

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

Proof. This is a contrapositive consequence of Lemma 5.2: 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}({{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}).

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

Another important trick to reduce game size, is to first apply bisimulation-minimization to the transition system and then only 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.5 The attacker wins {{\color{gray}[}p, \{q\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} on \mathcal{G}_{\triangle}^{\mathcal{S}} with e precisely if they win {{\color{gray}[}[p]_{\sim_\mathrm{B}}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}, \{[q]_{\sim_\mathrm{B}}\} on \mathcal{G}_{\triangle}^{{\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.2 and Lemma 5.3 to translate these sets to and from the winning budgets.

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

io.equiv.eqfiddle.tool.benchmark.Sizemark uses a small example system from Bisping (2023a) modelling Peterson’s mutual exclusion algorithm. The system has only \left|\mathcal{P}\right| = 20 states, but a lot of non-determinism due to saturation with internal behavior.

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

Figure 5.3 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 four fifth of the graph (leaving 241 thousand positions).

Only applying the bisimulation minimization roughly halves the graph (leaving 661 thousand positions). The bisimulation reduction is suprisingly effective, given that the bisimulation minimized Peterson system still has 19 states, that is, only one less than the originals 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-proporionate 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.

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 \left|Q\right| at conjunction challenges after {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\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 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 positive and negative conjuncts can only appear in certain combinations.

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

Observe that all the coordinates of the strong linear-time–branching-time spectrum 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 {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} \quad \mathrel{\smash{›\!\!\frac{\;\mathbf{0}\;}{}\!\!›}}_\blacktriangle \quad {{\color{gray}(}p,Q \mathbin{\backslash}Q_*, Q_*{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle}} \quad \text{with } Q_* \subseteq Q, to situations where \; Q_* \in \{ \; \varnothing,\quad \{ q \in Q \mid \operatorname{Ini}(q) \subseteq \operatorname{Ini}(p) \},\quad \{ q \in Q \mid \operatorname{Ini}(p) \subseteq \operatorname{Ini}(q) \},\quad \{ q \in Q \mid \operatorname{Ini}(p) = \operatorname{Ini}(q) \} \; \}.

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

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

Theorem 5.4 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( \left|\mathcal{P}\right|^{13} \cdot 2^{12\left|\mathcal{P}\right|} ) time and O( \left|\mathcal{P}\right| \cdot 2^{\left|\mathcal{P}\right|} ) space,

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

Now, the amount of all game positions is bounded by \left|G_{\blacktriangle}\right| \in \left|\mathcal{P}\right| \cdot 2^{\left|\mathcal{P}\right|}.

Concerning the maximal out-degree, now, defender conjunction positions are dominant, o_{\mathrel{\smash{›\!\!\frac{\;\enspace\;}{}\!\!›}}_\blacktriangle} \in \mathit{O}(\left|\mathcal{P}\right|).

Inserting the parameters in the time bounds of Lemma 4.7 yields: \begin{array}{rlccccccc} & O( & o_{\mathrel{\smash{›\!\!\frac{\;\enspace\;}{}\!\!›}}_\blacktriangle} & \cdot & \left|G_\blacktriangle\right|^{2d} & \cdot & (d^2 + 3^{d-1} \cdot d)) \\ = & O( & (\left|\mathcal{P}\right|) & \cdot & (\left|\mathcal{P}\right| \cdot 2^{\left|\mathcal{P}\right|})^{12} & \cdot & (6^2 + 3^{5} \cdot 6) & ) \\ = & O( & \left|\mathcal{P}\right|^{13} \cdot 2^{12\left|\mathcal{P}\right|} & ). \end{array}

For space complexity, only game positions are relevant, \mathit{O}( \left|G_\blacktriangle\right| \cdot 3^{d-1} \cdot d ) = \mathit{O}( \left|\mathcal{P}\right| \cdot 2^{\left|\mathcal{P}\right|} ).

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

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

Figure 5.4 is the lower part of a cube of possible game graph optimizations, where Figure 5.3 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 non-determinism of the Peterson system, which leads to big Q-sets in {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\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 non-determinism due to communication.⁵

⁵  The blowup 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 Individuals Equivalences

As we have seen, the strong spectroscopy characterizes the spectroscopy problem and each individual equivalence (and preorder). This section is about the feasability 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 polynomial portion of equivalence problems.

5.3.1 Deriving Equivalence Games

Let us first explicate how to derive characterize equivalences thrugh reachability games derived accoridng 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 derived from the spectroscopy game (\mathcal{G}_{\triangle}^{\mathcal{S}})^R under starting position ({{\color{gray}[}p,\{q\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}, N).

Theorem 5.5 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 ({{\color{gray}[}p,\{q\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}, N).

Proof. By Theorem 5.1, p \preceq_{\mathcal{O}^{}_{N}} q implies that the defender wins \mathcal{G}_{\triangle}^{\mathcal{S}} from {{\color{gray}[}p,\{q\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} when the attacker starts at energy N. In other words, N \notin \mathsf{Win}_\mathrm{a}({{\color{gray}[}p, \{q\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}) for \mathcal{G}_{\triangle}^{\mathcal{S}}. By Proposition 4.3, this implies ({{\color{gray}[}p, \{q\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\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 \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 The following processes are two of the more complex ones of the separating examples in Glabbeek (2001, p. 59). They are equal with respect to ready traces, but not for simulation-like and possible-future-like equivalences.

Example on equiv.io

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.
    View game. 

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

Figure 5.5: Pruned clever strong spectroscopy game below position {{\color{gray}[}\mathsf{ABCACB}, \{\mathsf{ABC}\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} instantiated to starting energy \mathrm{T} = (\infty, 0,0,0,0,0) to decide trace equivalence.

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

⁶  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 {{\color{gray}[}p, \{q\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\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 subgame used by the tool for Example 5.6, in reality is the one in Figure 5.6.

Figure 5.6: The subgame of Figure 5.5 that actually is used in equiv.io, disregarding some attacker options.

Still, non-determinism 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.

5.3.2 Regaining Polynomiality in Derived Equivalence Games

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

Proof. If the attacker wins {{\color{gray}[}p, Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} with e in a spectroscopy game, they also win {{\color{gray}[}p, Q'{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} with e for all Q' \subseteq Q. This is a side-consequence of the spectroscopy characterization (Lemma 5.2 and 5.3) through distinctions, as Q \cap \llbracket \varphi \rrbracket = \varnothing implies Q' \cap \llbracket \varphi \rrbracket = \varnothing for any \varphi.⁷

⁷ TODO: Try this out in Isabelle project

We can lift this result immediately to the derived preorder games as in Theorem 5.5.

Lemma 5.6 If the attacker wins ({{\color{gray}[}p, Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}, e) with \left|Q\right| > 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 ({{\color{gray}[}p, Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}, e) \mathrel{\smash{›\!\!\frac{\;\enspace\;}{}\!\!›}}({{\color{gray}[}p', Q'{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}, e').

Proof. The move 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 ({{\color{gray}[}p, Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}, e) \mathrel{\smash{›\!\!\frac{\;\enspace\;}{}\!\!›}}({{\color{gray}(}p, Q, \varnothing{\color{gray})}}_\mathtt{d}^{\color{gray}\smash{\scriptscriptstyle}}, e). After the defender choice of q \in Q, the game continues \dots \mathrel{\smash{›\!\!\frac{\;\enspace\;}{}\!\!›}}({{\color{gray}[}p, q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle\wedge}}, e) \mathrel{\smash{›\!\!\frac{\;\enspace\;}{}\!\!›}}({{\color{gray}[}p, \{q\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}, e) \mathrel{\smash{›\!\!\frac{\;\enspace\;}{}\!\!›}}({{\color{gray}[}p', \operatorname{Der}(q, α){\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}, e'), thanks to the sufficient energy budget. As \operatorname{Der}(q, α) \subseteq Q', we can use Proposition 5.1.

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

Lemma 5.7 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_\mathrm{\mathcal{O}^{}_{\mathrm{N}}} q in polynomial time, by computing who wins the N-preorder game in \mathit{O}(\left|\mathcal{P}\right| \cdot \left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right|) time and \mathit{O}(\left|\mathcal{P}\right|^2 \cdot \left|\mathit{Act}\right|) 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 non-determinism is resolved immediately thanks to Lemma 5.6.

We want to use that, according to Proposition 2.9, deciding a reachability game (G,G_{\mathrm{d}},\mathrel{\smash{›\!\!\frac{\;\enspace\;}{}\!\!›}}) takes \mathit{O}(\left|\mathrel{\smash{›\!\!\frac{\;\enspace\;}{}\!\!›}}\right|) time and \mathit{O}(\left|G\right|) 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}.⁸ Therefore, the following arguments focus on the latter.

⁸  If we were to allow k-step equivalences as in Figure 4.4, the k would also become a factor.

Lemma 5.6 allows us to prune away all moves deriving from observations from {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} with \left|Q\right| > 1. The pruning restricts the possibilities of Q that can appear on the right-hand side of {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}-positions to the sets \operatorname{Der}(\cdot, \cdot), that is, to \left|\mathcal{P}\right| \cdot \left|\mathit{Act}\right| options. Therefore, these attacker positions are bounded by \mathit{O}(\left|\mathcal{P}\right|^2 \cdot \left|\mathit{Act}\right|).

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

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

Inserting our bounds in Proposition 2.9, we get a time complexity of \mathit{O}(\left|\mathcal{P}\right| \cdot \left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right|) and \mathit{O}(\left|\mathcal{P}\right|^2 \cdot \left|\mathit{Act}\right|) space.⁹

⁹  This is with the understanding that the \mathit{O}(\left|\mathcal{P}\right|^2 \cdot \left|\mathit{Act}\right|) is dominated by \mathit{O}(\left|\mathcal{P}\right| \cdot \left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right|) with respect to time—of course, each position must be constrcucted at some point.

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

Figure 5.7: 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 costy.

TODO: Maybe also example where non-determinism has more effect?

5.4 Discussion

• Mention option of non-perfect attacker information as alternative to subset construction
• Difference to Bisping et al. (2022):
  • Lower exponentiality in conjunctions
  • No explicit construction of formulas
• highlight analogy to apartness (Geuvers & Jacobs (2021))
• mention that \mathit{O}(\left|\mathcal{P}\right| \cdot \left|\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}\right|) matches best algos for simulation, but not for bisimulation.

Bisping, B. (2023a). Process equivalence problems as energy games. In C. Enea & A. Lal (Eds.), Computer aided verification (pp. 85–106). Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-37706-8_5

Bisping, B. (2023b). Process equivalence problems as energy games. Technische Universität Berlin. https://doi.org/10.48550/arXiv.2303.08904

Bisping, B., Jansen, D. N., & Nestmann, U. (2022). Deciding All Behavioral Equivalences at Once: A Game for Linear-Time–Branching-Time Spectroscopy. Logical Methods in Computer Science, 18(3). https://doi.org/10.46298/lmcs-18(3:19)2022

Geuvers, H., & Jacobs, B. (2021). Relating apartness and bisimulation. Logical Methods in Computer Science, 17(3). https://doi.org/10.46298/LMCS-17(3:15)2021

Glabbeek, R. J. van. (2001). The linear time–branching time spectrum I: The semantics of concrete, sequential processes. In J. A. Bergstra, A. Ponse, & S. A. Smolka (Eds.), Handbook of process algebra (pp. 3–99). Elsevier. https://doi.org/10.1016/B978-044482830-9/50019-9

Martens, J., & Groote, J. F. (2023). Computing Minimal Distinguishing Hennessy-Milner Formulas is NP-Hard, but Variants are Tractable. In G. A. Pérez & J.-F. Raskin (Eds.), 34th international conference on concurrency theory (CONCUR 2023) (Vol. 279, pp. 32:1–32:17). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2023.32