Erik de Vink: On the BEM algorithm for deciding strong probabilistic bisimulation

Event Details

An algorithm for deciding strong probabilistic bisimulation, referred to as BEM, was proposed in 2000 by Baier, Engelen, and Majster-Cederbaum claiming O(m n log n) complexity for the construction of the bisimulation equivalence classes of a probabilistic automaton. Besides so-called Ordered Balanced Trees, the BEM algorithm uses straightforward datastructures. More recently, Groote and Rivera Verduzco proposed an algorithm, referred to as GRV, of the same complexity based on more intricate data structures. The running times of GRV, however, are around 1000 better than those of BEM, on a standard set of benchmarks. Today we take a closer look at how the BEM algorithm works, seeking explanation for the difference in performance compared to the GRV algorithm, leaving GRV for another occasion.