《计算机学报》文章摘要   全文下载
文章题目	一种求解认知难题的模型检测方法
作者	骆翔宇1)，2) 苏开乐3) 顾明1)
作者单位	1)(清华大学软件学院信息系统安全教育部重点实验室 北京 100084) 2)(桂林电子科技大学计算机与控制学院 广西桂林 541004) 3)(北京大学信息科学技术学院 北京 100871)
发表年份	2010
发表月份	3期(406—414)
文章摘要	摘要 用公告逻辑建模并求解和与积认知难题.提出一种动态认知模型，将环境认知模型与公告导致的认知模型线性组合，从而在时态认知逻辑模型检测技术中扩展支持公告逻辑的建模与验证.该模型检测方法不仅可以用于搜索认知难题的所有解，而且可以验证相关的时态认知性质，这一特性是当前认知逻辑模型检测工具MCK、MCMAS和DEMO不能完全支持的.作者采用OBDD开发了相关的符号化模型检测工具MCTK并对和与积难题进行建模和验证，实验结果说明了文中方法的正确性和高效性. 关键词 模型检测；OBDD；公告逻辑；时态认知逻辑；和与积难题 中图法分类号 TP301 DOI号: 10.3724/SP.J.1016.2009.00406