It’s All a Game
摘要
We study the connection between apartness and bisimulation games. Strong apartness has been proposed as a relation for distinguishing states in a labelled transition system. Prior work has shown that there is a clear connection between Hennessy-Milner logic, strong bisimilarity and strong apartness. We show that in a bisimulation game, winning strategies for \(\textsc {Spoiler}\) can be obtained from apartness proofs, and, vice versa, apartness proofs can be produced from winning \(\textsc {Spoiler}\) strategies.