Branching Bisimilarity with Explicit Divergence

Abstract. We consider the relational characterisation of branching bisimilarity with explicit diver-gence. We prove that it is an equivalence and that it coincides with the original definition of branch-ing bisimilarity with explicit divergence in terms of coloured traces. We also establish a correspon-dence with several variants of an action-based modal logic with until- and divergence modalities. 1