Proving Behavioural Apartness

TL;DR

This paper introduces behavioural apartness, a dual concept to behavioural equivalence, enabling finite proofs of system distinguishability and improving proof efficiency in coalgebraic models.

Contribution

It defines behavioural apartness by dualising behavioural equivalence, offering finite proof systems and optimized rules for a broad class of state-based systems.

Findings

Behavioural apartness allows finite proofs where bisimilarity requires infinite quantification.

Optimized proof rules improve efficiency in demonstrating system distinguishability.

Application to subdistribution functor showcases practical advantages.

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.