Relating Apartness and Branching Bisimulation Games
Jurriaan Rot, Sebastian Junges, Harsh Beohar

TL;DR
This paper explores the relationship between apartness relations and branching bisimulation games, demonstrating how game-winning strategies correspond to proofs of non-bisimilarity in finite state systems.
Contribution
It establishes a formal connection between apartness and two-player bisimulation games, extending the understanding of behavioral equivalences in coalgebraic models.
Findings
Winning configurations for Spoiler correspond to apartness proofs.
Results apply to image-finite systems for strong bisimilarity.
Results apply to finite systems for branching bisimilarity.
Abstract
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).
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
