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

TL;DR

This paper introduces a game-based method to analyze various weak behavioral equivalences in process theory, accounting for silent steps, using a multi-dimensional energy game approach.

Contribution

It provides the first generalized game characterization of the linear-time--branching-time spectrum with silent steps, unifying multiple equivalences in a single framework.

Findings

A multi-dimensional energy game characterizes weak behavioral equivalences.

The approach relates attacker-winning energy budgets to logical expressiveness.

The method efficiently decides equivalences involving silent steps.

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.