Proving Behavioural Apartness
Ruben Turkenburg, Harsh Beohar, Clemens Kupke, Jurriaan Rot
TL;DR
The paper introduces behavioural apartness as the dual notion to behavioural equivalence for $\mathsf{Set}$-based coalgebras, enabling finite inductive proofs of state inequivalence. It provides a soundness and completeness result for finitary endofunctors and a proof system with optimised rules, including one-step coverings to localise reasoning to states reachable in one step. The subdistribution functor $\mathcal{D}_s$ is used as a key motivating case where the classic cobisimilarity rule involves universal quantification over couplings, whereas behavioural apartness yields finite witnesses. The work points toward connections with coalgebraic modal logic and codensity-based approaches, suggesting broader applicability for distinguishing states in probabilistic and nondeterministic systems.
Abstract
Bisimilarity is a central notion for coalgebras. In recent work, Geuvers and Jacobs suggest to focus on apartness, which they define by dualising coalgebraic bisimulations. This yields the possibility of finite proofs of distinguishability for a wide variety of state-based systems. We propose behavioural apartness, defined by dualising behavioural equivalence rather than bisimulations. A motivating example is the subdistribution functor, where the proof system based on bisimilarity requires an infinite quantification over couplings, whereas behavioural apartness instantiates to a finite rule. In addition, we provide optimised proof rules for behavioural apartness and show their use in several examples.