Gastvortrag: Rob van Glabbeek: Axiomatising Probabilistic Weak and Branching Bisimilarity

Dienstag, 03.09.2019, 11.00 Uhr

Ort: RWTH Aachen University, Informatikzentrum - Ahornstr. 55, Hörsaal AH 1

Vortragender: Rob van Glabbeek (Data61, Australien)

 

Abstract: 

In classifying bisimulation equivalences on processes with probabilistic and nondeterministic choice, I consider 5 dimensions of design decisions:

1. Strong, weak or branching bisimilarity.

2. Optionally stability respecting and/or divergence preserving.

3. Does one allow combined or interpolated transitions, i.e. convex closure?

4. Can weak derivations have an unbounded length?

5. Is a bisimulation a state-based relation (or a decomposable relation on distributions), or a distribution-based one (and only weakly decomposable)?

Today I look at weak and branching bisimilarity, for now without preserving stability or divergence. It has been established that not allowing combined transitions leads to a failure of transitivity, so I do us convex closure. Deng and Palamidessi encountered insurmountable problems in creating complete axiomatisations for regular processes when sticking with bounded weak derivations. Hence I advocate infinitary ones, which may also be more natural.

This yields a four point semantic lattice, with branching finer than weak and state-based finer than distribution based. I present a complete axiomatisation of state-based weak bisimilarity for regular processes.

This is joint work with Nick Fisher. I also present a complete axiomatisation of distribution-based branching bisimilarity for finite processes. This is joint work with Jan Friso Groote and Erik de Vink.