一种求解认知难题的模型检测方法

• 作者: 苏开乐 顾明 骆翔宇
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 模型检测 OBDD 公告逻辑 时态认知逻辑 和与积难题
• 年，卷（期）: 2010,（3）
• 所属期刊栏目: 研究论文与技术报告
• 页码范围: 406-414
• 页数: 9页
• 分类号: TP301
• 字数: 9411字
• 语种: 中文
• DOI: 10.3724/SP.J.1016.2009.00406

摘要

用公告逻辑建模并求解和与积认知难题.提出一种动态认知模型,将环境认知模型与公告导致的认知模型线性组合,从而在时态认知逻辑模型检测技术中扩展支持公告逻辑的建模与验证.该模型检测方法不仅可以用于搜索认知难题的所有解,而且可以验证相关的时态认知性质,这一特性是当前认知逻辑模型检测工具MCK、MCMAS和DEMO不能完全支持的.作者采用OBDD开发了相关的符号化模型检测工具MCTK并对和与积难题进行建模和验证,实验结果说明了文中方法的正确性和高效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	苏开乐	北京大学信息科学技术学院	8	82	5.0	8.0
2	顾明	清华大学软件学院信息系统安全教育部重点实验室	72	1054	16.0	30.0
3	骆翔宇	清华大学软件学院信息系统安全教育部重点实验室	13	65	5.0	7.0