Branching bisimulation is a behavioural equivalence relation on labelled transition systems that takes internal actions into account. While it is slightly coarser than weak bisimulation, it has the advantage that there is a unique branching bisimulation equivalence quotient that can be found efficiently. With m the number of transitions and n the number of states, the classic O(mn) algorithm has recently been replaced by an O(m log n) algorithm, which is unfortunately rather complex. This paper provides a much more straightforward O(m log n) algorithm. Benchmarks show that in practice this new algorithm is faster and more memory efficient than its predecessors.

(Joint work with Jan Friso Groote, Jeroen Keiren and Anton Wijs)