A model checking approach for solving epistemic riddles

doi:10.3724/SP.J.1016.2010.00406

CORC > 北京大学 > 信息科学技术学院

	A model checking approach for solving epistemic riddles
	Luo, Xiang-Yu ; Su, Kai-Le ; Gu, Ming
刊名	jisuanji xuebaochinese journal of computers
	2010
DOI	10.3724/SP.J.1016.2010.00406
英文摘要	This paper aims to model and solve the Sum and Product Riddle in public announcement logic. A dynamic epistemic model is proposed, that is the linear temporal combination of the epistemic model of environment and the epistemic models after each announcement, such that the authors' model checking technique for temporal epistemic logic can be extended to support the modeling and verification of public announcement logic. This model checking method not only can help to find all solutions, but also verify related temporal epistemic properties. Such characteristic is not fully supported by the current version of MCK, MCMAS and DEMO. The authors implemented the proposed method in the symbolic model checker MCTK via OBDD and verified the sum and product riddle. The experimental results show that the proposed method is correct and efficient.; EI; 0; 3; 406-413; 33
语种	英语
内容类型	期刊论文
源URL	[http://ir.pku.edu.cn/handle/20.500.11897/327498]
专题	信息科学技术学院
推荐引用方式 GB/T 7714	Luo, Xiang-Yu,Su, Kai-Le,Gu, Ming. A model checking approach for solving epistemic riddles[J]. jisuanji xuebaochinese journal of computers,2010.
APA	Luo, Xiang-Yu,Su, Kai-Le,&Gu, Ming.(2010).A model checking approach for solving epistemic riddles.jisuanji xuebaochinese journal of computers.
MLA	Luo, Xiang-Yu,et al."A model checking approach for solving epistemic riddles".jisuanji xuebaochinese journal of computers (2010).