Branching bisimulation congruence for probabilistic systems

S. Andova, S. Georgievska, N. Trcka

Research output: Contribution to journalArticleAcademicpeer-review

13 Citations (Scopus)
3 Downloads (Pure)


A notion of branching bisimilarity for the alternating model of probabilistic systems, compatible with parallel composition, is defined. For a congruence result, an internal transition immediately followed by a non-trivial probability distribution is not considered inert. A weaker definition of branching bisimilarity for the same model has been given earlier. Here we show that our branching bisimulation is the coarsest congruence for parallel composition that is included in the weaker version. To support the use of the present equivalence as a reduction technique, we also show that probabilistic CTL formulae are preserved by our equivalence, and we provide a polynomial-time algorithm deciding branching bisimilarity.
Original languageEnglish
Pages (from-to)58-72
JournalTheoretical Computer Science
Issue number1
Publication statusPublished - 2012


Dive into the research topics of 'Branching bisimulation congruence for probabilistic systems'. Together they form a unique fingerprint.

Cite this