Abstract: Discrete Markov Chains describe probabilistic behaviour by indicating with which probabilities states in a directed graph can reach each other. Using weak bisimulation equivalent states can be merged making the graph smaller. In the world of Markov Chains this is often called lumping.

For a long time an O(m n) algorithm existed by Baier and Hermanns to determine weak bisimulation on Markov Chains, m being the number of the edges and n the number of vertices. By using ideas from the new class of efficient branching bisimulation algorithms in combination with an algorithm to efficiently maintain strongly connected components we managed to come up with a average time O(m log^4 n) algorithm, which is nowadays coined as “near linear time”.

The algorithm is so complex that we have no intention to implement it.

This work is a cooperation by David Jansen, Ferry Timmers, Pengfei Yang and Jan Friso Groote