vai al contenuto della pagina vai al menu di navigazione
 

Seminario "Exploring probabilistic bisimulations"

10/06/2013 dalle 11:00 alle 12:30

Dove DISI, Aula Nadia Busi, Mura Anteo Zamboni 7, Bologna

Aggiungi l'evento al calendario

Lunedì 10 giugno si terrà il seminario "Exploring probabilistic bisimulations" tenuto da Matthew Hennessy del Trinity College Dublin dalle ore 11 alle 12.30 presso l'aula seminario Nadia Busi, Dipartimento di Informatica - Scienza e Ingegneria, Mura Anteo Zamboni 7, Bologna.

 

Abstract:

We take a fresh look at strong probabilistic bisimulations for processes which exhibit both non-deterministic and probabilistic behaviour. We suggest that it is natural to interpret such processes as distributions over states in a probabilistic labelled transition system, a pLTS; this enables us to adapt the standard notion of contextual equivalence to this setting.

We then prove that a novel form of bisimulation equivalence between distributions are both sound and complete with respect to this contextual equivalence. Moreover a very simple extension to HML, Hennessy-Milner Logic, provides finite explanations for inequivalences between distributions. We also show that our bisimulations between distributions in a pLTS are simply an alternative characterisation of a standard notion of probabilistic bisimulation equivalence, defined between states in a pLTS.

Finally we discuss the extent to which a similar theory can be developed for a weak contextual equivalence, in which internal actions are unobservable.

References:

Matthew Hennessy, Exploring probabilistic bisimulations, part I.
Formal Aspects of Computing, Vol 24, number 4-6, pp. 749-768, 2012.

Yuxin Deng and Matthew Hennessy.
On the semantics of Markov automata.
Information and Computation, vol 222, pages 139-268, 2013.