摘要：Weak bisimulations are typically used in process algebras where silent stepsare used to abstract from internal behaviours. They facilitate relatingimplementations to specifications. When an implementation fails to conform toits specification, pinpointing the root cause can be challenging. In this paperwe provide a generic characterisation of branching-, delayed-, $\eta$- andweak-bisimulation as a game between Spoiler and Duplicator, offering anoperational understanding of the relations. We show how such games can be usedto assist in diagnosing non-conformance between implementation andspecification. Moreover, we show how these games can be extended to distinguishdivergences.
