The O(m log n) algorithm for branching bisimulation devised by Groote/Jansen/Keiren/Wijs was primarily directed towards Kripke structures and not to labelled transition systems. To verify branching bisimulation for LTSs an explicit translation is made to Kripke structures. This means that the complexity for LTSs actually is O(m (log n + log |Act|)) and in practice the memory requirements are very high (but still O(m+n)). Together with David Jansen a dedicated algorithm has been constructed which only requires O(m log n) and practically the current algorithm also  outperforms existing algorithms especially in memory requirements.

This is very much work in progress.