R.J. van Glabbeek (NICTA), B. Luttik (TU Eindhoven)
& N. Trčka (TU Eindhoven)
Original report: June 2006
Revised report: October 2007
We consider the relational characterisation of branching
bisimulation with explicit divergence. We prove that it is an
equivalence relation and that it coincides with the
original definition of branching bisimulation 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.
Keywords: Concurrency, labelled transition systems,
modal logic, branching bisimulation, divergence, coloured traces.
- Preliminary report (June 2006) available as
dvi,
ps,
pdf and
tex file.
In this version Lemma 5.3, and hence the proof of Corollary
5.4, is incorrect. This mistake has been corrected in
October 2007.
- Revised report (October 2007) available as
dvi,
ps,
pdf and
tex file.
- A further revision (December 2008), with a slightly
different title, obtained by adding didactic background
material, is available at
http://theory.stanford.edu/~rvg/abstracts.html#67.
Rob van Glabbeek
rvg@CS.Stanford.EDU