We present the first game characterization of contrasimilarity, the weakest form of bisimilarity. The game is finite for finite-state processes and can thus be used for contrasimulation equivalence checking, of which no tool has been capable to date. A machine-checked Isabelle/HOL formalization backs our work and enables further use of contrasimilarity in verification contexts.

翻译：我们展示了第一个不同的游戏特征,即最弱的两样形式。游戏对有限状态过程是有限的,因此可用于反模拟等同检查,迄今为止还没有工具能够使用。经过机器检查的Isabelle/HOL正式化支持了我们的工作,并允许在核查环境中进一步使用反类似性。