Branching Bisimilarity with Explicit Divergence

TL;DR

This paper characterizes branching bisimilarity with explicit divergence, proving its equivalence and connecting it to modal logic variants, thus advancing the theoretical understanding of process equivalences.

Contribution

It provides a formal proof of the equivalence of branching bisimilarity with explicit divergence and relates it to modal logic variants.

Findings

Proves that branching bisimilarity with explicit divergence is an equivalence.

Shows it coincides with the original coloured trace definition.

Establishes correspondence with modal logic variants.

Abstract

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