An O(m log n) algorithm for stuttering equivalence and branching bisimulation

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|Act|+log n)) time. Theoretically, our algorithm substantially improves upon existing algorithms which all have time complexity O(mn) [2,3,9]. 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.