An O (mlog n) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation

摘要

We provide a new algorithm to determine stuttering equivalence with time complexity O(mlog n), where n is the number of states and mis 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, where Act is the set of actions in a labeled transition system.