A simpler O(m log n) algorithm for branching bisimilarity on labelled transition systems

TL;DR

This paper introduces a simpler, faster, and more memory-efficient $O(m \\log n)$ algorithm for computing branching bisimilarity on labelled transition systems, improving over previous complex algorithms.

Contribution

It combines existing ideas to produce a simpler and more efficient algorithm for branching bisimilarity, outperforming prior methods in speed and memory usage.

Findings

The new algorithm has a complexity of $O(m \\log n)$.

Benchmarks show it is faster than previous algorithms.

It is more memory-efficient, making it ideal for minimization tasks.

Abstract

Branching bisimilarity is a behavioural equivalence relation on labelled transition systems that takes internal actions into account. It has the traditional advantage that algorithms for branching bisimilarity are more efficient than all algorithms for other weak behavioural equivalences, especially weak bisimilarity. With $m$ the number of transitions and $n$ the number of states, the classic $O(m n)$ algorithm was recently replaced by an $O(m (\log \lvert \mathit{Act}\rvert + \log n))$ algorithm, which is unfortunately rather complex. This paper combines its ideas with the ideas from Valmari. This results in a simpler algorithm with complexity $O(m \log n)$. Benchmarks show that this new algorithm is also faster and often far more memory efficient than its predecessors. This makes it the best option for branching bisimulation minimisation and preprocessing for weak bisimulation of LTSs.