An efficient algorithm to determine probabilistic bisimulation
J.F.~Groote,  H.J.~Rivera Verduzco and E.P.~de Vink

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 & Majster-Cederbaum
(Journal of Computer and System Sciences 60:187--231, 2000). Also
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.