Apartness is the opposite (dual) of bisimulation. Intuitively, two states in a system are apart if there is a positive way to distinguish them. Apartness is an inductive notion, so we have a deduction system for proving that two states are apart, and if we cannot prove they are apart, they are bisimilar. This works for various notions of bisimilarity, especially for those where the systems can be described as co-algebras. So apartness gives an inductive view on the co-inductive notion of bisimulation.

There is also a logical view on bisimulation: two states are bisimilar if-and-only-if they satisfy the same formulas of Hennessy-Milner logic (HML), where the precise syntax for HML formulas and the notion of satisfaction depends on the type of bisimulation one wants to talk about.

In the talk we will focus on this “if-and-only-if” in its dual form, using the inductive nature of apartness. We will prove (directly, without referring to bisimulation): Two states are apart if-and-only-if there is a Hennessy-Milner logic formula that distinguishes them.

The “only if” is proved by constructing the HML formula by induction on the proof that two states are apart. The “if” part is proven by induction on the HML formula. We will discuss this for Labelled Transition Systems (LTS) with strong bisimulation, weak bisimulation and branching bisimulation. For branching bisimulation, the proof is remarkably tricky and we propose a slightly different variant of HML, PHMLU, (Positive Hennessy-Milner Logic with Until) for branching bisimulation that simplifies the proof. We believe that PHMLU has merit of its own, as being the “natural logic” for branching bisimulation/apartness.