Linear-Time–Branching-Time Spectroscopy Accounting for Silent Steps

Benjamin Bisping10000-0002-0637-0171 David N. Jansen20000-0002-6636-3301

B. Bisping and D. N. Jansen

Technische Universität Berlin, Germany

State Key Laboratory of Computer Science, Institute of Software,
Chinese Academy of Sciences, Beijing, China

We provide the first generalized game characterization of van Glabbeek's linear-time–branching-time spectrum with silent steps.
Thereby, one multi-dimensional energy game can be used to decide a wide array of behavioral equivalences between stability-respecting branching bisimilarity and weak trace equivalence in one go.
To establish correctness, we relate attacker-winning energy budgets and distinguishing sublanguages of Hennessy–Milner logic characterized by eight dimensions of formula expressiveness.

§ INTRODUCTION: MECHANIZING THE SPECTRUM

Van Glabbeek's “linear-time–branching-time spectrum” of behavioral equivalences [11, 12, 13] has long been one of the fundamental pillars of research in concurrency theory.
Its two parts bring order to the zoo of equivalences.
But still, it is difficult to navigate, in particular, the second part [12], which considers equivalences that abstract from “internal” behavior, expressed by “silent” $\tau$-steps.
Abstracting internal behavior is crucial to model communication happening without participation of the observer.

This paper is about turning the silent-step linear-time–branching-time spectrum of [12] into an algorithm.
This means that researchers can provide a set of processes that ought to be equated (or distinguished) for their use case, and our algorithm can tell them “where” in the spectrum this set of (in-)equivalences holds;
it performs a spectroscopy, so to speak.

We follow our recent approach from [5, 4] to use a generalized bisimulation game
with moves corresponding to sets of conceivable distinguishing formulas that matter for the equivalences considered.
The core insight is that formulas can be partially ordered by the amount of Hennessy–Milner logic expressiveness they use in a way that aligns with the spectrum.

The game can then be understood as a multi-weighted energy game [4, 7, 15] where moves use up attacker's resources to distinguish processes.
Thereby, defender-won energy levels reveal non-distinguishing subsets of Hennessy–Milner logic (HML) and thus sets of maintained equivalences.

At its core, this paper extends the spectroscopy energy game of [4] by modalities needed to cover the weak equivalence spectrum of [12], namely, delayed observations, stable conjunctions, and branching conjunctions.
More precisely:

* In <ref>, we capture a big chunk of the linear-time–branching-time spectrum with silent steps by measuring expressive powers used in a HML-subset that corresponds to stability-respecting branching bisimilarity.

* In <ref>, we adapt the spectroscopy energy game of [4] to account for silent-step equivalences, including distinctions in terms of delayed observations ($\hmlEps\hmlObs{a}\ldots$), stable conjunctions ($\hmlAndS\{\hmlNeg\hmlObs{\tau}\hmlTrue, \ldots\}$), and branching conjunctions ($\hmlEps\hmlAndS\{\hmlObs{a}\ldots, \hmlEps\ldots\}$).

* <ref> proves that winning energy levels and equivalences coincide by closely relating distinguishing formulas and ways the attacker may win the energy game.

* <ref> lays out how to use the game to decide all equivalences at once, how to do so in exponential time, and how to decide even more (divergence-preserving) equivalences.

§ DISTINCTIONS AND EQUIVALENCES
IN SYSTEMS WITH SILENT STEPS

This paper follows the paradigm that equivalence is the absence of possibilities to distinguish.
We begin by introducing
distinguishing Hennessy–Milner logic formulas (<ref>),
the subset we will use in this paper (<ref>) and
a quantitative characterization of equivalences in terms of distinctive capabilities (<ref>)

§.§ Transition Systems and Hennessy–Milner Logic

[Dining hall philosophers]

Consider the following two processes from Bisping and Montanari [6], which reproduce an example from compile-time optimizations by Bell [2]. (We use Milner's [16] notation for $\ccs$-processes.)

\begin{align*}
\ccsIdentifier {P_c} \ccsDef &
\left(\, \action{pl} \ccsPrefix \action{sp} \ccsPrefix \action{aEats}\,
\ccsPar \, \action{pl} \ccsPrefix \action{sp} \ccsPrefix \action{bEats}\,
\ccsPar \, \ccsOutm{\action{pl}} \,
\ccsPar \, \action{op} \ccsPrefix \ccsOutm{\action{sp}} \,
\right)\;\ccsHide\:\{\action{pl}, \action{sp}\}\\
\ccsIdentifier {P_p} \ccsDef &
\left(\,
\action{pl} \ccsPrefix \action{op} \ccsPrefix \action{sp} \ccsPrefix \action{aEats}\,
\ccsPar \, \action{pl} \ccsPrefix \action{op} \ccsPrefix \action{sp} \ccsPrefix \action{bEats}\,
\ccsPar \, \ccsOutm{\action{pl}} \,
\ccsPar \, \ccsOutm{\action{sp}} \,
\right)\;\ccsHide\:\{\action{pl}, \action{sp} \}
\end{align*}

Both systems each model a pair of philosophers $\ccsIdentifier A$ and $\ccsIdentifier B$ who race for resources.
First, they need to get a plate $\action{pl}$, then spaghetti $\action{sp}$, finally they eat $\action{aEats}$ or $\action{bEats}$.
In $\ccsIdentifier{P_c}$ the spaghetti becomes available once the dining hall counter opens $\action{op}$.
In $\ccsIdentifier{P_p}$ it's the philosophers waiting for $\action{op}$, before grabbing the spaghetti.
<ref> shows a corresponding transition system, where internal communication is represented by $\tau$-transitions.
As the race is already settled once the only plate has been taken, the difference between the systems seems to be mostly … philosophical.
But many notions of equivalence consider the systems to be different.
In the rest of the subsection we will formalize how different they are.

scale=.9, center
[->,auto,node distance=2cm, rel/.style=dashed,font=, blue, ext/.style=line width=1pt]

(Pp) [right of=Pc, node distance=5cm] $\ccsIdentifier{P_p}$;

(A1) [below right of=Pc, node distance=1.5cm] $\circ$;
(A2) [below of=A1, node distance = 1.3cm] $\circ$;
(A3) [below of=A2, node distance = 1.0cm] $\ccsIdentifier A$;

(B1) [below left of=Pp, node distance=1.5cm] $\circ$;
(B2) [below of=B1, node distance = 1.3cm] $\circ$;
(B3) [below of=B2, node distance = 1.0cm] $\ccsIdentifier B$;

(Stop) [below left = .2cm and 1cm of B3] $\ccsStop$;

(AB) [above of=Stop, node distance = 2.3cm] $\ccsIdentifier{AB}$;

(Pc) edge [bend right=10, swap] node $\tau$ (A1)
(A1) edge [bend right=10, swap, ext] node $\action{op}$ (A2)
(A2) edge [bend right=10, swap] node $\tau$ (A3)
(A3) edge [bend right=5, swap, ext] node $\action{aEats}$ (Stop)
(Pc) edge [bend left=10, pos=0.3] node $\tau$ (B1)
(B1) edge [bend left=10, ext] node $\action{op}$ (B2)
(B2) edge [bend left=10] node $\tau$ (B3)
(B3) edge [bend left=5, ext] node $\action{bEats}$ (Stop)
(Pc) edge [bend left=15, ext] node [pos=0.9] $\action{op}$ (AB)
(AB) edge [bend left=10] node $\tau$ (A2)
(AB) edge [bend right=10, swap] node $\tau$ (B2)

(Pp) edge[bend right=10, swap, pos=0.3] node $\tau$ (A1)
(Pp) edge[bend left=10] node $\tau$ (B1)

The philosopher system from <ref>.

A labeled transition system is a tuple $\system=(\proc,\actions,\step{})$ where $\proc$ is the set of processes, $\actions$ is the set of actions, and ${\step{}}\subseteq \proc\times\actions\times \proc$ is the transition relation.

$\tau \in \actions$ labels silent steps and $\stepWeak$ is notation for the reflexive transitive closure of internal activity $\step{\tau}^*$.
The name $\varepsilon \notin \actions$ is reserved and indicates no (visible) action.
A process $p$ is called stable if .

We implicitly lift the relations to sets of processes $P \step{\alpha} P'$ (with $P, P' \subseteq \proc$, $\alpha \in \actions$), which is defined to be true if $P' = \{ p' \in \proc \mid \exists p \in P \ldotp p \step{\alpha} p'\}$.

The syntax of Hennessy–Milner logic over a set $\actions$ of actions, $\hmlA$, is defined through the grammar with start symbol $\varphi$:

\begin{align*}
\varphi {} ::= {} & \hmlObs{\alpha}\varphi & \text{with } \alpha \in \actions \\
| \quad & \hmlEps\varphi \quad | \quad \hmlTauOpt\varphi\\
| \quad & \hmlAndS \{\psi, \psi, ...\} \\
\psi {} ::= {}    & \hmlNeg \varphi \mid \varphi.
\end{align*}

Its semantics $\;\smash{\hmlSemantics{\;\cdot\;}{\system}{}}$ over a transition system $\system=(\proc,\actions,\step{})$ is given as the set of processes where a formula “is true” by:

\begin{align*}
\hmlSemantics{\hmlObs{\alpha}\varphi}{\system}{} \defEq &\;
\{p \in \proc \mid
\exists p' \in \hmlSemantics{\varphi}{\system}{} \ldotp p \step{\alpha} p'\}
\\[0.25\baselineskip]
\hmlSemantics{\hmlEps\varphi}{\system}{} \defEq &\;
\{p \in \proc \mid
\exists p' \in \hmlSemantics{\varphi}{\system}{} \ldotp p \stepWeak p'\}
\\[0.25\baselineskip]
\hmlSemantics{\hmlTauOpt\varphi}{\system}{} \defEq &\;
\{p \in \proc \mid
\exists p' \in \hmlSemantics{\varphi}{\system}{} \ldotp p \step{\tau} p'\}
\cup \hmlSemantics{\varphi}{\system}{}
\\[0.25\baselineskip]
\smash{\hmlSemantics{\hmlAndS \Psi}{\system}{}} \defEq &\;
\bigcap \{ \hmlSemantics{\psi}{\system}{} \mid \psi \in \mathit{Pos}(\Psi) \} %\\
\,\;\setminus\;\; %&\;
\bigcup \{ \hmlSemantics{\varphi}{\system}{} \mid
(\hmlNeg \varphi) \in \mathit{Neg}(\Psi) \}
\\*[0.25\baselineskip]
& \text{where } \mathit{Neg}(\Psi) \defEq \{ \psi \in \Psi \mid \exists \varphi \ldotp \psi = \hmlNeg\varphi\} \text{ and } \mathit{Pos}(\Psi) \defEq \Psi \setminus \mathit{Neg}(\Psi) .
\end{align*}

We write $\hmlTrue$ for the empty conjunction $\hmlAndS \varnothing$.
Moreover, to reduce case distinctions we define the notation $\hmlOpt{\alpha}\varphi$ to mean $\hmlObs{\alpha}\varphi$ if $\alpha \neq \tau$,
and analogously write $p \step{\hmlOpt{\alpha}} p'$ if $p \step{\alpha} p'$, or if $\alpha = \tau$ and $p = p'$.

In <ref>, $\varphi_\mathsf{cp} \defEq \hmlEps\hmlObsI{op}\hmlEps\hmlAndS\{\hmlEps\hmlObsI{aEats}\hmlTrue, \hmlEps\hmlObsI{bEats}\hmlTrue \}$ distinguishes $\ccsIdentifier{P_c}$ from $\ccsIdentifier{P_p}$.
$\varphi_\mathsf{cp}$ states that a weak $\action{op}$-step may happen such that, afterwards, a state can be reached from where $\action{aEats}$ and $\action{bEats}$ are possible (after further internal behavior).
This is true of $\ccsIdentifier{P_c}$ because of the $\ccsIdentifier{AB}$-state, but not of $\ccsIdentifier{P_p}$.

A formula $\varphi \in \hmlA$ is said to distinguish a processes $p$ from $q$ iff $p \in \hmlSemantics{\varphi}{\smash{\system}}{}$ and $q \notin \smash{\hmlSemantics{\varphi}{\smash{\system}}{}}$.
The formula is said to distinguish a process $p$ from a set of processes $Q$ iff it distinguishes $p$ from every $q \in Q$.

A sublanguage of Hennessy–Milner logic, $\obs{\mathit N} \subseteq \hmlA$, corresponding to a notion of observability $N$, either distinguishes two processes, $p \not\bPreord{\mathit N} q$, if it contains a distinguishing formula, or otherwise preorders them, $p \bPreord{\mathit N} q$.
If processes are preordered in both directions, $p \bPreord{\mathit N} q$ and $q \bPreord{\mathit N} p$, then they are considered $N\!$-equivalent, $p \bEquiv{\mathit N} q$.

§.§ A Logic for Branching Bisimilarity and Below

The Hennessy–Milner logic of <ref> can be used to characterize strong bisimilarity and coarser equivalences.
In this paper, we direct our attention to those that allow for silent behavior to happen before visible actions are observed.
We thus focus on the following subset of $\hmlA$,
where the brick-red part represents stable conjunctions
and the steel-blue part branching conjunctions:

We characterize stability-respecting branching Hennessy–Milner logic, $\hmlBA \subseteq \hmlA$, by the following context-free grammar starting with $\varphi$:

\begin{align*}
\varphi {} ::= {} & \hmlEps\chi \\*
| \quad & \hmlAndS \{\psi, \psi, ...\} \\
\chi {} ::= {} & \hmlObs{a}\varphi & \text{with } a \in \actions \setminus \{\tau\} \\*
| \quad & \hmlAndS \{\psi, \psi, ...\} \\*
| \quad & \textcolor{stabilityColor}{\hmlAndS \{\neg\hmlObs{\tau}\hmlTrue, \psi, \psi, ...\}} \\*
| \quad & \textcolor{etaColor}{\hmlAndS \{\hmlOpt{\alpha}\varphi, \psi, \psi, ...\}} \\
\psi {} ::= {}    & \hmlNeg\hmlEps\chi \mid \hmlEps\chi.
\end{align*}

[][see full proof, restate]

$\hmlBA$ characterizes stability-respecting branching bisimilarity.

Encode to and from the modal characterization of stability-respecting branching bisimilarity by Fokkink, van Glabbeek and Luttik [8].

Fokkink, van Glabbeek and Luttik [8] gave the following modal characterization of stability-respecting branching bisimilarity
(we adapt their logic to our notation):

\begin{align*}
\upsilon {} ::= {} &
\hmlAnd{i}{I} \upsilon_i \;|\;
\hmlNeg \upsilon \;|\;
\hmlEps(\upsilon \wedge \hmlOpt{\alpha} \upsilon) \;|\;
\hmlEps(\overline{\upsilon} \wedge \neg \hmlObs{\tau}\hmlTrue)\\
\overline{\upsilon} {} ::= {} &
\hmlAnd{i}{I} \overline{\upsilon}_i \;|\;
\hmlNeg \overline{\upsilon} \;|\;
\hmlObs{\alpha} \upsilon \;|\;
\upsilon
\end{align*}

Formulas of the form $\upsilon$ characterize stability-respecting branching bisimilarity,
and formulas of the form $\overline{\upsilon}$ characterize its rooted variant.
The two notions coincide on stable processes.

We can prove the proposition by showing that their and our modal characterization can be transformed into each other.
Some formulas cannot be transformed, but they are not relevant to distinguish processes:
If a negated conjunction (a disjunction) $\hmlNeg\hmlAnd{i}{I} \upsilon_i$ distinguishes $p$ from $Q$,
then there is some $i \in I$ such that $p \in \hmlSemantics{\hmlNeg \upsilon_i}{}{}$ and $Q \cap \hmlSemantics{\hmlNeg \upsilon_i}{}{} = \varnothing$,
so $\hmlNeg \upsilon_i$ also distinguishes $p$ from $Q$.
Further, if a double negation $\hmlNeg\hmlNeg \upsilon$ distinguishes $p$ from $Q$,
then also $\upsilon$ does.
We can therefore restrict negative $\upsilon$-formulas
to those of the form $\hmlNeg\hmlEps(\upsilon \wedge \hmlOpt{\alpha} \upsilon)$
and $\hmlNeg\hmlEps(\overline{\upsilon} \wedge \neg \hmlObs{\tau}\hmlTrue)$.

To translate a (positive or restricted negative) $\upsilon$-formula
to a $\varphi$-formula, we can define a mapping $\Phi$,
together with a mapping $\overline{\Phi}$ that translates $\overline{\upsilon}$-formulas.
The latter will only be used on stable processes and it only needs to preserve truth values on these,
so we can liberally insert $\hmlEps$-operators

and set
$\overline{\Phi}(\hmlObs{\tau} \upsilon) := \hmlAndS\{\hmlNeg\hmlEps\hmlTrue\}$.

For the rest, the translation is straightforward.

For the other direction, we can define a mapping from $\varphi$-formulas to $\upsilon$-formulas.
The only nontrivial case is the $\hmlEps$-operator,
which can be translated by
$\Upsilon(\hmlEps\chi) := \hmlEps(\Upsilon(\chi) \wedge \hmlTauOpt \hmlTrue)$.

In conclusion, the two languages distinguish the same processes,
which proves our claim.

§.§ Price Spectra of Behavioral Equivalences

max width=
[auto,node distance=2.5cm,align=center]
(BBs)stability-respecting  branching bisim $\eqName{BB^{\color{stabilityColor}sr}}$

(BB)[below left of=BBs]branching bisim $\eqName{BB}$

(eB)[xshift=-5mm, below left of=BB]$\eta$-bisim $\eqName{\eta}$

(DB)[below right of=BB]delay bisim $\eqName{DB}$

(B)[below left of=DB]weak bisim $\eqName{B}$

(S2)[below left of=B]$2$-nested sim $\eqName{2S}$

(C)[below right of=B]contrasim $\eqName{C}$

(RS)[below left of=S2]ready sim $\eqName{RS}$

(R)[below right of=RS]readiness $\eqName{R}$

(PF)[above right of=R] possible futures $\eqName{PF}$

(IF)[below right of=PF]impossible futures $\eqName{IF}$

(S)[below left of=RS]sim $\eqName{1S}$

(eS)[above left of=RS]$\eta$-sim $\eqName{\eta S}$

(F)[below right of=R]failures $\eqName{F}$

(T)[below left of=F]traces $\eqName{T}$

(DBs)[xshift=12mm, above right of=DB, node distance=1.75cm]s.-r. delay bisim $\eqName{DB^{sr}}$

(SB)[below right of=DBs]stable bisim $\eqName{SB}$

(Cs)[below right of=SB]stable contrasim $\eqName{C^s}$

(RSs)[below left of=SB]stable ready sim $\eqName{RS^s}$

(Rs)[below of=RSs, node distance=3cm]stable readiness $\eqName{R^s}$

(IFs)[below of=Cs, node distance=3cm]stable impos. fut. $\eqName{IF^s}$

(Fs)[below right of=Rs]stable failures $\eqName{F^s}$

(BBs) edge (BB)
(BB) edge ([xshift=10mm]eB.north)
(BB) edge (DB)
([xshift=10mm]eB.south) edge (B)
(eB.south) edge (eS)
(DB) edge (B)
(B) edge (S2)
(B) edge (C)
(C) edge (IF)
(S2) edge (RS)
(S2) edge (PF)
(RS) edge (S)
(RS) edge (R)
(PF) edge (R)
(PF) edge (IF)
(eS) edge (S)
(S) edge (T)
(IF) edge (F)
(R) edge (F)
(F) edge (T)

(BBs) edge (DBs)
([xshift=-4mm]DBs.south) edge ([xshift=-9mm,yshift=-5mm]DBs.south)
(DBs) edge (SB)
(SB) edge (RSs)
(SB) edge (Cs)
(Cs) edge (IFs)
(RSs) edge (Rs)
(Rs) edge (Fs)
(IFs) edge (Fs)
(Fs) edge ([xshift=30mm]T.east)
([xshift=30mm]T.east) edge (T.east)

Hierarchy of equivalences/preorders becoming finer towards the top.

Van Glabbeek [12] uses about 20 dimensions to characterize 155 “notions of observability” (derived from five dimensions of testing scenarios).
These then entail behavioral preorders and equivalences given as modal characterizations.
In this subsection, we recast the notions of observability as coordinates in a (more quantitative) 8-dimensional space of HML formula expressiveness.

We will “price” formulas of $\hmlBA$ by vectors we call energies. The pricing allows to conveniently select subsets of $\hmlBA$ in terms of coordinates.

We denote as energies, $\energies$, the set of $8$-dimensional vectors $(\nats)^8$, and as extended energies, $\energies_\infty$, the set $(\nats\cup\{\infty\})^8$.

We compare (extended) energies component-wise: $\vectorComponents[8]{e} \leq \vectorComponents[8]{f}$ iff $e_i \leq f_i$ for each $i$.
Least upper bounds $\sup$ are defined as usual as component-wise supremum.

We write $\unit{i}$ for the standard unit vector where the $i$-th component is $1$ and every other component equals $0$. $\zeroVec$ is defined to be the vector $(0,0, \ldots, 0)$. Vector addition and subtraction happen component-wise as usual.

In <ref>, we order the equivalences along dimensions of $\hmlBA$-expressiveness they use in terms of operator depths (maximal occurrences of an operator on a path from root to leaf in the abstract syntax tree).
Intuitively, the dimensions are:

* Modal depth (of observations $\hmlObs{\alpha}$, $\hmlOpt{\alpha}$),

* Depth of branching conjunctions (with one observation clause not starting with $\hmlEps$),

* Depth of instable conjunctions (that do not enforce stability by a $\hmlNeg \hmlObs{\tau} \hmlTrue$-conjunct),

* Depth of stable conjunctions (that do enforce stability by a $\hmlNeg \hmlObs{\tau} \hmlTrue$-conjunct),

* Depth of immediate conjunctions (that are not preceded by $\hmlEps$),

* Maximal modal depth of positive clauses in conjunctions,

* Maximal modal depth of negative clauses in conjunctions,

* Depth of negations.

The expressiveness price $\expr \colon \! \hmlBA \rightarrow \energies_\infty$ of a formula
is defined in mutual recursion with helper functions $\expr^\varepsilon$ for $\chi$-productions and $\expr^\wedge$ for $\psi$;
if multiple rules apply to a formula, pick the first one:

\begin{align*}
\expr\left(\hmlTrue\right) \defEq
\expr^\varepsilon\left(\hmlTrue\right) & \defEq
\zeroVec
\\
\textstyle\expr\left(\hmlEps\chi\right) & \defEq
\textstyle\expr^\varepsilon\left(\chi\right)
\\
\textstyle\expr\left(\hmlAndS\Psi\right) & \defEq
\unit{5} + \textstyle\expr^\varepsilon\left(\hmlAndS \Psi\right)
\\
%\expr^\varepsilon\left(\hmlObs{\alpha}\varphi\right) \defEq
\expr^\varepsilon\left(\hmlOpt{\alpha}\varphi\right) & \defEq
\unit{1} + \expr(\varphi)
\\
\textstyle\expr^\varepsilon\left(\hmlAndS(\{ \textcolor{etaColor}{\hmlOpt{\alpha}\varphi} \} \cup \Psi) \right) & \defEq
\textcolor{etaColor}{\unit{2}} + \textstyle\expr^\varepsilon\left(\hmlAndS(\{ \hmlEps\hmlOpt{\alpha}\varphi \} \cup \Psi \setminus \{ \hmlOpt{\alpha}\varphi \}) \right)
\\
\textstyle\expr^\varepsilon\left(\hmlAndS \Psi\right) & \defEq
\sup\;\{ \expr^\wedge\left(\psi\right) \mid \psi \in \Psi \}
\begin{cases}
\textcolor{stabilityColor}{\unit{4}} & \text{if } \textcolor{stabilityColor}{\hmlNeg\hmlObs{\tau}\hmlTrue} \in \Psi\\
\unit{3} & \text{otherwise}
\end{cases}
\\
\expr^\wedge\left(\textcolor{stabilityColor}{\hmlNeg\hmlObs{\tau}\hmlTrue}\right) & \defEq
\zeroVec
\\
\expr^\wedge\left(\hmlNeg\varphi\right) & \defEq
\sup\;\{ \unit{8} + \expr\left(\varphi\right) \,,\, (0,0,0,0,0,0,\expr_1\left(\varphi\right),0) \}
\\
\expr^\wedge\left(\varphi\right) & \defEq
\sup\;\{ \expr\left(\varphi\right) \,,\, (0,0,0,0,0,\expr_1\left(\varphi\right),0,0) \}
\end{align*}

$\varphi_\mathsf{cp} = \hmlEps\hmlObsI{op}\hmlEps\hmlAndS\{\hmlEps\hmlObsI{aEats}\hmlTrue, \hmlEps\hmlObsI{bEats}\hmlTrue \}$,
the formula in <ref>, has expressiveness price $\expr(\varphi_\mathsf{cp}) = (2,0,1,0,0, 1,0,0) \leq e_{\mathrm{1S}} = (\infty,0, \allowbreak \infty,0,0,\infty,0,0)$
(and also $\expr(\varphi_\mathsf{cp}) \leq e_{\mathrm{R}}$).

Each language of formulas with prices below a coordinate $e_N$ given in fig:ltbt-spectrum characterizes the named notion of equivalence
through $\obs{\mathit N} = \{ \varphi \mid \expr(\varphi) \leq e_N\}$.

That is, $p \bPreord{\mathit{N}} q$ with respect to notion $N$, iff no $\varphi$ with $\expr(\varphi) \leq e_N$ distinguishes $p$ from $q$.
So, we actually see the notions of preorder / equivalence to be defined through these coordinates.
For stability-respecting branching bisimilarity, where $\obs{\eqName{BB^{sr}}} = \hmlBA$, <ref> establishes that our modal characterization
has the same distinctive power as the one by [8],
although their subset of $\hmlA$ is slightly different from ours.
For other notions, there too are superficial differences. We give two examples.

[Weak trace equivalence and inclusion]
The notion of weak trace inclusion (and equivalence) is defined through $e_{\eqName{T}} = (\infty,0,0,0,0,0,0,0)$ and <ref> inducing $\obs{T}$, the language given by the grammar:

\begin{align*}
\varphi_\eqName{T} \quad ::= \quad & \quad \hmlEps\hmlObs{a}\varphi_\eqName{T}
\quad | \quad \hmlEps\hmlTrue
\quad | \quad \hmlTrue .
\end{align*}

This slightly deviates from languages one would find in other publications. For instance, Gazda et al. [10] do not have the second production. But this production does not increase expressivity, as $\hmlSemantics{\hmlEps\hmlTrue}{}{} = \hmlSemantics{\hmlTrue}{}{} = \proc$.

[Weak bisimulation equivalence and preorder]
The logic of weak bisimulation observations $\obs{WB}$ defined through $e_{\eqName{WB}} = (\infty,0,\infty,0,0,\infty,\infty,\infty)$ equals the language defined by the grammar:

\begin{align*}
\varphi_\eqName{WB} \quad ::= \quad & \hmlEps\hmlObs{a}\varphi_\eqName{WB}
\quad | \quad \hmlEps\hmlAndS \{\psi_\eqName{WB}, \psi_\eqName{WB}, ...\} \\
\psi_\eqName{WB} \quad ::= \quad    & \hmlNeg\varphi_\eqName{WB} \quad \mid \quad \varphi_\eqName{WB}.
\end{align*}

Let us contrast this to the definition for weak bisimulation observations $\obs{WB'}$ from Gazda et al. [10]:

\begin{align*}
\varphi_\eqName{WB'} \quad ::= \quad \hmlEps\varphi_\eqName{WB'}
\quad | \quad \hmlEps\hmlObs{a}\hmlEps\varphi_\eqName{WB'}
\quad | \quad \hmlAndS \{\varphi_\eqName{WB'}, \varphi_\eqName{WB'}, ...\}
\quad | \quad \hmlNeg\varphi_\eqName{WB'}.
\end{align*}

Our $\obs{WB}$ allows a few formulas that $\obs{WB'}$ lacks, such as $\hmlEps\hmlObs{a}\hmlEps\hmlObs{a}\hmlEps\hmlTrue$.
This does not increase expressivity as $\obs{WB'}$ has $\hmlEps\hmlObs{a}\hmlEps\hmlEps\hmlObs{a}\hmlEps\hmlTrue$ and $\hmlSemantics{\hmlEps\hmlEps\varphi}{}{} = \hmlSemantics{\hmlEps\varphi}{}{}$.

For the other direction, there is a bigger difference due to $\obs{WB'}$ allowing more freedom in the placement of conjunction and negation.
In particular it allows top-level conjunctions and negated conjunctions without $\hmlEps$ in between. But these features cannot add distinction power.
Top-level negation in $\obs{WB'}$ however adds distinction power to the preorders, effectively turning them into equivalence relations.
We do not enforce this and thus ${\bPreord{WB}} \neq {\bEquiv{WB}}$ for many systems;
e.g. $\tau \ccsPrefix \action a \bPreord{WB} \tau \ccsChoice \tau \ccsPrefix \action a$, but $\tau \ccsChoice \tau \ccsPrefix \action a \not\bPreord{WB} \tau \ccsPrefix \action a$ due to $\hmlEps\hmlAndS\{\hmlNeg\hmlEps\hmlObs{a}\hmlTrue\}$.
However, as a distinction by $\hmlNeg \varphi$ in one direction implies one by $\varphi$ in the other, we know that this difference is ironed out once we consider the equivalence $\bEquiv{WB}$.

Continuing Examples <ref> and <ref>, $\varphi_\mathsf{cp} \in \obs{WB}$, the language of formulas that characterize weak bisimilarity.
Thus, the formula disproves weak bisimilarity, $\ccsIdentifier{P_c} \not\bEquiv{WB} \ccsIdentifier{P_p}$.
More precisely, $\varphi_\mathsf{cp}$ is from the languages of weak simulation $\obs{WS}$ and of weak instable readiness $\obs{R}$, hence already disproving these two and every finer preorder.
It does not disprove stable bisimulation because $\obs{SB}$ only allows stable conjunctions (i.e. conjunctions with a $\hmlNeg\hmlObs{\tau}\hmlTrue$-conjunct).
Indeed the two processes cannot be distinguished if conjunctions must be stable or may only contain negative conjuncts. They hence are stable bisimilar and contrasimilar.
With this information, we can demarcate in <ref> which equivalences relate $\ccsIdentifier{P_c}$ and $\ccsIdentifier{P_p}$, and which do not.
The following main part of the paper is about how to draw such lines using a quantitative game to reliably rule out that certain $\hmlBA$-sublogics can distinguish processes.

None of the logics in <ref> restrict the first dimension,
but the modal depth is kept to simplify the calculation of dimensions 6 and 7.
It could also be used to define $k$-step bisimilarity and similar notions.

§ A GAME OF DISTINGUISHING CAPABILITIES

After some preliminaries on energy games in <ref>, we present the spectroscopy game accounting for silent steps in three layers:
In <ref>, a variant of the strong bisimulation game is relaxed into a delay bisimulation game by permitting internal behavior to happen before observations.
Then, <ref> adds stable conjunctions, which are used in stable bisimulation and stability-respecting delay bisimulation.
<ref> finally provides “just-before” branching conjunctions, needed for $\eta$-(bi)simulation and branching bisimulation.
To justify the game moves, each subsection explicates what productions of $\hmlBA$-formulas winning attacker moves correspond to.
In <ref>, we will use the correspondence to prove correctness.

<ref> gives a schematic overview of the game rules, where the game continues from the dotted nodes as from the initial node.
The colors differentiate the layers and match the scheme of <ref> and <ref>.

§.§ Declining Energy Games

Equivalence problems of the strong linear-time–branching-time spectrum can be characterized as multi-dimensional energy games as outlined in [4].
In this subsection, we revisit the definitions we will need in this paper.
For a more detailed presentation—in particular on how to compute attacker and defender winning budgets on this class of games—we refer to [4].

The set of energy updates, $\energyUpdates$, contains $\vectorComponents[8]{u} \in \energyUpdates$ where each component is of the form

* $u_k \in \{-1, 0\}$ (relative update), or

* $u_k = \mathtt{min}_D$ where $D \subseteq \{1, \ldots, 8\}$ and $k \in D$ (minimum selection update).

Applying an update to an energy, $\energyUpdate(e, u)$, where $e = \vectorComponents[8]{e} \in \energies_\infty$ and $u = \vectorComponents[8]{u} \in \energyUpdates$, yields a new energy vector $e'$ where $k$th components $e'_k \defEq e_k + u_k$ for $u_k \in \ints$ and $e'_k \defEq \min_{d\in D} e_d$ for $u_k = \mathtt{min}_D$.
Updates that would cause any component to become negative are undefined, i.e., $\energyUpdate$ is a partial function.

An $8$-dimensional declining energy game $\game[g_{0},e_0] = (G, G_\defenderSubscript, \gameMove,\allowbreak w, g_0, e_0)$ is played on a directed graph uniquely labeled by energy updates consisting of

* a set of game positions $G$, partitioned into

* a set of defender positions $G_\defenderSubscript\subseteq G$

* a set of attacker positions $G_\attackerSubscript\defEq G \setminus G_\defenderSubscript$,

* a relation of game moves $\operatorname{\gameMove}\subseteq G \times G$,

* a weight function for the moves $w \colon (\operatorname{\gameMove}) \to \energyUpdates$,

* an initial position $g_{0}\in G$, and

* an initial energy budget vector $e_{0} \in \energies_\infty$.

The notation $g \gameMoveX{u} g'$ stands for $g \gameMove g'$ and $w(g,g') = u$.

We call the (finite or infinite) paths $\rho = g_{0}g_{1}\ldots\in G^{\infty}$ with $g_{i}\gameMoveX{u_i} g_{i+1}$ plays of $\game[g_{0},e_{0}]$.

The energy level of a play at round $i$, $\energyLevel_{\rho}(i)$, is recursively given as
$\energyLevel_{\rho}(0) \defEq e_0$ and otherwise as
$\energyLevel_{\rho}(i+1) \defEq \energyUpdate(\energyLevel_{\rho}(i), u_i)$.

Like $\energyUpdate$, also $\energyLevel$ is a partial function.
Plays where energy levels become undefined (negative) are won by the defender.
So are infinite plays.
If a finite play is stuck (, $g_{0}\dots \mbox{$g_{n} \centernot{\gameMove}$}$), the stuck player loses: The defender wins if $g_{n}\in G_\attackerSubscript$, and the attacker wins if $g_{n}\in G_\defenderSubscript$.

An attacker strategy is a map from play prefixes ending in attacker positions to next game moves
$s \colon (G^* \times G_\attackerSubscript) \to G$ with $s(g_0 \ldots g_\attackerSubscript) \in (g_\attackerSubscript \gameMove \cdot)$.
Similarly, a defender strategy names moves starting in defender states.
If all plays consistent with a strategy $s$ ensure a player to win,
$s$ is called a winning strategy for this player.
The player with a winning strategy for $\game[g_{0},e_0]$ is said to win $\game$ from position $g_{0}$ with initial budget $e_0$.
We call $\attackerWin(g) = \{e \mid \game[g, e] \text{\upshape{} is won by the attacker}\}$ the attacker winning budgets.

[][see full proof]

The attacker winning budgets can be characterized by the two rules:

g_u g'

(e, u) ∈(g')

e ∈(g_)

∀(u,g') ∈(g_· ·)
(e, u) ∈(g')

e ∈(g_)

Use well-foundedness of attacker winning strategies.

It is easy to check that the rules will not allow to derive $e \in \attackerWin(g)$
if there is no attacker winning strategy for $\game[g,e]$;
therefore, the rules are sound.

For completeness, note that it is possible to define an order on pairs of game position and winning energy budget, $(g,e)$, as follows:
Fix a winning strategy for the attacker.
Then let $(g',e') < (g_\attackerSubscript,e)$ if, at attacker position $g_\attackerSubscript$, the strategy chooses some game move $g_\attackerSubscript \gameMoveX{u} g'$ and $e' = \energyUpdate(e,u)$;
and let $(g',e') < (g_\defenderSubscript,e)$ if, from defender position $g_\defenderSubscript$, there is a game move $g_\defenderSubscript \gameMoveX{u} g'$ and $e' = \energyUpdate(e,u)$.
This order must be well-founded on the attacker-winning game positions
(otherwise the defender could enforce an infinite play if the attacker plays this strategy).
Using well-founded induction over this order,
it is possible to find a derivation of $e \in \attackerWin(g)$ for every pair $(g,e)$ such that $\game[g,e]$ is won by the attacker.

max width=
[>->,shorten <=1pt,shorten >=0.5pt,auto,node distance=2cm, rel/.style=dashed,font=,
posStyle/.style=draw, inner sep=1ex,minimum size=1cm,minimum width=2cm,anchor=center,draw,black,fill=gray!5]
[posStyle, initial, initial text=]
(AttDelay) [right = 1.6cm of Att] $\attackerPos[\varepsilon]{p,Q_\varepsilon}$;
[ellipse, draw, inner sep=1ex, minimum size=1cm,minimum width=2cm,fill=gray!5]
(Def) [below = 2.2cm of AttDelay] $\defenderPos{p,Q}$;
[ellipse, draw=stabilityColor, inner sep=1ex, minimum size=1cm,minimum width=2cm,fill=stabilityColor!3]
(DefStab) [above right = 1.2cm of Def] $\defenderPosColor[s]{stabilityColor}{p,\{ q\!\in\!Q_\varepsilon \mid q \nostep{\tau} \}}$;
[ellipse, draw=etaColor, inner sep=1ex, minimum size=1cm,minimum width=2cm,fill=etaColor!3]
(DefBranch) [right = 3.3cm of AttDelay] $\defenderPosColor[\eta]{etaColor}{p,\alpha,p',Q_\varepsilon \setminus Q_\alpha, Q_\alpha}$;
[posStyle, draw=etaColor, fill=etaColor!3]
(AttBranch) [above=.9cm of DefBranch] $\attackerPosColor[\eta]{etaColor}{p',Q'}$;
(AttConj) [below right = 1.2cm and .2cm of DefStab] $\attackerPos[\wedge]{p,q}$;
[posStyle, dashed]
(AttSwap) [right = 2cm of AttConj] $\attackerPos[\varepsilon]{q,\{p' \mid p \stepWeak p'\}}$;
[posStyle, dashed]
(AttContinue) [above = 1.5cm of AttSwap] $\attackerPos[\varepsilon]{p,\{q' \mid q \stepWeak q'\}}$;
[posStyle, dashed]
(AttObs) [right = 2cm of AttBranch] $\attackerPos{p^\prime,Q^\prime}$;
(Att) edge
node[label=-90:$\textcolor{gray}{\zeroVec}$] $Q \stepWeak Q_\varepsilon$ (AttDelay)
(Att) edge[bend right=15]
node[pos = .4, label=-150:$\textcolor{gray}{\zeroVec}$] $Q = \varnothing$ (Def)
(Att) edge[bend right=60]
node[pos = .6, label=-130:$\textcolor{gray}{-\unit{5}}$] $Q \neq \varnothing$ (Def)
(AttDelay) edge [out=155,in=115,looseness=4, pos=.6] node $p \step{\tau} \ldots\; \textcolor{gray}{\zeroVec}$ (AttDelay)
(AttDelay.north) edge[bend left=28]
node[pos=.3, align=center, label=[label distance=0.0cm]-30:$\textcolor{gray}{-\unit{1}}$] $p\step{a}p'$
$Q_\varepsilon \step{a} Q'$ (AttObs)
(AttDelay) edge
node[pos =.74, label=[label distance=0cm]-180:$\textcolor{gray}{\zeroVec}$] $Q = Q_\varepsilon$ (Def)
(AttDelay) edge[draw=stabilityColor]
node[pos=.7,label=[label distance=0.2cm]-175:$\textcolor{stabilityColor!50}{\zeroVec}$] $\textcolor{stabilityColor}{p \centernot{\step{\tau}}}$ (DefStab)
(AttDelay) edge[draw=etaColor]
node[align=center,label=[label distance=0cm]-90:$\textcolor{etaColor!50}{\zeroVec}$] $\textcolor{etaColor}{p \step{\alpha} p'}$
$\textcolor{etaColor}{\varnothing \neq Q_\alpha \subseteq Q_\varepsilon}$ (DefBranch)
(Def) edge[bend right=15]
node[pos=.3, label=[label distance=0.1cm]-100:$\textcolor{gray}{-\unit{3}}$] $q \in Q$ (AttConj)
(DefStab) edge[draw=stabilityColor, bend right=15]
node[align=right, pos=.7, label=[label distance=0.2cm]-160:$\textcolor{stabilityColor!50}{-\unit{4}}$] $\textcolor{stabilityColor}{q\!\in\!Q_\varepsilon}$
$\textcolor{stabilityColor}{q \nostep{\tau}}$ (AttConj)
(AttConj) edge[bend left=10]
node[label=[label distance=0.0cm]-75:$\textcolor{gray}{\updMin{1,6},0,0,0,0,0,0,0}$]  (AttContinue)
(AttConj) edge[bend right=15]
node[below] $\textcolor{gray}{\updMin{1,7},0,0,0,0,0,0,-1}$ (AttSwap)
(DefBranch) edge[draw=etaColor]
node[pos=.42, label=[label distance=0.1cm]-0:$\textcolor{etaColor!50}{\updMin{1,6},-1,-1,0,0,0,0,0}$] $\textcolor{etaColor}{Q_\alpha\! \step{(\alpha)} Q'}$ (AttBranch)
(AttBranch) edge[draw=etaColor]
node[below]$\textcolor{etaColor!50}{-\unit{1}}$ (AttObs)
(DefBranch) edge[bend left=5, draw=etaColor]
node[pos=.1, align=center, label=[label distance=0.2cm]-180:$\textcolor{etaColor!50}{-\unit{2}-\unit{3}}$] $\textcolor{etaColor}{q \in Q_\varepsilon \setminus Q_\alpha}$ (AttConj);

Schematic spectroscopy game $\gameSpectroscopy$ of Definitions <ref> (the black part),
<ref> (with position $\defenderPosColor[s]{stabilityColor}{\cdots}$),
and <ref> (with positions $\defenderPosColor[s]{stabilityColor}{\cdots}$, $\defenderPosColor[\eta]{etaColor}{\cdots}$ and $\attackerPosColor[\eta]{etaColor}{\cdots}$).

§.§ Delaying Observations in the Spectroscopy Energy Game

We begin with the part of the game that is close to the “strong” spectroscopy game of [4].
It matches the black part of the $\hmlBA$-grammar of <ref>.

For a system $\system=(\proc,\actions,\step{})$,
the spectroscopy delay energy game $\game_\varepsilon^\system[g_0,e_0]=(G,G_\defenderSubscript,\gameMove,w,g_{0},e_0)$
consists of

* attacker positions $\attackerPos{p,Q}$ $\in G_\attackerSubscript$,

* attacker delayed positions $\attackerPos[\varepsilon]{p,Q}$ $\in G_\attackerSubscript$,

* attacker clause positions $\attackerPos[\wedge]{p,q}$ $\in G_\attackerSubscript$,

* defender conjunction positions $\defenderPos{p,Q}$ $\in G_\defenderSubscript$,

where $p, q \in \proc$, $Q \in \powerSet{\proc}$, and nine kinds of moves:

* delay $\attackerPos{p,Q}$ $\gameMoveX{\mathmakebox[6.3em]{0,0,0,0,0,0,0,0}}$ $\attackerPos[\varepsilon]{p,Q'}$ if $Q \stepWeak Q'$,

* procrastination $\attackerPos[\varepsilon]{p,Q}$ $\gameMoveX{\mathmakebox[6.3em]{0,0,0,0,0,0,0,0}}$ $\attackerPos[\varepsilon]{p',Q}$ if $p \step{\tau} p'$, $p \neq p'$,

* observation $\attackerPos[\varepsilon]{p,Q}$ $\gameMoveX{\mathmakebox[6.3em]{-1,0,0,0,0,0,0,0}}$ $\attackerPos{p',Q'}$ if $p\!\step{a}\!p'\!$, $Q\!\!\step{a}\!Q'\!$, $a\!\neq\!\tau\!$,

* finishing $\attackerPos{p,\varnothing}$ $\gameMoveX{\mathmakebox[6.3em]{0,0,0,0,0,0,0,0}}$ $\defenderPos{p,\varnothing}$,

* early conj. $\attackerPos{p,Q}$ $\gameMoveX{\mathmakebox[6.3em]{0,0,0,0,-1,0,0,0}}$ $\defenderPos{p,Q}$ if $Q \neq \varnothing$,

* late instable conj. $\attackerPos[\varepsilon]{p,Q}$ $\gameMoveX{\mathmakebox[6.3em]{0,0,0,0,0,0,0,0}}$ $\defenderPos{p,Q}$,

* conj. answers $\defenderPos{p,Q}$ $\gameMoveX{\mathmakebox[6.3em]{0,0,-1,0,0,0,0,0}}$ $\attackerPos[\wedge]{p,q}$ if $q \in Q$,

* positive clauses $\attackerPos[\wedge]{p,q}$ $\gameMoveX{\mathmakebox[6.3em]{\updMin{1,6},0,0,0,0,0,0,0}}$ $\attackerPos[\varepsilon]{p,Q}$ if $\{q\} \stepWeak Q$,

* negative clauses $\attackerPos[\wedge]{p,q}$ $\gameMoveX{\mathmakebox[6.3em]{\updMin{1,7},0,0,0,0,0,0,-1}}$$\attackerPos[\varepsilon]{q,Q}$if $\{p\} \stepWeak Q$ and $p \neq q$.

Starting at $\ccsIdentifier{P_c}$ and $\ccsIdentifier{P_p}$ of <ref> with energy $(2,0,1,0,0, 1,0,0)$, the attacker can move with
$\attackerPos{\ccsIdentifier{P_c}, \{ \ccsIdentifier{P_p} \}}
\gameMoveX{\text{delay}}
\attackerPos[\varepsilon]{\ccsIdentifier{P_c}, \{
\ccsIdentifier{P_p},
\action{op} \ccsPrefix \tau \ccsPrefix \ccsIdentifier{A},
\action{op} \ccsPrefix \tau \ccsPrefix \ccsIdentifier{B}
\}}\!
\gameMoveX{\text{observation\vphantom{y}}}\linebreak[3]
\gameMoveX{\text{delay}}
\gameMoveX{\text{late instable conj}}\!
\defenderPos{
\tau \ccsPrefix \tau \ccsPrefix \ccsIdentifier{A} \ccsChoice \tau \ccsPrefix \tau \ccsPrefix \ccsIdentifier{B},
\allowbreak
\{
\tau \ccsPrefix \ccsIdentifier{A}, \ccsIdentifier{A},
\tau \ccsPrefix \ccsIdentifier{B}, \ccsIdentifier{B}
\}
(For clarity, we label the moves by the names of their rules.
Also, we use simpler bisimilar CCS terms to refer to the reached processes.)
If the defender selects $\ccsIdentifier{A}$, the attacker wins by
\tau \ccsPrefix \tau \ccsPrefix \ccsIdentifier{A} \ccsChoice \tau \ccsPrefix \tau \ccsPrefix \ccsIdentifier{B},
\ccsIdentifier{A}
\gameMoveX{\text{positive clause}}
\allowbreak
\gameMoveX{\text{procrastination}}
\gameMoveX{\text{procrastination}}
\attackerPos[\varepsilon]{
\ccsIdentifier{B},
\{\ccsIdentifier{A}\}
\gameMoveX{\text{observation\vphantom{y}}}\linebreak[2]
\gameMoveX{\text{finishing}}
\mbox{$\defenderPos{\ccsStop, \varnothing}
\centernot\gameMove$}$.
An analogous sequence works for all defender choices.
Thus, the attacker wins the game.

Note that the attacker would not win if any component of the starting energy vector were lower.
Therefore, $(2,0,1,0,0,1,0,0)$ is a minimal winning budget for the attacker.
There also are some other minimal budgets, where positive conjuncts are sidestepped through immediate negations, for instance $(2,0,2,0,1,0,1,2) \leq e_{\mathrm{DB}}$.
Combined, the $\attackerWin(\attackerPos{\ccsIdentifier{P_c}, \{ \ccsIdentifier{P_p} \}})$ reveal that contrasimulation, $e_{\mathrm{C}} \notin \attackerWin(\attackerPos{\ccsIdentifier{P_c}, \{ \ccsIdentifier{P_p} \}})$, is the finest notion to preorder $\ccsIdentifier{P_c} \bPreord{C}\ccsIdentifier{P_p}$.

The tree of winning moves in <ref> corresponds to formula and budget of <ref>, $\varphi_\mathsf{cp} = \hmlEps\hmlObsI{op}\hmlEps\hmlAndS\{\hmlEps\hmlObsI{aEats}\hmlTrue, \hmlEps\hmlObsI{bEats}\hmlTrue \}$.
This is no coincidence, but rather our core design principle for game moves.
As we will prove in <ref>, attacker's winning moves match distinguishing $\hmlBA$-formulas.
To illustrate this relationship, we provide the definitions of how attacker strategies correspond to formulas already in the present section.

Given the set of winning budgets $\attackerWin$,
the set of attacker strategy formulas $\hmlStrategies$ for a position with given energy level $e$ is defined inductively:

p,Q u [ε]p,Q'

e' = (e, u) ∈([ε]p,Q')

χ∈([ε]p,Q', e')

χ∈(p,Q, e)
[ε]p,Q u [ε]p',Q

e' = (e, u) ∈([ε]p',Q)

χ∈([ε]p',Q, e')

χ∈([ε]p,Q, e)
[ε]p,Q u p',Q'

e' = (e, u) ∈(p',Q')

p a p'

Q a Q'

φ∈(p',Q', e')

aφ∈([ε]p,Q, e)
*[left=early conj]
p,Q u p,Q

e' = (e, u) ∈(p,Q)

φ∈(p,Q, e')

φ∈(p,Q, e)
*[left=late conj]
[ε]p,Q u p,Q

e' = (e, u) ∈(p,Q)

χ∈(p,Q, e')

χ∈([ε]p,Q, e)
p,Q u_q [∧]p,q

e_q = (e, u_q) ∈([∧]p,q)

ψ_q ∈([∧]p,q, e_q)

for each  q ∈Q

qQψ_q ∈(p,Q, e)
[∧]p,q u [ε]p,Q'

e' = (e, u) ∈([ε]p,Q')

χ∈([ε]p,Q', e')

χ∈([∧]p,q, e)
[∧]p,q u [ε]q,P'

e' = (e, u) ∈([ε]q,P')

χ∈([ε]q,P', e')

χ∈([∧]p,q, e)

We will prove in Lemmas <ref> and <ref> that the attacker strategy formulas are distinguishing formulas
whose expressiveness price $\expr$ generally is equal to the second parameter of $\hmlStrategies$.
There is one technical difference though:
For attacker delayed positions,
if $\chi \in \hmlStrategies(\attackerPos[\varepsilon]{p,Q}, e)$,
then $\hmlEps\chi$ is a formula that distinguishes $p$ from $Q$
(see <ref>, Item <ref>).
Otherwise, rule (procr) in <ref> would need to prepend $\hmlEps$ to the distinguishing formula,
possibly leading to repeated $\hmlEps\hmlEps\cdots\hmlEps\chi$.

§.§ Covering Stable Failures and Conjunctions

In formalisms that allow abstraction, that is, turning visible behavior into internal one, as with CSP's hiding operator, many equivalences characterized by the core game $\game_\varepsilon$ of the previous section, are no congruences.
One example would be (instable) failures;
van Glabbeek [12] thus rather focusses on stable failures instead.
In order to cover such “stable” and “stability-respecting” equivalences, we must separately count stable conjunctions.

The stability game $\game_s^\system$
extends the delay game $\game_\varepsilon^\system$ of <ref> by

* defender stable conjunction positions 17em
$\defenderPos[s]{p,Q} \in G_\defenderSubscript$,

where $p \in \proc$, $Q \in \powerSet{\proc}$, and two kinds of moves:

* late stable conj. $\attackerPos[\varepsilon]{p,Q}$ $\gameMoveX{\mathmakebox[5em]{0,0,0,0,0,0,0,0}}$ $\defenderPos[s]{p,Q'}$ if $Q'\! = \!\{ q \in Q \mid q\!\nostep{\tau} \}$,

* conj. s-answers $\defenderPos[s]{p,Q}$ $\gameMoveX{\mathmakebox[5em]{0,0,0,\textcolor{stabilityColor}{-1},0,0,0,0}}$ $\attackerPos[\wedge]{p,q}$ if $q \in Q$.

Noticing that these new rules allow no new (incomparable) wins for the attacker in <ref>, $e_\mathrm{SB} \notin \attackerWin(\attackerPos{\ccsIdentifier{P_c}, \{ \ccsIdentifier{P_p} \}})$ for  $\game_s$ exposes stable bisimulation as another finest equivalence for the example processes.
Stable bisimilarity and contrasimilarity are commonly the coarsest reasonable abstractions of bisimilarity for systems with internal behavior.

For the stability game, we extend the rules of <ref> as follows:

[ε]p,Q u [s]p,Q

e' = (e, u) ∈([s]p,Q)

χ∈([s]p,Q, e')

χ∈([ε]p,Q, e)
*[left=stable conj]
[s]p,Q u_q [∧]p,q

e_q = (e, u_q) ∈([∧]p,q)

ψ_q ∈([∧]p,q, e_q)

for each  q ∈Q

({τ} ∪{ ψ_q |q ∈Q }) ∈([s]p,Q, e)

§.§ Extending to Branching Bisimulation

One last kind of distinctions is necessary to characterize branching bisimilarity, the strongest common abstraction of bisimilarity for systems with silent steps:
its characteristic branching conjunctions.

The full spectroscopy energy game $\gameSpectroscopy^\system$
extends <ref> by

* defender branching positions 15em
$\defenderPos[\eta]{p,\alpha,p',Q,Q_\alpha} \in G_\defenderSubscript$,

* attacker branching positions 15em
$\attackerPos[\eta]{p,Q} \in G_\attackerSubscript$,

where $p, p' \in \proc$ and $Q, Q_\alpha \in \powerSet{\proc}$ as well as $\alpha \in \actions$, and four kinds of moves:

* branching conj. $\attackerPos[\varepsilon]{p,Q}$
$\gameMoveX{\mathmakebox[10.5em]{0,0,0,0,0,0,0,0}}$$\defenderPos[\eta]{p,\alpha,p',Q \setminus Q_\alpha,Q_\alpha}$

if $p \step{\alpha} p'\!$, $\varnothing \neq Q_\alpha \subseteq Q$,

* br. answer $\defenderPos[\eta]{p,\alpha,p',Q,Q_\alpha}$$\gameMoveX{\mathmakebox[6.5em]{0,\textcolor{etaColor}{-1},-1,0,0,0,0,0}}$$\attackerPos[\wedge]{p,q}$if $q \in Q$,

* br. observation $\defenderPos[\eta]{p,\alpha,p',Q,Q_\alpha}$$\gameMoveX{\mathmakebox[6.5em]{\updMin{1,6},\textcolor{etaColor}{-1},-1,0,0,0,0,0}}$$\attackerPos[\eta]{p',Q'}$with $Q_\alpha\!\!\step{\hmlOpt\alpha}\! Q'\!$,

* br. accounting $\attackerPos[\eta]{p,Q}$

Intuitively, when the attacker chooses a branching conjunction move
$\attackerPos{p,Q} \gameMove \attackerPos[\varepsilon]{p,Q'}
\gameMove \defenderPos[\eta]{p,\alpha,p',\linebreak[0] \mbox{$Q' \setminus Q_\alpha$},Q_\alpha}$,
they claim that $p \not\bPreord{} Q$ because of transition $p \step{\alpha} p'$.
The defender can counter by providing a path $q \stepWeak q' \step{\hmlOpt{\alpha}} q''$ that $\eta$-simulates it,
, $p \bPreord{} q'$ and $p' \bPreord{} q''$.
In the game, this means that the defender picks a specific $q' \in Q'$ for the simulating path.
Then, the attacker has to counter further by claiming either that $p \not\bPreord{} q'$ so the game continues with $\attackerPos[\wedge]{p,q'}$,
or that $p' \not\bPreord{} q''$ for any $q' \step{\hmlOpt{\alpha}} q''$ so the game continues with (a superset of) $\attackerPos{p',\{q'' \mid q' \step{\hmlOpt{\alpha}} q''\}}$.
To make the moves align with the production in <ref>,
the attacker already made this second choice by dividing set $Q'$ into parts $Q' \setminus Q_\alpha$ and $Q_\alpha$.

An earlier version of our game published to arXiv did not include attacker branching positions
but moved directly $\defenderPos[\eta]{p,\alpha,p',Q,Q_\alpha} \gameMove \attackerPos{p',Q'}$.
This requires two updates $\updMin{1,6}$ and $-1$ in the first dimension.
It would be possible to remove attacker branching positions if one allowed positive updates:
one could update $-\unit{1}$ earlier, with moves $\attackerPos[\varepsilon]{p,Q} \gameMoveX{-1,-1,-1,0,0,-1,0,0} \defenderPos[\eta]{p,\alpha,p', \linebreak[0] \mbox{$Q \setminus Q_\alpha$}, Q_\alpha} \gameMoveX{\updMin{1,6},0,0,0,0,0,0,0} \attackerPos{p',Q'}$
(one needs to update $-\unit{6}$ as well in the branching [2] conj. move because the order with $\updMin{1,6}$ is swapped)
and partially undo this update in the branching answer $\defenderPos[\eta]{p,\alpha,p',\linebreak[0] \mbox{$Q \setminus Q_\alpha$}, Q_\alpha} \gameMoveX{+1,0,0,0,0,0,+1,0,0} \attackerPos[\wedge]{p,q}$.
However, we prefer to disallow updates that “generate” energy.

For the full spectroscopy game, we extend the rules of <ref> as follows:

[ε]p,Q u [η]p,α,p',Q',Q_α

e' = (e, u) ∈([η]p,α,p',Q',Q_α)

χ∈([η]p,α,p',Q',Q_α, e')

χ∈([ε]p,Q, e)
*[left=branch conj]
[η]p,α,p',Q,Q_α u_α [η]p',Q' u'_α p',Q'

e_α= ((e, u_α), u'_α) ∈(p',Q')

φ_α∈(p',Q', e_α)

[η]p,α,p',Q,Q_α u_q [∧]p,q

e_q = (e, u_q) ∈([∧]p,q)

ψ_q ∈([∧]p,q, e_q)

for each  q ∈Q

({α φ_α} ∪{ ψ_q |q ∈Q }) ∈([η]p,α,p',Q,Q_α, e)

§ CORRECTNESS

We now state in what sense winning energy levels and equivalences coincide.

For all $e \in \energies_\infty$, $p \in \proc$, $Q \in \powerSet{\proc}$, the following are equivalent:

* There exists a formula $\varphi \in \hmlBA$ with price $\expr(\varphi) \leq e$ that distinguishes $p$ from $Q$.

* The attacker wins $\gameSpectroscopy[\attackerPos{p,Q}, e]$ (that is, $e \in \attackerWin(\attackerPos{p,Q})$).

With <ref>, this implies that,
for a notion of equivalence $N$ with coordinate $e_N$ in <ref>,
$p \bPreord{\mathit{N}} q$ precisely if
the defender wins $\gameSpectroscopy[\attackerPos{p,\{q\}}, e_N]$
(that is, if $e_N \notin \attackerWin(\attackerPos{p,\{q\}})$).

The proof of the theorem is given through the following three lemmas.
The direction from (1) to (2) is covered by <ref> when combined with the upward-closedness of attacker winning budgets.
From (2) to (1), the link is established through formulas in $\hmlStrategies$ by Lemmas <ref> and <ref>.

[][see full proof]

If $\varphi \in \hmlBA$ distinguishes $p$ from $Q$, then we are sure to have $\expr(\varphi) \in \attackerWin(\attackerPos{p,Q})$.

By mutual structural induction on $\varphi$, $\chi$, and $\psi$ with respect to the following claim:

* At attacker positions, if $\varphi \in \hmlBA$ distinguishes $p$ from $Q \neq \varnothing$, then $\expr(\varphi) \in \attackerWin(\attackerPos{p,Q})$;

* if $\chi$ distinguishes $p$ from $Q \neq \varnothing$ and $Q$ is closed under $\stepWeak$ (i.e. $Q \stepWeak Q$),
then $\expr^\varepsilon(\chi) \in \attackerWin(\attackerPos[\varepsilon]{p,Q})$;

* and if $\psi$ distinguishes $p$ from $q$,
then $\expr^\wedge(\psi) \in \attackerWin(\attackerPos[\wedge]{p,q})$.

* At defender positions, if $\hmlAndS \Psi$ distinguishes $p$ from $Q \neq \varnothing$,
then $\expr^\varepsilon(\hmlAndS \Psi) \in \attackerWin(\defenderPos{p,Q})$;

* if $\hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi$ distinguishes $p$ from $Q \neq \varnothing$
and the processes in $Q$ are stable,
then $\expr^\varepsilon(\hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi) \in \attackerWin(\defenderPos[s]{p,Q})$;

* and if $\hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \Psi$ distinguishes $p$ from $Q$,
then $\expr^\varepsilon(\hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \Psi) \in \attackerWin(\defenderPos[\eta]{p,\alpha,p',\linebreak[0] \mbox{$Q \setminus Q_\alpha$}, Q_\alpha})$
for any $p \step{\alpha} p' \in \hmlSemantics{\varphi'}{}{}$ and $Q \cap \hmlSemantics{\hmlAndS \Psi}{}{} \subseteq Q_\alpha \subseteq Q \setminus \hmlSemantics{\hmlOpt{\alpha}\varphi'}{}{}$.

If $Q = \varnothing$, the lemma is very easy to prove.
So let us assume that $Q \neq \varnothing$ for the rest.
To get an inductive property, we actually prove the following property:

* At attacker positions, if $\varphi \in \hmlBA$ distinguishes $p$ from $Q \neq \varnothing$, then $\expr(\varphi) \in \attackerWin(\attackerPos{p,Q})$;

* if $\chi$ distinguishes $p$ from $Q \neq \varnothing$ and $Q$ is closed under $\stepWeak$ (i.e. $Q \stepWeak Q$),
then $\expr^\varepsilon(\chi) \in \attackerWin(\attackerPos[\varepsilon]{p,Q})$;

* and if $\psi$ distinguishes $p$ from $q$,
then $\expr^\wedge(\psi) \in \attackerWin(\attackerPos[\wedge]{p,q})$.

* At defender positions, if $\hmlAndS \Psi$ distinguishes $p$ from $Q \neq \varnothing$,
then $\expr^\varepsilon(\hmlAndS \Psi) \in \attackerWin(\defenderPos{p,Q})$;

* if $\hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi$ distinguishes $p$ from $Q \neq \varnothing$
and the processes in $Q$ are stable,
then $\expr^\varepsilon(\hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi) \in \attackerWin(\defenderPos[s]{p,Q})$;

* and if $\hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \Psi$ distinguishes $p$ from $Q$,
then $\expr^\varepsilon(\hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \Psi) \in \attackerWin(\defenderPos[\eta]{p,\alpha,p',\linebreak[0] \mbox{$Q \setminus Q_\alpha$}, Q_\alpha})$
for any $p \step{\alpha} p' \in \hmlSemantics{\varphi'}{}{}$ and $Q \cap \hmlSemantics{\hmlAndS \Psi}{}{} \subseteq Q_\alpha \subseteq Q \setminus \hmlSemantics{\hmlOpt{\alpha}\varphi'}{}{}$.

and we prove this by mutual induction over the structure of $\varphi$, $\chi$, and $\psi$.

* Assume $\varphi$ distinguishes $p$ from $Q \neq \varnothing$.

$\varphi = \hmlEps\chi$:
That means that there exists $p \stepWeak p' \in \hmlSemantics{\chi}{}{}$
and $Q' \cap \hmlSemantics{\chi}{}{} = \varnothing$ for $Q \stepWeak Q'$.
Therefore, $\chi$ distinguishes $p'$ from $Q'$ and $Q' \stepWeak Q'$.
By induction hypothesis we conclude that $\expr^\varepsilon(\chi) \in \attackerWin(\attackerPos[\varepsilon]{p',Q'})$.

Now there are the moves $\attackerPos{p,Q} \gameMoveX{\text{delay}}
\attackerPos[\varepsilon]{p,Q'} \overset{\text{procrastination}}{\gameMove \cdots \gameMove}
\attackerPos[\varepsilon]{p',Q'}$.
Using <ref> over these moves,
we can conclude that $\expr^\varepsilon(\chi) \in \attackerWin(\attackerPos{p,Q})$.
We get the result because $\expr(\varphi) = \expr^\varepsilon(\chi)$.

$\varphi = \hmlAndS \Psi$:
There is the move $\attackerPos{p,Q} \gameMoveX{\text{early conj.}} \defenderPos{p,Q}$.
By induction hypothesis we conclude that $\expr^\varepsilon(\hmlAndS \Psi) \in \attackerWin(\defenderPos{p,Q})$.
Using <ref>
we immediately get that $\expr(\varphi) = \expr^\varepsilon(\varphi) + \unit{5} \in \attackerWin(\attackerPos{p,Q})$.

* Assume $\chi$ distinguishes $p$ from $Q$ (and $Q \stepWeak Q$).

$\chi = \hmlObs{a}\varphi'$:
That means that there exist $p' \in \hmlSemantics{\varphi'}{}{}$ such that $p \step{a} p'$.
On the other hand, $Q' \cap \hmlSemantics{\varphi'}{}{} = \varnothing$, where $Q \step{a} Q'$,
and therefore $\varphi'$ distinguishes $p'$ from $Q'$.

Now there is the move $\attackerPos{p,Q} \gameMoveX{\text{observation}} \attackerPos{p',Q'}$,
By induction hypothesis we conclude that $\expr(\varphi') \in \attackerWin(\attackerPos{p',Q'})$.
We can calculate $\expr^\varepsilon(\hmlObs{a}\varphi') := \unit{1} + \expr(\varphi')$;
in other words, $\energyUpdate(\expr^\varepsilon(\chi),-\unit{1}) = \expr(\varphi')$.
With <ref>,
we get that $\expr^\varepsilon(\chi) \in \attackerWin(\attackerPos{p,Q})$.

$\chi = \hmlAndS \Psi$:
There is the move $\attackerPos[\varepsilon]{p,Q}\allowbreak \gameMoveX{\text{late instable conj.}} \defenderPos{p,Q}$;
we use the proof for $\defenderPos{p,Q}$ that follows in (4) and <ref>
to then get $\expr^\varepsilon(\chi) \in \attackerWin(\attackerPos{p,Q})$.

$\chi = \hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi$:
We argue as in the previous case using (5).

$\chi = \hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \Psi$:
Note that there must exist $p \step{\hmlOpt{\alpha}} p' \in \hmlSemantics{\varphi'}{}{}$
(otherwise $p \not\in \hmlSemantics{\hmlOpt{\alpha}\varphi'}{}{} \supseteq \hmlSemantics{\chi}{}{}$,
so $\chi$ would not distinguish $p$ from anything),
and there must exist $Q_\alpha$ satisfying
$Q \cap \hmlSemantics{\hmlAndS \Psi}{}{} \subseteq Q_\alpha \subseteq Q \setminus \hmlSemantics{\hmlOpt{\alpha}\varphi'}{}{}$
(otherwise $Q \cap \hmlSemantics{\hmlAndS \Psi}{}{} \not\subseteq Q \setminus \hmlSemantics{\hmlOpt{\alpha}\varphi'}{}{}$
and therefore $\varnothing \neq (Q \cap \hmlSemantics{\hmlAndS \Psi}{}{}) \setminus (Q \setminus \hmlSemantics{\hmlOpt{\alpha}\varphi'}{}{})
= Q \cap \hmlSemantics{\hmlAndS \Psi}{}{} \cap \hmlSemantics{\hmlOpt{\alpha}\varphi'}{}{} = Q \cap \hmlSemantics{\chi}{}{}$,
so $\chi$ would not distinguish any process from $Q$).
Choose some $p'$ and $Q_\alpha$ satisfying these constraints.
Then there is the move $\attackerPos[\varepsilon]{p,Q} \gameMoveX{\text{branching conj.}} \defenderPos[\eta]{p,\alpha,p',\linebreak[0] \mbox{$Q \setminus Q_\alpha$},Q_\alpha}$;
we use the proof for $\defenderPos[\eta]{p,\alpha,p',\linebreak[0] \mbox{$Q \setminus Q_\alpha$},Q_\alpha}$ that follows in (6) and <ref>
to get $\expr^\varepsilon(\chi) \in \attackerWin(\attackerPos[\varepsilon]{p,Q})$.

* Assume $\psi$ distinguishes $p$ from $q$.

$\psi = \hmlEps\chi$:
That means that there exists $p \stepWeak p' \in \hmlSemantics{\chi}{}{}$
and $Q' \cap \hmlSemantics{\chi}{}{} = \varnothing$ for $\{q\} \stepWeak Q'$.
Therefore, $\chi$ distinguishes $p'$ from $Q'$ and $Q' \stepWeak Q'$.
By induction hypothesis we conclude that $\expr^\varepsilon(\chi) \in \attackerWin(\attackerPos[\varepsilon]{p',Q'})$.

Now there are moves $\attackerPos[\wedge]{p,q} \gameMoveX{\text{positive clause}}
\attackerPos[\varepsilon]{p,Q'} \overset{\text{procrastination}}{\gameMove \cdots \gameMove}
\attackerPos[\varepsilon]{p',Q'}$.
Using <ref> over the procrastination moves,
we can conclude that $\expr(\hmlEps\chi) = \expr^\varepsilon(\chi) \in \attackerWin(\attackerPos[\varepsilon]{p,Q'})$.
An easy calculation shows that
$\energyUpdate(\expr^\wedge(\psi), (\updMin{1,6},0,0,0,0,0,0,0)) \geq \expr^\varepsilon(\chi)$,
and this allows to apply <ref> and get the result.

$\psi = \hmlNeg\hmlEps\chi$:
That means that there exists $q \stepWeak q' \in \hmlSemantics{\chi}{}{}$
and $P' \cap \hmlSemantics{\chi}{}{} = \varnothing$ for $\{p\} \stepWeak P'$.
Therefore, $\chi$ distinguishes $q'$ from $P'$ and $P' \stepWeak P'$.
By induction hypothesis we conclude that $\expr^\varepsilon(\chi) \in \attackerWin(\attackerPos[\varepsilon]{q',P'})$.
A similar calculation as in the previous case shows that
$\energyUpdate(\expr^\wedge(\psi), (\updMin{1,7},0,\linebreak[0] 0,0,0,0,0,-1)) \geq \expr^\varepsilon(\chi)$,
and this allows to apply <ref> and get the result.

* Assume $\hmlAndS \Psi$ distinguishes $p$ from $Q$.

We can find, for every $q \in Q$, some $\psi_q \in \Psi$ such that $q \notin \hmlSemantics{\psi_q}{}{}$
(so $\Psi \neq \varnothing$).
Choose one such covering of $\psi_q$s.
Let $\Psi' := \{ \psi_q \mid q \in Q \} \subseteq \Psi$.
Each $\psi_q$ either has the form $\hmlEps\chi_q$ or $\hmlNeg\hmlEps\chi_q$.
We set $\Psi'_+ := \{ \chi_q \mid q \in Q, \psi_q = \hmlEps\chi_q \}$ and $\Psi'_- := \{ \chi_q \mid q \in Q, \psi_q = \hmlNeg\hmlEps\chi_q \}$.
It must be the case that $p \in \hmlSemantics{\hmlAnd{q}{Q} \psi_q}{}{}$ and $Q \cap \hmlSemantics{\hmlAnd{q}{Q} \psi_q}{}{} = \varnothing$.

Now there are the moves $\defenderPos{p,Q}
\gameMoveX{\text{conj.\@ answer}} \attackerPos[\wedge]{p,q}$
for all $q \in Q$.

We have to show that
$e_0 := \expr^\varepsilon(\chi) = \unit{3} + \sup \{ \expr^\wedge(\psi) \mid \psi \in \Psi \} \in \attackerWin(\defenderPos{p,Q})$.
As $\attackerWin(\defenderPos{p,Q})$ is upwards-closed,
we can restrict the supremum to $\Psi'$ instead of $\Psi$, so
it suffices to prove that $\sup \{ \expr^\wedge(\psi) + \unit{3} \mid \psi \in \Psi' \} \in \attackerWin(\defenderPos{p,Q})$.
Now, to show this using <ref>,
we have to quantify over all game moves from $\defenderPos{p,Q}$, i.e. over all conjunction answers,
which lead to the positions $\attackerPos[\wedge]{p,q}$ for $q \in Q$.
We have $\energyUpdate(e_0, -\unit{3}) \geq \expr^\wedge(\psi_q)$,
and by induction hypothesis $\expr^\wedge(\psi_q)\in \attackerWin(\attackerPos[\wedge]{p,q})$.
Applying <ref> immediately leads to the desired result.

* Assume $\hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi$ distinguishes $p$ from $Q$, where $p$ and the processes in $Q$ are stable.

We choose $\psi_q$ (for every $q \in Q$) and define $\Psi'$, $\Psi'_+$ and $\Psi'_-$ as in the previous case.

Now there are the moves $\defenderPos[s]{p,Q}
\gameMoveX{\text{conj.\@ s-answer}} \attackerPos[\wedge]{p,q}$
for all $q \in Q$.
We have to show that
$\expr^\varepsilon(\chi) = \unit{4} + \sup \{ \expr^\wedge(\psi) \mid \psi \in \Psi \} \in \attackerWin(\defenderPos[s]{p,Q})$.
This proceeds exactly as in the previous case.

* Assume $\hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \Psi$ distinguishes $p$ from $Q$, $p \step{\alpha} p' \in \hmlSemantics{\varphi'}{}{}$ and $Q \cap \hmlSemantics{\hmlAndS \Psi}{}{} \subseteq Q_\alpha \subseteq Q \setminus \hmlSemantics{\hmlOpt{\alpha}\varphi'}{}{}$.

We choose $\psi_q$ (for every $q \in Q$) and define $\Psi'$, $\Psi'_+$ and $\Psi'_-$ as in the previous case.

There are the moves $\defenderPos[\eta]{p,\alpha,p',\linebreak[0] \mbox{$Q \setminus Q_\alpha$}, Q_\alpha}
\gameMoveX{\text{br.\ answer}} \attackerPos[\wedge]{p,q}$
for all $q \in Q \setminus Q_\alpha$.
Additionally, there are the moves $\defenderPos[\eta]{p,\alpha,p',\linebreak[0] \mbox{$Q \setminus Q_\alpha$},Q_\alpha}
\gameMoveX{\text{br.\ observation}} \attackerPos[\eta]{p',Q'}
\gameMoveX{\text{br.\ accounting}} \attackerPos{p',Q'}$ for $Q_\alpha \step{\hmlOpt{\alpha}} Q'$,
and $\varphi'$ distinguishes $p'$ from $Q'$.

We have to show that
$e_0 := \expr^\varepsilon(\chi) = \unit{2} + \unit{3} + \sup \{ \expr^\wedge(\hmlEps\hmlOpt{\alpha}\varphi') \} \cup \{ \expr^\wedge(\psi) \mid \psi \in \Psi \} \in \attackerWin(\defenderPos[\eta]{p,\alpha,p',\linebreak[0] \mbox{$Q \setminus Q_\alpha$},Q_\alpha})$.
For the branching answer moves, this proceeds exactly as in the previous cases.
For the branching observation move,
we have to show that $e_2 := \energyUpdate(\energyUpdate(e_0, (\updMin{1,6},-1,-1,\linebreak[0] 0,0,0,0,0)),-\unit{1}) \in \attackerWin{\attackerPos{p',Q'}}$.
We know that $e_2 \geq \expr(\varphi')$
and by induction hypothesis $\expr(\varphi') \in \attackerWin{\attackerPos{p',Q'}}$.
This suffices to apply <ref> and get the result.

[][see full proof]

If $e \in \attackerWin(\attackerPos{p,Q})$, there is $\varphi \in \hmlStrategies(\attackerPos{p,Q}, e)$ with $\expr(\varphi) \leq e$.

By well-founded induction over pairs of game positions and attacker's winning energy budgets with respect to the claim:

* At attacker positions, if $e \in \attackerWin(\attackerPos{p,Q})$,
then there is $\varphi \in \hmlStrategies(\attackerPos{p,Q}, e)$ with $\expr(\varphi) \leq e$;

* if $e \in \attackerWin(\attackerPos[\varepsilon]{p,Q})$,
then there is $\chi \in \hmlStrategies(\attackerPos[\varepsilon]{p,Q}, e)$ with $\expr^\varepsilon(\chi) \leq e$;

* if $e \in \attackerWin(\attackerPos[\wedge]{p,q})$,
then there is $\psi \in \hmlStrategies(\attackerPos[\wedge]{p,q}, e)$ with $\expr^\wedge(\psi) \leq e$.

* At defender positions, if $e \in \attackerWin(\defenderPos{p,Q})$,
then there is $\hmlAndS \Psi \in \hmlStrategies(\defenderPos{p,Q})$ with $\expr^\varepsilon(\hmlAndS \Psi) \leq e$;

* if $e \in \attackerWin(\defenderPos[s]{p,Q})$,
then there is $\hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi \in \hmlStrategies(\defenderPos[s]{p,Q})$ with $\expr^\varepsilon(\hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi) \leq e$;

* if $e \in \attackerWin(\defenderPos[\eta]{p,\alpha,p',\mbox{$Q \setminus Q_\alpha$},Q_\alpha})$,
then there is $\hmlAndS \{ \hmlObs{\alpha}\varphi' \} \cup \Psi \in \hmlStrategies(\defenderPos[\eta]{p,\alpha,\linebreak[0] p', \mbox{$Q \setminus Q_\alpha$},Q_\alpha})$ with $\expr^\varepsilon(\hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \Psi) \leq e$.

We prove a more detailed result, namely:

* At attacker positions, if $e \in \attackerWin(\attackerPos{p,Q})$,
then there is $\varphi \in \hmlStrategies(\attackerPos{p,Q}, e)$ with $\expr(\varphi) \leq e$;

* if $e \in \attackerWin(\attackerPos[\varepsilon]{p,Q})$,
then there is $\chi \in \hmlStrategies(\attackerPos[\varepsilon]{p,Q}, e)$ with $\expr^\varepsilon(\chi) \leq e$;

* if $e \in \attackerWin(\attackerPos[\wedge]{p,q})$,
then there is $\psi \in \hmlStrategies(\attackerPos[\wedge]{p,q}, e)$ with $\expr^\wedge(\psi) \leq e$.

* At defender positions, if $e \in \attackerWin(\defenderPos{p,Q})$,
then there is $\hmlAndS \Psi \in \hmlStrategies(\defenderPos{p,Q})$ with $\expr^\varepsilon(\hmlAndS \Psi) \leq e$;

* if $e \in \attackerWin(\defenderPos[s]{p,Q})$,
then there is $\hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi \in \hmlStrategies(\defenderPos[s]{p,Q})$ with $\expr^\varepsilon(\hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi) \leq e$;

* if $e \in \attackerWin(\defenderPos[\eta]{p,\alpha,p',\mbox{$Q \setminus Q_\alpha$},Q_\alpha})$,
then there is $\hmlAndS \{ \hmlObs{\alpha}\varphi' \} \cup \Psi \in \hmlStrategies(\defenderPos[\eta]{p,\alpha,\linebreak[0] p', \mbox{$Q \setminus Q_\alpha$},Q_\alpha})$ with $\expr^\varepsilon(\hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \Psi) \leq e$.

We fix a winning attacker strategy for $\game[g,e]$
and prove this by the same well-founded induction over pairs of game position and winning energy budget, $(g, e)$,
as in the proof of <ref>.
We distinguish cases depending on the kind of position.

* Assume $e \in \attackerWin(\attackerPos{p,Q})$.
We distinguish further depending on the move that the strategy chooses:

Delay move $\attackerPos{p,Q} \gameMoveX{\zeroVec} \attackerPos[\varepsilon]{p,Q_\varepsilon}$:
We know $e = \energyUpdate(e,\zeroVec) \in \attackerWin(\attackerPos[\varepsilon]{p,Q_\varepsilon})$
and that $(\attackerPos[\varepsilon]{p,Q_\varepsilon},e) < (\attackerPos{p,Q},e)$ in the well-founded order,
so by induction hypothesis we know that there exists $\chi \in \hmlStrategies(\attackerPos[\varepsilon]{p,Q_\varepsilon},e)$
and $\expr^\varepsilon(\chi) \leq e$.
But then $\hmlEps\chi \in \hmlStrategies(\attackerPos{p,Q},e)$ by rule (delay) of <ref>
and $\expr(\hmlEps\chi) = \expr^\varepsilon(\chi) \leq e$.

Early conjunction move $\attackerPos{p,Q} \gameMoveX{-\unit{5}} \defenderPos{p,Q}$:
We know that $e' = \energyUpdate(e,\allowbreak-\unit{5}) \in \attackerWin(\defenderPos{p,Q})$
and that $(\defenderPos{p,Q},e') < (\attackerPos{p,Q},e)$ in the well-founded order,
so by induction hypothesis we know that there exists a conjunction formula $\hmlAndS \Psi \in \hmlStrategies(\defenderPos{p,Q},e')$
and $\expr^\varepsilon(\hmlAndS \Psi) \leq e'$.
But then, by rule (early conj) of <ref>,
$\hmlAndS \Psi \in \hmlStrategies(\attackerPos{p,Q},e)$ and $\expr(\hmlAndS \Psi) \leq e$.

* Assume $e \in \attackerWin(\attackerPos[\varepsilon]{p,Q})$.
We distinguish further depending on the move that the strategy chooses:

Procrastination move $\attackerPos[\varepsilon]{p,Q} \gameMoveX{\zeroVec} \attackerPos[\varepsilon]{p',Q}$:
We know that $\energyUpdate(e,\zeroVec) = e \in \attackerWin(\attackerPos[\varepsilon]{p',Q})$.
By induction hypothesis, we know that there is a formula $\chi \in \hmlStrategies(\attackerPos[\varepsilon]{p',Q},e)$
and $\expr^\varepsilon(\chi) \leq e$;
therefore, by rule (procr) of <ref>,
$\chi \in \hmlStrategies(\attackerPos[\varepsilon]{p,Q},e)$.

Late (instable) conjunction move $\attackerPos[\varepsilon]{p,Q} \gameMoveX{\zeroVec} \defenderPos{p,Q}$:
It must be the case that $e \in \attackerWin(\defenderPos{p,Q})$.
By induction hypothesis there is some formula $\hmlAndS \Psi \in \hmlStrategies(\defenderPos{p,Q}, e)$
and $\expr^\varepsilon(\hmlAndS \Psi) \leq e$;
therefore, by rule (late conj) of <ref>,
$\hmlAndS \Psi \in \hmlStrategies(\attackerPos[\varepsilon]{p,Q},e)$.

Stable conjunction move $\attackerPos[\varepsilon]{p,Q} \gameMoveX{\zeroVec} \defenderPos[s]{p,\{ q \in Q \mid \mbox{$q \centernot{\step{\tau}}$} \}}$:
It must be the case that $p$ is stable and $e \in \attackerWin(\defenderPos{p,\{q \in Q \mid \mbox{$q \centernot{\step{\tau}}$} \}})$.
By induction hypothesis there is some formula $\hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi \in \hmlStrategies(\defenderPos[s]{p,\{ q \in Q \mid \mbox{$q \centernot{\step{\tau}}$} \}})$
and $\expr^\varepsilon(\hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi) \leq e$;
therefore, by rule (stable) of <ref>,
$\hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi \in \hmlStrategies(\attackerPos[\varepsilon]{p,Q},e)$.

Branching conjunction move $\attackerPos[\varepsilon]{p,Q} \gameMoveX{\zeroVec} \defenderPos{p,\alpha,p',Q\setminus Q_\alpha, Q_\alpha}$:
It must[4] be the case that $e \in \attackerWin(\defenderPos{p,\alpha,p',Q\setminus Q_\alpha, Q_\alpha})$.
By induction hypothesis there is a formula $\hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \Psi \in \hmlStrategies(\defenderPos{p,\alpha,p',Q\setminus Q_\alpha, Q_\alpha})$
and $\expr^\varepsilon(\hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \Psi) \leq e$;
therefore, by rule (branch) of <ref>,
$\hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \Psi \in \hmlStrategies(\attackerPos[\varepsilon]{p,Q})$.

* Assume $e \in \attackerWin(\attackerPos[\wedge]{p,q})$.
We distinguish further depending on the move that the strategy chooses:

Positive clause $\attackerPos[\wedge]{p,q} \gameMoveX{(\updMin{1,6},0,0,0,0,0,0,0)} \attackerPos[\varepsilon]{p,\{ q' \mid q \stepWeak q' \}}$:
It must be the case that $e' := \energyUpdate(e,(\updMin{1,6},0,0,0,0,0,0,0)) \in \attackerWin(\attackerPos[\varepsilon]{p,\{ q' \mid q \stepWeak q' \}})$.
By induction hypothesis there is some formula $\chi \in \hmlStrategies(\attackerPos[\varepsilon]{p,\{ q' \mid q \stepWeak q' \}}, e')$
and $\expr^\varepsilon(\chi) \leq e'$;
therefore, by rule (pos) of <ref>,
$hmlEps\chi \in \hmlStrategies(\attackerPos[\wedge]{p,q}, e)$.

Negative clause $\attackerPos[\wedge]{p,q} \gameMoveX{(\updMin{1,7},0,0,0,0,0,0,-1)} \attackerPos[\varepsilon]{q,\{ p' \mid p \stepWeak p' \}}$:
It must be[4] the case that $e' := \energyUpdate(e,(\updMin{1,7},0,0,0,0,0,0,-1)) \in \attackerWin(\attackerPos[\varepsilon]{q,\{ p' \mid p \stepWeak p' \}})$.
By induction hypothesis there is a formula $\chi \in \hmlStrategies(\attackerPos[\varepsilon]{q,\{ p' \mid p \stepWeak p' \}}, e')$
and $\expr^\varepsilon(\chi) \leq e'$;
therefore, by rule (neg) of <ref>,
$\hmlNeg\hmlEps\chi \in \hmlStrategies(\attackerPos[\wedge]{p,q}, e)$.

* Assume $e \in \attackerWin(\defenderPos{p,Q})$.
For every move $\defenderPos{p,Q} \gameMoveX{-\unit{3}} \attackerPos[\wedge]{p,q}$,
it must be the case that $e' := \energyUpdate(e,-\unit{3}) \in \attackerWin(\attackerPos[\wedge]{p,q})$,
so by induction hypothesis there are formulas $\psi_q \in \hmlStrategies(\attackerPos[\wedge]{p,q})$ with $\expr^\wedge(\psi_q) \leq e'$.
Therefore, by rule (conj) of <ref>,
$\hmlAnd{q}{Q} \psi_q \in \hmlStrategies(\defenderPos{p,Q}, e)$,
and $\expr^\varepsilon(\hmlAnd{q}{Q} \psi_q) = \unit{3} + \sup \{ \expr^\wedge(\psi_q) \mid q \in Q \} \leq e$.

* Assume $e \in \attackerWin(\defenderPos[s]{p,Q})$.
Similar to the previous case.

* Assume $e \in \attackerWin(\defenderPos[\eta]{p,\alpha,p',\linebreak[0] \mbox{$Q \setminus Q_\alpha$},Q_\alpha})$.
Then there are moves $\defenderPos[\eta]{p,\alpha,p',\linebreak[0] \mbox{$Q \setminus Q_\alpha$},Q_\alpha} \gameMoveX{-\unit{2}-\unit{3}} \attackerPos[\wedge]{p,q}$
for every $q \in Q \setminus Q_\alpha$;
it must be the case that $e' := \energyUpdate(e,-\unit{2}-\unit{3}) \in \attackerWin(\attackerPos[\wedge]{p,q})$,
so by induction hypothesis there are formulas $\psi_q \in \hmlStrategies(\attackerPos[\wedge]{p,q})$ with $\expr^\wedge(\psi_q) \leq e'$.
Also, for the moves $\defenderPos[\eta]{p,\alpha,p',\linebreak[0] \mbox{$Q \setminus Q_\alpha$},Q_\alpha}\linebreak[0] \gameMoveX{(\updMin{1,6},-1,-1,0,0,0,0,0)} \attackerPos[\eta]{p',Q'} \gameMoveX{-\unit{1}} \attackerPos{p',Q'}$,
it must be the case that $e'' := \energyUpdate(\energyUpdate(e,(\updMin{1,6},-1,-1,0,0,0,0,0)),-\unit{1}) \in \attackerWin(\attackerPos{p',Q'})$,
so by induction hypothesis there is $\varphi' \in \hmlStrategies(\attackerPos{p',Q'},e'')$ with $\expr(\varphi') \leq e''$.

Therefore, by rule (branch conj) of <ref>,
$\hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \{ \psi_q \mid q \in Q \setminus Q_\alpha \} \in \hmlStrategies(\defenderPos[\eta]{p,\alpha,p',\linebreak[0] \mbox{$Q \setminus Q_\alpha$},Q_\alpha}, e)$
and $\expr^\varepsilon(\hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \{ \psi_q \mid q \in Q \setminus Q_\alpha \}) \leq e$.

[][see full proof]

If $\varphi \in \hmlStrategies(\attackerPos{p,Q}, e)$,
then $\varphi$ distinguishes $p$ from $Q$.

By induction over the derivation of $~\cdots \in \hmlStrategies(g, e)$
according to Definitions <ref>, <ref> and <ref> on the claim:

* At attacker positions, if $\varphi \in \hmlStrategies(\attackerPos{p,Q}, e)$,
then $\varphi$ distinguishes $p$ from $Q$;

if $\chi \in \hmlStrategies(\attackerPos[\varepsilon]{p,Q}, e)$ and $Q \stepWeak Q$,
then $\hmlEps\chi$ distinguishes $p$ from $Q$;

* if $\psi \in \hmlStrategies(\attackerPos[\wedge]{p,q}, e)$,
then $\psi$ distinguishes $p$ from $\{ q \}$.

* At defender positions, if $\hmlAndS \Psi \in \hmlStrategies(\defenderPos{p,Q}, e)$,
then $\hmlAndS \Psi$ distinguishes $p$ from $Q$;

* if $\hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi \in \hmlStrategies(\defenderPos[s]{p,Q}, e)$
and $p$
is stable,
then the stable conjunction $\hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi$ distinguishes $p$ from $Q$;

* if $\hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \Psi \in \hmlStrategies(\defenderPos[\eta]{p,\alpha,p',Q \setminus Q_\alpha,Q_\alpha}, e)$
and $Q_\alpha \subseteq Q$,
then the branching conjunction $\hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \Psi$ distinguishes $p$ from $Q$.

Again, to get an inductive property, we actually prove the following:

* At attacker positions, if $\varphi \in \hmlStrategies(\attackerPos{p,Q}, e)$,
then $\varphi$ distinguishes $p$ from $Q$;

* if $\chi \in \hmlStrategies(\attackerPos[\varepsilon]{p,Q}, e)$ and $Q \stepWeak Q$,
then $\hmlEps\chi$ distinguishes $p$ from $Q$;

* if $\psi \in \hmlStrategies(\attackerPos[\wedge]{p,q}, e)$,
then $\psi$ distinguishes $p$ from $\{ q \}$.

* At defender positions, if $\hmlAndS \Psi \in \hmlStrategies(\defenderPos{p,Q}, e)$,
then $\hmlAndS \Psi$ distinguishes $p$ from $Q$;

* if $\hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi \in \hmlStrategies(\defenderPos[s]{p,Q}, e)$
and $p$
is stable,
then the stable conjunction $\hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi$ distinguishes $p$ from $Q$;

* if $\hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \Psi \in \hmlStrategies(\defenderPos[\eta]{p,\alpha,p',Q \setminus Q_\alpha,Q_\alpha}, e)$
and $Q_\alpha \subseteq Q$,
then the branching conjunction $\hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \Psi$ distinguishes $p$ from $Q$.

We prove the result by induction over the derivation of $~\cdots \in \hmlStrategies(g, e)$
according to Definitions <ref>, <ref> and <ref>.

* Assume $\varphi \in \hmlStrategies(\attackerPos{p,Q}, e)$.

Due to rule (delay) in <ref>:
Then $\varphi = \hmlEps\chi$ and for $Q'$ with $Q \stepWeak Q'$
we have $\chi \in \hmlStrategies(\attackerPos[\varepsilon]{p,Q'}, e)$.
By induction hypothesis, $\hmlEps\chi$ distinguishes $p$ from $Q'$,
but then it also distinguishes $p$ from $Q \subseteq Q'$.

Due to rule (early conj) in <ref>:
Note that (early conj) has the premise $\attackerPos{p,Q} \gameMoveX{u} \defenderPos{p,Q}$,
but this move can be a finishing move $\attackerPos{p,\varnothing} \gameMoveX{\zeroVec} \defenderPos{p,\varnothing}$
or an early conjunction move $\attackerPos{p,Q} \gameMoveX{-\unit{5}} \defenderPos{p,Q}$ with $Q \neq \varnothing$.
In either case, we have that $\varphi = \hmlAndS \Psi \in \hmlStrategies(\defenderPos{p,Q}, \energyUpdate(e, u))$.
By induction hypothesis, $\hmlAndS \Psi$ distinguishes $p$ from $Q$,
and this is exactly what we need to prove about $\varphi = \hmlAndS \Psi$.

* Assume $\chi \in \hmlStrategies(\attackerPos[\varepsilon]{p,Q}, e)$ and $Q \stepWeak Q$.

Due to rule (procr) in <ref>:
Then there exists $p \stepWeak p'$ such that $\chi \in \hmlStrategies(\attackerPos[\varepsilon]{p',Q}, e)$.
By induction hypothesis, we have that $\hmlEps\chi$ distinguishes $p'$ from $Q$,
but then it also distinguishes $p$ from $Q$.

Due to rule (observation) in <ref>:
Then $\chi = \hmlObs{a}\varphi$
and there are $p \step{a} p'$ and $Q \step{a} Q'$ such that $\varphi \in \hmlStrategies(\attackerPos{p',Q'},\energyUpdate(e,-\unit{1}))$.
By induction hypothesis we have that $\varphi$ distinguishes $p'$ from $Q'$.
Therefore, $p \in \hmlSemantics{\chi}{}{} \subseteq \hmlSemantics{\hmlEps\chi}{}{}$.
If there were some $q \in Q \cap \hmlSemantics{\hmlEps\chi}{}{}$,
then we would have a path $q \stepWeak q' \step{a} q'' \in \hmlSemantics{\varphi}{}{}$.
But $q' \in Q$ because $Q \stepWeak Q$ and therefore $q'' \in Q' \cap \hmlSemantics{\varphi}{}{} = \varnothing$.
Therefore $\hmlEps\chi$ distinguishes $p$ from $Q$.

Due to rule (late conj) in <ref>:
Then $\chi\! \in\! \hmlStrategies(\defenderPos{p,Q},e)$.
By induction hypothesis, $\chi$ distinguishes $p$ from $Q$.
As in the previous case,
we use $Q \stepWeak Q$ to get that $\hmlEps\chi$ distinguishes $p$ from $Q$.

Due to rule (stable) in <ref>:
Then $\chi = \hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi$ and $\chi \in \hmlStrategies(\defenderPos[s]{p, \{ q \in Q \mid \mbox{$q \centernot{\step{\tau}}$} \}}, e)$.
By induction hypothesis, $\chi$ distinguishes $p$ from the stable states in $Q$.
Therefore, $p \in \hmlSemantics{\chi}{}{} \subseteq \hmlSemantics{\hmlEps\chi}{}{}$.
Instable states do not satisfy $\hmlNeg\hmlOpt{\tau}\hmlTrue$,
so if there were some instable $q \in Q \cap \hmlSemantics{\hmlEps\chi}{}{}$,
then we would have a path $q \stepWeak \mbox{$q' \centernot{\step{\tau}}$}$
with $q' \in \hmlSemantics{\chi}{}{}$.
But $q' \in Q$ because $Q \stepWeak Q$,
so $q'$ cannot satisfy $\chi$ by induction hypothesis.
Therefore $\hmlEps\chi$ distinguishes $p$ from all states in $Q$.

Due to rule (branching conj) in <ref>:
Then $\chi \in \hmlStrategies(\defenderPos[\eta]{p,\alpha,\linebreak[0] p',\mbox{$Q \setminus Q_\alpha$},Q_\alpha})$
(for some $\alpha$, $p'$ and $Q_\alpha \subseteq Q$).
By induction hypothesis, $\chi$ distinguishes $p$ from $Q$.
As in the previous case,
we use $Q \stepWeak Q$ to get that $\hmlEps\chi$ distinguishes $p$ from $Q$.

* Assume $\psi \in \hmlStrategies(\attackerPos[\wedge]{p,q}, e)$.

Due to rule (pos) in <ref>:
Then $\psi$ has the form $\hmlEps\chi$ and $\chi \in \hmlStrategies(\attackerPos[\varepsilon]{p, Q'},\linebreak[0] \energyUpdate(e, (\updMin{1,6},0,0,0,\linebreak[0] 0,0,0,0)))$ for $\{q\} \stepWeak Q'$.
By induction hypothesis, $\hmlEps\chi$ distinguishes $p$ from $Q'$,
and because $q \in Q'$, it also distinguishes $p$ from $q$.

Due to rule (neg) in <ref>:
Then $\psi$ has the form $\hmlNeg\hmlEps\chi$ and $\chi \in \hmlStrategies(\attackerPos[\varepsilon]{q,P'}, \linebreak[0] \energyUpdate(e, (\updMin{1,7},0,0,0,\linebreak[0] 0,0,0,-1)))$ for $\{p\} \stepWeak P'$.
By induction hypothesis, $\hmlEps\chi$ distinguishes $q$ from $P'$,
and because $p \in P'$, its negation $\psi$ distinguishes $p$ from $q$.

* Assume $\hmlAndS \Psi \in \hmlStrategies(\defenderPos{p,Q}, e)$.

Due to rule (conj) in <ref>:
Then $\Psi$ can be written as $\{ \psi_q \mid q \in Q \}$,
where $\psi_q \in \hmlStrategies(\attackerPos[\wedge]{p,q},\linebreak[0] \energyUpdate(e, -\unit{3}))$.
By induction hypothesis, $\psi_q$ distinguishes $p$ from $q$,
so also $\hmlAndS \Psi$ distinguishes $p$ from $q$.
Because this holds for every $q \in Q$,
we have that $\hmlAndS \Psi$ distinguishes $p$ from $Q$.

* Assume $\hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi \in \hmlStrategies(\defenderPos[s]{p,Q}, e)$ and $p$ is stable.

Due to rule (stable conj) in <ref>:
Then $\Psi$ can be written as $\{ \psi_q \mid q \in Q \}$,
where $\psi_q \in \hmlStrategies(\attackerPos[\wedge]{p,q},\linebreak[0] \energyUpdate(e, -\unit{4}))$.
By induction hypothesis, $\psi_q$ distinguishes $p$ from $q$.
Because this holds for every $q \in Q$ and $p$ is stable,
we have that $\hmlAndS \{ \hmlNeg\hmlObs{\tau}\hmlTrue \} \cup \Psi$ distinguishes $p$ from $Q$.

* Assume $\hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \Psi \in \hmlStrategies(\defenderPos[\eta]{p,\alpha,p',Q \setminus Q_\alpha,Q_\alpha}, e)$ and $Q_\alpha \subseteq Q$.

Due to rule (branch conj) in <ref>:
Then $\Psi$ can be written as $\{ \psi_q \mid q \in Q \setminus Q_\alpha \}$,
where $\psi_q \in \hmlStrategies(\attackerPos[\wedge]{p,q},\linebreak[0] \energyUpdate(e, -\unit{2}-\unit{3}))$.
By induction hypothesis, $\psi_q$ distinguishes $p$ from $q$.
Because this holds for every $q \in Q \setminus Q_\alpha$,
we have that $\hmlAndS \Psi$ distinguishes $p$ from $Q \setminus Q_\alpha$.

Additionally, there exist moves $\defenderPos[\eta]{p,\alpha,p',\linebreak[0] \mbox{$Q \setminus Q_\alpha$},Q_\alpha} \gameMove \attackerPos[\eta]{p',Q'} \gameMove \attackerPos{p',Q'}$
where $p \step{\alpha} p'$, $Q_\alpha \step{\hmlOpt{\alpha}} Q'$,
and $\varphi \in \hmlStrategies(\attackerPos{p,Q},\linebreak[0] \energyUpdate(\energyUpdate(e,\allowbreak(\updMin{1,6},0,0,0,\linebreak[0] 0,0,0,0)),-\unit{1}))$.
By induction hypothesis, $\varphi$ distinguishes $p'$ from $Q'$,
so $\hmlOpt{\alpha}\varphi$ distinguishes $p$ from $Q_\alpha$.

Together we have that $\hmlAndS \{ \hmlOpt{\alpha}\varphi' \} \cup \Psi$ distinguishes $p$ from $Q$.

§ ALGORITHMS, REFINEMENTS, AND VARIATIONS

This section explains how to use the game in algorithms (<ref>) and then makes a few notes that are of interest in the algorithmic context.

In <ref>, we discuss how to lower complexity at the cost of losing the clear modal link that <ref> cherished.
<ref> explains how to cover divergence preservation and completed observations through pre-processing.
<ref> hints at possibilities of how to include further linear-time notions, which need an additional dimension.

§.§ Deciding All Equivalences at Once

The full spectroscopy energy game can be used in algorithms to decide behavioral equivalences.
Our prototype implementation [3] can be tried out on <https://equiv.io> with source on <https://github.com/benkeks/equivalence-fiddle/>.

The game allows checking individual equivalences by instantiating it to start with an energy vector $e_N$ from <ref>.
The remaining reachability game can be played with (usually exponential) time and space complexities depending on the selected vector.
Precisely if the attacker wins from $\attackerPos{p, \{q\}}$, then $p \not\bPreord{\mathit{N}} q$.
Their strategy can be seen as a witness distinguishing formula along the lines of <ref>.
Preferring clever moves speeds up the algorithm; for instance, if one has arbitrarily many conjunctions at one's disposal, selecting those if there are multiple right-hand side processes reduces the game to polynomial size.

More generally, one can decide all equivalences at once by computing attacker budgets $\attackerWin(\attackerPos{p, \{q\}})$.
The output will inform about the most fitting preorders to relate and distinguish $p$ and $q$.
As explained in [4], this has space complexity $\bigo(\relSize{G})$ and time complexity $\relSize{\gameMove} \cdot 2^{\bigo(o)}$ for a concrete spectrum,

where $o$ is the out-degree of $\gameMove$.
For this paper's full spectroscopy game, $\gameSpectroscopy$:
$\relSize{G_\vartriangle} \in \bigo (\relSize{\step{\cdot}} \cdot 3^{\relSize{\proc}})$,
$\relSize{\gameMove_\vartriangle} \in \bigo (\relSize{\step{\cdot}} \cdot \relSize{\proc} \cdot 3^{\relSize{\proc}})$, and
$o_\vartriangle \in \bigo (\relSize{\step{\cdot}} \cdot 2^{\relSize{\proc}})$,
because of the defender branching positions and their surroundings.
This amounts to double-exponential time complexity.
The next subsection discusses how to alleviate this.

§.§ Linear instead of Exponential Out-Degree

That branching conjunctions lead to double-exponentiality seems off:
These moves are for $\eta$- and branching bisimilarity,
which are known to be at the less expensive (sub-cubic [14]) end of equivalence problems.
De Frutos Escrig et al.'s branching bisimulation game [9] is polynomially sized.

And indeed, linear out-degree would suffice if we were to reformulate the branching conjunction part of the game to be closer to other definitions of $\eta$- and branching bisimilarity.
We provide an explicit definition in Appendix <ref>.

Such a reformulation would break the implication from distinguishing formulas $\hmlBA$ to attacker winning budgets (<ref>) in some instances.
As far as we see, this problem goes away in a less fine-grained spectrum where conjunctions are not counted.
So, in most algorithmic instances, the simplified game of Appendix <ref> would be just right.
For the theoretical work of the present paper to have one characterization that aligns with the quantified notions of observability nicely, however, the simplification is not admissible.

§.§ Divergence Preservation and Completed Observations

Logic and game, as we have presented them, are blind to divergence and to completed observations.
Van Glabbeek [12] uses additional modalities:
$\Delta$ for divergence with $\hmlSemantics{\Delta}{}{} \defEq \{p \mid p \step{\tau}^\omega\}$;
$0$ for completed observations with $\hmlSemantics{0}{}{} \defEq \{p \mid \forall a. \mbox{$p \centernot{\step{a}}$} \}$
(and $\lambda \defEq 0 \lor \Delta$).

We have decided against including these in the game.
At least on finite-state systems, they may be understood to be special action observations.
In this view, divergence and completion are something to be modelled (or added through pre-processing) into a system $\system$ before turning to our game of equivalence questions on $\system'$.

For $0$, the transformation from $\system$ to $\system'$ is obvious:
Add a $p \step{\checkmark} \bot$ to the transition system for each $p \in \proc$ where  for every $a \in \actions \setminus \{\tau\}$ (with $\checkmark$ and $\bot$ fresh).
Then $\hmlSemantics{\hmlObs{\checkmark}\hmlTrue}{\smash{\system'}}{}\!\! = \hmlSemantics{0}{\smash{\system}}{}\!$.

For finite-state systems, divergence can be addressed by an argument from Groote et al. [14].
Add $p \step{\delta} \bot$ to the transition system for each $p \in \proc$ that lives on a $\tau$-cycle $p \step{\tau}^+ p$.
Then $\hmlSemantics{\hmlEps\hmlObs{\delta}\hmlTrue}{\smash{\system'}}{}\!\! = \hmlSemantics{\Delta}{\smash{\system}}{}$.
Note that the unary diverges-while operator of divergence-preserving branching bisimilarity [8], $\Delta \varphi$, is then naturally expressed as branching conjunction $\hmlEps\hmlAndS\{\hmlObs{\delta}\hmlTrue, \varphi\}$.

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

§.§ Revivals, Failure Traces, and Ready Traces

While many readers will feel that the spectrum of <ref> already is quite crowded, others might miss (stable) revivals, failure traces, and ready traces, which are relevant to the CSP community [18].

These notions demand to differentiate between the modal depth of the deepest positive conjunct and of the other positive conjuncts.
For instance, ready traces may have one arbitrarily deep positive conjunct at each conjunction, but all the others are capped to modal depth 1.
Thus, these equivalences need an additional dimension for measurements.

Bisping [4] shows how to include this aspect into the expressiveness metric and the game for notions that have no special treatment of internal behavior.
This comes at at the cost of making conjunctions more complicated,
but in principle, can be transferred to the present game.

§ CONCLUSION: SEMANTICS FOR EVERYONE!

In the interview accompanying their CONCUR'21 test-of-time award [1],
Nestmann and Pierce recount how the turning point of their work on distributed choice encodings [17] was joining forces with Milner and Jensen of the “Pi-club” in Edinburgh to find a notion of equivalence fitting their needs.
But not everyone has a Pi-club at their disposal.
Using this paper's game, one can mechanically survey the linear-time–branching-time spectrum with silent moves.
We thus hope this new application of energy games to semantics will prove useful for future research into concurrency theory and expressiveness.

[1]
Barwell, A.D., Ferreira, F., Yoshida, N.: CONCUR test-of-time award for the
period 1994–97 interview with Uwe Nestmann and Benjamin C.
Pierce. Journal of Logical and Algebraic Methods in Programming
125,  100744 (2022). 10.1016/j.jlamp.2021.100744,

[2]
Bell, C.J.: Certifiably sound parallelizing transformations. In: Gonthier, G.,
Norrish, M. (eds.) Certified Programs and Proofs: CPP, LNCS, vol. 8307, pp.
227–242. Springer, Cham (2013). 10.1007/978-3-319-03545-1_15

[3]
Bisping, B.: Linear-time–branching-time spectroscope (2023).
10.5281/zenodo.6726493, archived on Zenodo

[4]
Bisping, B.: Process equivalence problems as energy games. In: Enea, C., Lal,
A. (eds.) Computer Aided Verification. pp. 85–106. Springer Nature
Switzerland, Cham (2023). 10.1007/978-3-031-37706-8_5

[5]
Bisping, B., Jansen, D.N., Nestmann, U.: Deciding all behavioral equivalences
at once: A game for linear-time–branching-time spectroscopy. Logical Methods
in Computer Science  18(3) (2022). 10.46298/lmcs-18(3:19)2022

[6]
Bisping, B., Montanari, L.: A game characterization for contrasimilarity. In:
Dardha, O., Castiglioni, V. (eds.) Proceedings Combined 28th International
Workshop on Expressiveness in Concurrency and 18th Workshop on Structural
Operational Semantics, Electronic Proceedings in Theoretical Computer
Science, vol. 339, pp. 27–42. Open Publishing Association (2021).

[7]
Fahrenberg, U., Juhl, L., Larsen, K.G., Srba, J.: Energy games in multiweighted
automata. In: Cerone, A., Pihlajasaari, P. (eds.) Theoretical Aspects of
Computing – ICTAC 2011, LNCS, vol. 6916, pp. 95–115. Springer, Heidelberg
(2011). 10.1007/978-3-642-23283-1_9

[8]
Fokkink, W., van Glabbeek, R., Luttik, B.: Divide and congruence III: From
decomposition of modal formulas to preservation of stability and divergence.
Information and Computation  268,  104435 (2019).

[9]
de Frutos Escrig, D., Keiren, J.J.A., Willemse, T.A.C.: Games for
bisimulations and abstraction. Logical Methods in Computer Science
13(4:15),  1–40 (2017). 10.23638/LMCS-13(4:15)2017

[10]
Gazda, M., Fokkink, W., Massaro, V.: Congruence from the operator's point of
view: Syntactic requirements on modal characterizations. Acta Informatica
57(3–5),  329–351 (2020). 10.1007/s00236-019-00355-5

[11]
van Glabbeek, R.J.: The linear time–branching time spectrum: extended
abstract. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR'90, LNCS, vol. 458,
pp. 278–297. Springer, Berlin (1990). 10.1007/BFb0039066

[12]
van Glabbeek, R.J.: The linear time–branching time spectrum II: The
semantics of sequential systems with silent moves; extended abstract. In:
Best, E. (ed.) CONCUR'93, LNCS, vol. 715, pp. 66–81. Springer, Berlin
(1993). 10.1007/3-540-57208-2_6

[13]
van Glabbeek, R.J.: The linear time–branching time spectrum I: The semantics
of concrete, sequential processes. In: Bergstra, J.A., Ponse, A., Smolka,
S.A. (eds.) Handbook of Process Algebra, chap. 1, pp. 3–99. Elsevier,
Amsterdam (2001). 10.1016/B978-044482830-9/50019-9

[14]
Groote, J.F., Jansen, D.N., Keiren, J.J.A., Wijs, A.J.: An $\bigo(m \log n)$
algorithm for computing stuttering equivalence and branching bisimulation.
ACM Transactions on Computational Logic (TOCL)  18(2),  13:1–13:34
(2017). 10.1145/3060140

[15]
Kupferman, O., Shamash Halevy, N.: Energy games with resource-bounded
environments. In: Klin, B., Lasota, S., Muscholl, A. (eds.) 33rd
International Conference on Concurrency Theory: CONCUR, LIPIcs, vol. 243, pp.
19:1–19:23. Schloss Dagstuhl – Leibniz-Zentrum für Informatik,
Saarbrücken (2022). 10.4230/LIPIcs.CONCUR.2022.19

[16]
Milner, R.: Communication and Concurrency. Prentice-Hall, Inc., Upper Saddle
River, NJ, USA (1989)

[17]
Nestmann, U., Pierce, B.C.: Decoding choice encodings. Information and
Computation  163(1),  1–59 (2000). 10.1006/inco.2000.2868

[18]
Roscoe, A.W.: Revivals, stuckness and the hierarchy of CSP models. Journal of
Logic and Algebraic Programming  78(3),  163–190 (2009).

§ PROOFS

§ AN ALTERNATIVE SPECTROSCOPY GAME

The operational definition for branching bisimilarity (for instance in [8]) usually reads rather like:

$\bEquiv{BB}$ is the greatest symmetric relation such that $p \bEquiv{BB} q$ and $p \step{\alpha} p'$ implies $\alpha = \tau$ and $p' \bEquiv{BB} q$, or $q \stepWeak q' \step{\alpha} q''$ for some $q', q''$ with $p \bEquiv{BB} q'$ and $p' \bEquiv{BB} q''$.

If we were to read this definition directly as a game, it differs from the branching conjunction moves in <ref>, because the latter requires the attacker to name as $Q_\alpha$ ex-ante which $q'$ to challenge directly and which ones only after the $\alpha$ step, and to have one continuation for the whole $Q_\alpha$ group.
A reformulation closer to the operational definition of $\eta$- and branching bisimilarity would read:

The simplified spectroscopy energy game $\gameSpectroscopyClever^\system$
extends <ref> by

* defender branching positions 17em
$\defenderPos[\eta]{p,\alpha,p',Q} \in G_\defenderSubscript$,

* attacker branching clause positions 17em
$\attackerPos[\eta]{p,\alpha,p',q} \in G_\attackerSubscript$,

* attacker branching positions 17em
$\attackerPos[\eta]{p,Q} \in G_\attackerSubscript$,

where $p, p' \in \proc$, $Q \in \powerSet{\proc}$ and $\alpha \in \actions$, and seven kinds of moves:

* branching conj. $\attackerPos[\varepsilon]{p,Q}$
$\gameMoveX{\mathmakebox[8.3em]{0,0,0,0,0,0,0,0}}$$\defenderPos[\eta]{p,\alpha,p'\!,Q}$if $p\!\step{\alpha}\!p'\!$,$Q\!\neq\!\varnothing$

* branching answer $\defenderPos[\eta]{p,\alpha,p'\!,Q}$$\gameMoveX{\mathmakebox[6em]{0,\textcolor{etaColor}{-1},-1,0,0,0,0,0}}$$\attackerPos[\eta]{p,\alpha,p',q}$if $q \in Q$,

* br. observation $\attackerPos[\eta]{p,\alpha,p',q}$$\gameMoveX{\mathmakebox[6em]{\updMin{1,6},0,0,0,0,0,0,0}}$$\attackerPos[\eta]{p',Q'}$if $\{ q \} \step{\hmlOpt{\alpha}} Q'$,

* br. reset $\attackerPos[\eta]{p,\alpha,p',q}$$\gameMoveX{\mathmakebox[6em]{0,0,0,0,0,0,0,0}}$$\attackerPos[\wedge]{p,q}$,

* early br. accounting$\attackerPos[{\makebox[0pt][l]{$\scriptscriptstyle\eta$}}]{p,Q}$
$\gameMoveX{\mathmakebox[8.3em]{-1,0,0,0,-1,0,0,0}}$$\defenderPos{p,Q}$if $Q \neq \varnothing$,

* early br. finishing$\attackerPos[{\makebox[0pt][l]{$\scriptscriptstyle\eta$}}]{p,\varnothing}$

* late br. accounting $\attackerPos[{\makebox[0pt][l]{$\scriptscriptstyle\eta$}}]{p,Q}$
$\gameMoveX{\mathmakebox[8.3em]{-1,0,-1,0,0,0,0,0}}$$\attackerPos[\varepsilon]{p,Q'}$if $Q \stepWeak Q'$.

The simplified game part encodes nested conjunctions like $\hmlAndS\{ \hmlOpt{\alpha} \formulaHighlight{\hmlAndS} \Psi', \psi_1, \ldots\}$ or the cheaper $\hmlAndS\{ \hmlOpt{\alpha} \formulaHighlight{\hmlEps \hmlAndS} \Psi', \psi_1, \ldots\}$.
The $\Psi'$ are the formulas from after branching observation moves, while the $\psi_i$ come from the resets.
More formally:

For the simplified spectroscopy game, we extend the rules of <ref> as follows:

[ε]p,Q u [η]p,α,p',Q

e' = (e, u) ∈([η]p,α,p',Q)

χ∈([η]p,α,p',Q, e')

χ∈([ε]p,Q, e)
*[left=branch early cont]
[η]p, Q u p,Q

e' = (e, u) ∈(p,Q)

φ∈(p,Q, e')

φ∈([η]p, Q, e)
*[left=branch late cont]
[η]p, Q u [ε]p,Q'

e' = (e, u) ∈([ε]p, Q')

χ∈(p,Q, e')

χ∈([η]p, Q, e)
*[left=branch conj]
[η]p,α,p',Q u [η]p, α, p', q u' g_q

e_q = ((e, u), u') ∈(g_q)

ψ_q ∈(g_q, e_q)

for each  q ∈Q

Q_α= {q_α∈Q |∃Q'g_q_α = [η]p', Q' }

φ_α= merge({ψ_q_α |q_α∈Q_α})

({α φ_α} ∪{ ψ_q |q ∈Q ∖Q_α}) ∈([η]p,α,p',Q, e)

where $\mathrm{merge}(\Psi) := \begin{cases}
\hmlEps \hmlAndS \mathrm{flatten}(\Psi) & \text{ if each $\psi \in \Psi \setminus \{\hmlTrue\}$ starts with $\hmlEps$}\\
\hmlAndS \mathrm{flatten}(\Psi) & \text{ otherwise}
\end{cases}$

and $\mathrm{flatten}(\Psi) := \bigcup_{\psi \in \Psi} \begin{cases}
\Psi' & \text{ if } \psi = \hmlAndS \Psi'\\
\{\psi \} & \text{ otherwise}
\end{cases}$.

However, the counting of conjunctions in this game does not align well with our theorems:
Sometimes the inner conjunction $\hmlAndS \Psi'$ might be unifiable to contain only one element, such that a cheapest attack formula needs one fewer conjunction level than what the game predicts.
<ref> would not hold for this formulation.

This is a rather theoretical problem:
Notions that allow branching/$\eta$ observations do not care about precise counting of conjunctions; either there are immediate conjunctions or there are none.
Therefore, an implementation not caring about the very-cheapest formulas in the sense of this paper, and only interested in notions where $(e_N)_2 > 0$ implies $(e_N)_3, (e_N)_4, (e_N)_5 \in \{0, \infty\}$, can employ the simpler formulation of <ref>.

For $\attackerWin$ of $\gameSpectroscopyClever$, we obtain a time complexity of $2^{\bigo(\relSize{\actions} \cdot \relSize{\proc})}$, because

$\relSize{\gameMove_\blacktriangle} \in \bigo (\relSize{\step{\cdot}} \cdot \relSize{\proc} \cdot 2^{\relSize{\proc}})$ and
$o_\blacktriangle \in \bigo (\relSize{\actions} \cdot \relSize{\proc})$ only.