Deciding All Behavioral Equivalences at Once: A Game for Linear-Time--Branching-Time Spectroscopy

TL;DR

This paper presents a generalized bisimulation game that efficiently identifies the finest behavioral equivalences between finite-state processes across the entire linear-time--branching-time spectrum, using logic formulas.

Contribution

It introduces a unified game-based approach to decide all behavioral equivalences simultaneously within the spectrum, extending previous methods.

Findings

The algorithm can determine the most precise behavioral equivalence between processes.

It identifies formulas from the spectrum that distinguish processes.

The approach generalizes existing bisimulation games.

Abstract

We introduce a generalization of the bisimulation game that finds distinguishing Hennessy-Milner logic formulas from every finitary, subformula-closed language in van Glabbeek's linear-time--branching-time spectrum between two finite-state processes. We identify the relevant dimensions that measure expressive power to yield formulas belonging to the coarsest distinguishing behavioral preorders and equivalences; the compared processes are equivalent in each coarser behavioral equivalence from the spectrum. We prove that the induced algorithm can determine the best fit of (in)equivalences for a pair of processes.