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

摘要：

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

关键词：模型检测、OBDD、公告逻辑、时态认知逻辑、和与积难题

所属期刊栏目：33

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金重点项目90718039;国家"九七三"重点基础研究发展规划项目基金2010CB328103;国家杰出青年科学基金60725207;国家自然科学基金60763004;广西青年科学基金桂科青0728090;中国博士后科学基金20090450389

在线出版日期：2010-05-10（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：406-414