Equivalences for Silent Transitions in Probabilistic Systems (Extended Abstract)

S. Andova, T.A.C. Willemse

    Research output: Contribution to journalArticleAcademic

    1 Citation (Scopus)
    23 Downloads (Pure)


    We address abstraction in the setting of probabilistic reactive systems, and study its formal underpinnings for the strictly alternating model. In particular, we define the notion of branching bisimilarity and study its properties by studying two other equivalence relations, viz. coloured trace equivalence and branching bisimilarity using maximal probabilities. We show that both alternatives coincide with branching bisimilarity. The alternative characterisations have their own merits and focus on different aspects of branching bisimilarity. Together they give a better understanding of branching bisimilarity. A crucial observation, and, in fact a major motivation for this work is that the notions of branching bisimilarity in the alternating and in the non-alternating model differ, and that the latter one discriminates between systems that are intuitively branching bisimilar.
    Original languageEnglish
    Pages (from-to)53-66
    JournalElectronic notes in theoretical computer science
    Issue number2
    Publication statusPublished - 2005
    Event11th International Workshop on Expressiveness in Concurrency, EXPRESS 2004 - London, United Kingdom
    Duration: 30 Aug 200430 Aug 2004
    Conference number: 11


    • Abstraction
    • Branching bisimulation
    • Probabilistic systems
    • Process theory
    • Coloured trace equivalence

    Fingerprint Dive into the research topics of 'Equivalences for Silent Transitions in Probabilistic Systems (Extended Abstract)'. Together they form a unique fingerprint.

    Cite this