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.

翻译：双相似性是余代数领域的一个核心概念。在近期工作中，Geuvers与Jacobs建议聚焦于分离性，他们通过将余代数双模拟对偶化来定义这一概念。这为各类基于状态的系统提供了有限步可区分性证明的可能性。我们提出行为分离性，其通过将对偶化对象从双模拟转为行为等价来定义。一个典型例子是子分布函子：基于双相似性的证明系统需要对耦合进行无限量化，而行为分离性则能实例化为有限规则。此外，我们为行为分离性提供了优化证明规则，并通过多个实例展示其应用。