Paper Info
Title
An O(mlogn) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation.
Abstract
We provide a new algorithm to determine stuttering equivalence with time complexity O(mlogn), 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, where Act is the set of actions in a labeled transition system. Theoretically, our algorithm substantially improves upon existing algorithms, which all have time complexity of the form O(mn) at best. Moreover, it has better or equal space complexity. Practical results confirm these findings: they show that our algorithm can outperform existing algorithms by several orders of magnitude, especially when the Kripke structures are large. The importance of our algorithm stretches far beyond stuttering equivalence and branching bisimulation. The known O(mn) algorithms were already far more efficient (both in space and time) than most other algorithms to determine behavioral equivalences (including weak bisimulation), and therefore they were often used as an essential preprocessing step. This new algorithm makes this use of stuttering equivalence and branching bisimulation even more attractive.
Year
DOI
Venue
2017
10.1145/3060140
ACM Trans. Comput. Log.
Keywords
Field
DocType
Branching bisimulation,algorithm
Kripke structure,Discrete mathematics,Binary logarithm,Combinatorics,Of the form,Spacetime,Algorithm,Preprocessor,Bisimulation,Time complexity,Stuttering equivalence,Mathematics
Journal
Volume
Issue
ISSN
18
2
1529-3785
Citations 
PageRank 
References 
6
0.50
22
Authors
4
Name
Order
Citations
PageRank
Jan Friso Groote11626154.19
David N. Jansen230924.09
J. J. A. Keiren3978.13
Anton Wijs420322.84