One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics

TL;DR

This work provides the first generalized game characterization of van Glabbeek's linear-time--branching-time spectrum with silent steps, and relates attacker-winning energy budgets and distinguishing sublanguages of Hennessy--Milner logic that are characterized by eight dimensions of formula expressiveness.

Abstract

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 characterize and decide a wide array of weak 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 that we characterize by eight dimensions of formula expressiveness.

Figures (5)

• Figure 1: How the paper combines the weak spectrum glabbeek1993ltbt and the spectroscopy approach bisping2023equivalenceEnergyGames.
• Figure 2: A pair of processes $\mathsf{P_e}$ and $\mathsf{P_\ell}$ together with versions $\mathsf{P^\tau_e}$ and $\mathsf{P^\tau_\ell}$ of the two where $\mathit{idle}$ has been abstracted into internal $\tau$-behavior.
• Figure 3: Hierarchy of weak behavioral equivalences/preorders, becoming finer towards the top. Each notion $N$ comes with its expressiveness coordinate $e_N$. Lines mean implication of equivalence/preordering from bottom to top.
• Figure 4: Schematic spectroscopy game $\mathcal{G}_\vartriangle$ of Definitions \ref{['def:spectroscopy-delay-game']} (the black part), \ref{['def:spectroscopy-stability-game']} (with position $\textcolor{stabilityColor!50}{(}\textcolor{stabilityColor}{\cdots}\textcolor{stabilityColor!50}{)_\mathtt{d}^{{s}}}$), and \ref{['def:spectroscopy-game-full']} (with positions $\textcolor{stabilityColor!50}{(}\textcolor{stabilityColor}{\cdots}\textcolor{stabilityColor!50}{)_\mathtt{d}^{{s}}}$, $\textcolor{etaColor!50}{(}\textcolor{etaColor}{\cdots}\textcolor{etaColor!50}{)_\mathtt{d}^{{\eta}}}$ and $\textcolor{etaColor!50}{[}\textcolor{etaColor}{\cdots}\textcolor{etaColor!50}{]_\mathtt{a}^{{\eta}}}$).
• Figure 5: Spectroscopy delay game $\mathcal{G}_\varepsilon$ from $\textcolor{gray}{[}\mathsf{A^\tau_e}, \{ \mathsf{A^\tau_\ell}, \mathsf{B^\tau_\ell} \}\textcolor{gray}{]_\mathtt{a}^{{}}}$ for \ref{['exa:attack-formula']}. Each position names minimal attacker-winning budgets (due to the thick arrows) and corresponding distinguishing formulas (pink). Zeros and $\mathbf{0}$-updates are omitted for readability. Also, the game graph under defender-won reflexive position $\textcolor{gray}{[}\mathsf{0},\{ \mathsf{0} \}\textcolor{gray}{]_\mathtt{a}^{{}}}$ (dashed in blue) is omitted.

Theorems & Definitions (21)

• Definition 2.1: Labeled transition system with silent steps
• Example 2.1
• Definition 2.2: Branching Hennessy--Milner logic
• Definition 2.3: Distinguishing formulas and preordering languages
• Example 2.2
• Remark 2.1
• Definition 2.4: Branching bisimilarity, operationally
• proof
• Definition 2.5: Energies
• Definition 2.6: Formula prices