2016/01/07 by Jan Friso Groote, Groote, Jan Friso, Anton Wijs +1
Computer Science · #68Q60 #68Q85 #Algorithms and Data Compression #D.2.4 #Data Structures and Algorithms (cs.DS) #FOS: Computer and information sciences #G.2.2 #Logic in Computer Science (cs.LO) #Machine Learning and Algorithms #Software Engineering Research #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1601.01478
openalex publication_date 2016/01/07 · openalex created_date 2025/10/27 · openalex updated_date 2026/07/28
We provide a new algorithm to determine stuttering equivalence with time\ncomplexity O(m \log n), where n is the number of states and m is the\nnumber of transitions of a Kripke structure. This algorithm can also be used to\ndetermine branching bisimulation in O(m(\log |\Act|+ \log n)) time\nwhere \Act is the set of actions in a labelled transition system.\nTheoretically, our algorithm substantially improves upon existing algorithms\nwhich all have time complexity O(m n) at best. Moreover, it has better or\nequal space complexity. Practical results confirm these findings showing that\nour algorithm can outperform existing algorithms with orders of magnitude,\nespecially when the sizes of the Kripke structures are large. The importance of\nour algorithm stretches far beyond stuttering equivalence and branching\nbisimulation. The known O(m n) algorithms were already far more efficient\n(both in space and time) than most other algorithms to determine behavioural\nequivalences (including weak bisimulation) and therefore it was often used as\nan essential preprocessing step. This new algorithm makes this use of\nstuttering equivalence and branching bisimulation even more attractive.\n