An O(m log n) Algorithm for Stuttering Equivalence and Branching Bisimulation

TL;DR

This paper introduces a new $O(m \, log \, n)$ algorithm for stuttering equivalence and branching bisimulation, significantly improving efficiency over previous methods and enhancing their practical applicability in large systems.

Contribution

The paper presents a novel algorithm with improved time and space complexity for stuttering equivalence and branching bisimulation, outperforming all prior algorithms with $O(m n)$ complexity.

Findings

Algorithm achieves $O(m \, log \, n)$ time complexity.

Practical results show orders of magnitude performance improvements.

Algorithm enhances the utility of behavioral equivalence computations.

Abstract

We provide a new algorithm to determine stuttering equivalence with time complexity $O(m \log n)$, where $n$ is the number of states and $m$ is the number of transitions of a Kripke structure. This algorithm can also be used to determine branching bisimulation in $O(m(\log |\mathit{Act}|+ \log n))$ time where $\mathit{Act}$ is the set of actions in a labelled transition system. Theoretically, our algorithm substantially improves upon existing algorithms which all have time complexity $O(m n)$ at best. Moreover, it has better or equal space complexity. Practical results confirm these findings showing that our algorithm can outperform existing algorithms with orders of magnitude, especially when the sizes of the Kripke structures are large. The importance of our algorithm stretches far beyond stuttering equivalence and branching bisimulation. The known $O(m n)$ algorithms were already far more efficient (both in space and time) than most other algorithms to determine behavioural equivalences (including weak bisimulation) and therefore it was often used as an essential preprocessing step. This new algorithm makes this use of stuttering equivalence and branching bisimulation even more attractive.