5 Spectroscopy of the Strong Equivalence Spectrum
This section will be filled with contents from Process Equivalence Problems as Energy Games.
5.1 The Strong Spectroscopy Game
5.1.1 The Game
Definition 5.1 For a system \mathcal{S}=(\mathcal{P},\mathit{Act},\xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{}$}}}), the 6-dimensional spectroscopy energy game \mathcal{G}_{\triangle}^{\mathcal{S}}[g_0,e_0]=(G,G_{{\mathrm{d}}},\mathrel{\smash{›\!\!\frac{\quad}{}\!\!›}},w,g_{0},e_0) consists of
- attacker positions {{\color{gray}[}p,Q{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}} \in G_{\mathrm{a}},
- attacker clause 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}
A schematic representation can be seen in Figure 5.1.
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{max}}_\mathrm{d}({{\color{gray}[}p_0, \{q_0\}{\color{gray}]}}_\mathtt{a}^{\color{gray}\smash{\scriptscriptstyle}}).1
1 Proof in Lemma 1 of Bisping (2023).
5.1.2 Correctness
5.1.3 Complexity
5.2 More Specific Games
5.2.1 The Clever Game
5.2.2 Instance Games
5.3 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