We have studied the dual of bisimulation: the notion of “apartness”. Intuitively, two elements are apart if there is a positive way to distinguish them. Apartness is the dual of bisimilarity in a precise categorical sense: apartness is an initial algebra and gives rise to an induction principle.

In the talk we will focus on the inductive nature of apartness, described by a least fixed point, which can therefore be defined via proof rules. In particular we look at weak forms of bisimulation on labelled transition systems, where silent (τ) steps are included. We define an apartness notion that corresponds to weak bisimulation and another one that corresponds to branching bisimulation. The proof rules for apartness can e.g. be used to show that two states of a labelled transition system are not branching bismilar. To support the apartness view on labelled transition systems, we cast a number of well-known properties of branching bisimulation in terms of branching apartness and prove them.