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, Hopcrofts idea of process the smaller half 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.

作者: Weisong Li

作者单位: Institute of Software, Chinese Academy of Sciences Graduate University of Chinese Academy of Sciences Beijing, China

会议类型: 国际会议

会议名称: Third International Symposium on Theoretical Aspects of Software Engineering TASE 2009(第三届软件工程理论国际研讨会)

会议地点: 天津

会议语种:英文

页码: 241-248

在线出版日期: 2009-07-29（万方平台首次上网日期，不代表论文的发表时间）