Geuvers and Jacobs (LMCS 2021) formulated the notion of apartness relation on state-based systems modelled as coalgebras. In this context apartness is formally dual to bisimilarity, and gives an explicit proof system for showing that certain states are not bisimilar. In the current paper, we relate apartness to another classical element of the theory of behavioural equivalences: that of turn-based two-player games. Studying both strong and branching bisimilarity, we show that winning configurations for the Spoiler player correspond to apartness proofs, for transition systems that are image-finite (in the case of strong bisimilarity) and finite (in the case of branching bisimilarity).

翻译：Geuvers 与 Jacobs (LMCS 2021) 提出了以余代数建模的状态系统上的分离关系概念。在此框架下，分离关系在形式上是互模拟关系的对偶概念，并为证明特定状态间不具有互模拟性提供了显式的证明系统。本文旨在建立分离关系与行为等价理论中另一经典要素——回合制双人博弈——之间的联系。通过研究强互模拟与分支互模拟，我们证明：对于像有限（强互模拟情形）及有限（分支互模拟情形）的转移系统，Spoiler 玩家的获胜配置恰好对应于分离关系证明。