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

Benjamin Bisping, David N. Jansen, Uwe Nestmann

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 li…