Paper accepted at QAPL2015

Title: Rooted probabilistic branching bisimulation as a congruence

Autores: Matias David Lee y Erik de Vink.

Abstract: We propose a probabilistic transition system specification format, referred to as probabilistic RBB safe, for which rooted probabilistic branching bisimulation is a congruence. The congruence theorem is based on work of Fokkink for the qualitative case. For this to work, the transition system specification theory in the setting of labeled transition systems needs to be extended to deal with probability distributions, both syntactically and semantically. We adapt the notion of probabilistic branching bisimulation from work of Andova et al.\ for the alternating model, to provide a scheduler-free characterization. Counter examples are given to justify the various conditions related to the format.