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

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.

In Proceedings EXPRESS/SOS 2024, arXiv:2411.13318

References in corpus (7)

• Divide and Congruence III: From Decomposition of Modal Formulas to Preservation of Stability and Divergence
• Unifying the Linear Time-Branching Time Spectrum of Process Semantics
• Deciding All Behavioral Equivalences at Once: A Game for Linear-Time--Branching-Time Spectroscopy
• A Game Characterization for Contrasimilarity
• Explaining Behavioural Inequivalence Generically in Quasilinear Time
• Linear-Time--Branching-Time Spectroscopy Accounting for Silent Steps
• Process Equivalence Problems as Energy Games