model checking: a coalgebraic approach

ISCAS OpenIR

	model checking: a coalgebraic approach
	Gao Jianhua; Jiang Ying
	2011
会议名称	5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011
会议录名称	Proceedings - 5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011
页码	235-238
会议日期	August 29,
会议地点	Xi'an, Shaanxi, China
收录类别	EI
ISBN	9780769545066
部门归属	(1) State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing 100190 China; (2) Graduate University Chinese Academy of Sciences China
摘要	State explosion problem is the main obstacle of model checking. In this work, we address this problem from a co algebraic point of view. We establish an effective method to prove uniformly the existence of the smallest Kripke structure with respect to bisimilarity, which describes all behaviors of the Kripke structures with no redundancy. We show this smallest Kripke structure generates a minimal one for each given finite Kripke structure and some kind of infinite ones. This method is based on the existence of the final co algebra of a suitable endofunctor and can be generalized smoothly to other co algebraic structures. A naive implementation of this method is developed in Ocaml. © 2011 IEEE.; State explosion problem is the main obstacle of model checking. In this work, we address this problem from a co algebraic point of view. We establish an effective method to prove uniformly the existence of the smallest Kripke structure with respect to bisimilarity, which describes all behaviors of the Kripke structures with no redundancy. We show this smallest Kripke structure generates a minimal one for each given finite Kripke structure and some kind of infinite ones. This method is based on the existence of the final co algebra of a suitable endofunctor and can be generalized smoothly to other co algebraic structures. A naive implementation of this method is developed in Ocaml. © 2011 IEEE.
关键词	Algebra Software Engineering
主办者	IEEE CS; IFIP
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16220
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Gao Jianhua,Jiang Ying. model checking: a coalgebraic approach[C],2011:235-238.