Proving Behavioural Apartness: A Coalgebraic Approach to Distinguishing States

This paper proposes behavioural apartness, defined by dualising behavioural equivalence, as an alternative to cobisimilarity for proving distinguishability of states in coalgebras. The authors provide a sound and complete proof system for behavioural apartness that allows for finite proofs, in contrast to the universal quantification required by the cobisimilarity approach.