algorithms for computing weak bisimulation equivalence

	algorithms for computing weak bisimulation equivalence
	Li Weisong
	2009
会议名称	3rd International Symposium on Theoretical Aspects of Software Engineering
会议录名称	Proceedings - 2009 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009
会议日期	JUL 29-31,
会议地点	Tianjin, PEOPLES R CHINA
出版地	10662 LOS VAQUEROS CIRCLE, PO BOX 3014, LOS ALAMITOS, CA 90720-1264 USA
出版者	THIRD INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS
ISBN	978-0-7695-3757-3
部门归属	Chinese Acad Sci, Inst Software, Beijing, Peoples R China.
摘要	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.
关键词	Formal Verification Model Checking Time Complexity Transitional Relation Graph Unlabeled Kripke Structure Weak Bisimulation Equivalence Algorithm Computational Complexity Formal Verification Graph Theory
主办者	IEEE Comp Soc, IFIP, Tianjin Normal Univ
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/8308
专题	基础软件与系统重点实验室
推荐引用方式 GB/T 7714	Li Weisong. algorithms for computing weak bisimulation equivalence[C]. 10662 LOS VAQUEROS CIRCLE, PO BOX 3014, LOS ALAMITOS, CA 90720-1264 USA:THIRD INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS,2009.

条目包含的文件
文件名称/大小	文献类型	版本类型	开放类型	使用许可
algorithms for compu（175KB）			开放获取	--	请求全文