An efficient algorithm to determine probabilistic bisimulation

J.F. Groote, Héctor J. Rivera Verduzco, E.P. de Vink

Research output: Contribution to journalArticleAcademicpeer-review

11 Citations (Scopus)
79 Downloads (Pure)


We provide an algorithm to efficiently compute bisimulation for probabilistic labeled transition systems, featuring non-deterministic choice as well as discrete probabilistic choice. The algorithm is linear in the number of transitions and logarithmic in the number of states, distinguishing both action states and probabilistic states, and the transitions between them. The algorithm improves upon the proposed complexity bounds of the best algorithm addressing the same purpose so far by Baier, Engelen and Majster-Cederbaum (Journal of Computer and System Sciences 60:187–231, 2000). In addition, experimentally, on various benchmarks, our algorithm performs rather well; even on relatively small transition systems, a performance gain of a factor 10,000 can be achieved.
Original languageEnglish
Article number131
Number of pages22
Issue number9
Publication statusPublished - 5 Sept 2018


  • probabilistic system with nondeterminism; probabilistic labeled transition system; probabilistic bisimulation; partition-refinement algorithm
  • Probabilistic labeled transition system
  • Probabilistic bisimulation
  • Partition-refinement algorithm
  • Probabilistic system with nondeterminism


Dive into the research topics of 'An efficient algorithm to determine probabilistic bisimulation'. Together they form a unique fingerprint.

Cite this