Speaker: Bas Luttik (FM, TU/e)
Title: Branching Bisimulation Equivalence with Explicit Divergence
 
Abstract:
(Joint work with Rob van Glabbeek and Nikola Trcka)

The original notion of branching bisimulation equivalence abstracts entirely 
from divergence (infinite internal activity). This is the reason that the notion 
does not preserve all properties expressible in the logic CTL*-X. The equivalence 
on labeled transition systems that corresponds precisely with the equivalence 
induced by validity of CTL*-X formulas is the notion of divergence sensitive 
branching bisimulation of De Nicola and Vaandrager. However, their equivalence 
has another deficiency: it identifies deadlock and livelock and therefore is not 
a congruence for parallel composition.
 
Branching bisimulation equivalence with explicit divergence extends branching 
bisimulation equivalence with a divergence condition that distinguishes between 
deadlock and livelock. It turns out to be the coarsest congruence for parallel 
composition on transition systems that preserves the validity of CTL*-X formulas. 
In my talk I'll present a convenient relational characterization of branching 
bisimulation equivalence with explicit divergence, and I'll explain 
the connection with the logic CTL*-X.