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)
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.