Bisimulation for probabilistic transition systems : a coalgebraic approach

The notion of bisimulation as proposed by Larsen and Skou for discrete probabilistic transition systems is shown to coincide with a coalgebraic definition in the sense of Aczel and Mendler in terms of a set functor, which associates to a set its collection of simple probability distributions. This coalgebraic formulation makes it possible to generalize the concepts of discrete probabilistic transition system and probabilistic bisimulation to a continuous setting involving Borel probability measures. A functor M is introduced that yields for a metric space its collection of Borel probability measures. Under reasonable conditions, this functor exactly captures generalized probabilistic bisimilarity. Application of the final coalgebra paradigm to a functor based on M then yields an internally fully abstract semantical domain with respect to probabilistic bisimulation, which is therefore well-suited for the interpretation of probabilistic specification and stochastic programming concepts.