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). |
个性服务 |
查看访问统计 |
相关权益政策 |
暂无数据 |
收藏/分享 |
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。
修改评论