Bisimulation for probabilistic transition systems : a coalgebraic approach

E.P. Vink, de, J.J.M.M. Rutten

    Research output: Contribution to journalArticleAcademicpeer-review

    93 Citations (Scopus)

    Abstract

    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 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 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.
    Original languageEnglish
    Pages (from-to)271-293
    Number of pages23
    JournalTheoretical Computer Science
    Volume221
    Issue number2
    DOIs
    Publication statusPublished - 1999

    Fingerprint

    Dive into the research topics of 'Bisimulation for probabilistic transition systems : a coalgebraic approach'. Together they form a unique fingerprint.

    Cite this