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

TL;DR

This paper introduces a unified energy game framework to characterize and decide various weak behavioral equivalences in process theory, bridging the gap between branching bisimilarity and weak trace semantics.

Contribution

It provides the first generalized game characterization for the spectrum with silent steps, connecting energy budgets with logical expressiveness.

Findings

A multi-dimensional energy game characterizes weak behavioral equivalences.

The approach relates attacker-winning budgets to logical sublanguages.

The method unifies decision procedures for multiple equivalences.

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.