Algorithms for Computing Weak Bisimulation Equivalence

Weak bisimulation equivalence is an important relation in formal verification. There is only one specific algorithm for computing weak simulation equivalence on unlabeled Kripke structure. We exploit two ways to improve the algorithm for this problem. First, the transitional relation graph is reduced to its s.c.c component graph. Second, Hopcroftpsilas idea of ldquoprocess the smaller halfrdquo is incorporated to further improve time complexity. These two methods avoid the computation of transitive reflexive closure of the original transitional relation and achieve better time complexity in most practical cases of model checking.