-
题名一种求解认知难题的模型检测方法
被引量:5
- 1
-
-
作者
骆翔宇
苏开乐
顾明
-
机构
清华大学软件学院信息系统安全教育部重点实验室
桂林电子科技大学计算机与控制学院
北京大学信息科学技术学院
-
出处
《计算机学报》
EI
CSCD
北大核心
2010年第3期406-414,共9页
-
基金
国家自然科学基金重点项目(90718039)
国家"九七三"重点基础研究发展规划项目基金(2010CB328103)
+3 种基金
国家杰出青年科学基金(60725207)
国家自然科学基金(60763004)
广西青年科学基金(桂科青0728090)
中国博士后科学基金(20090450389)资助
-
文摘
用公告逻辑建模并求解和与积认知难题.提出一种动态认知模型,将环境认知模型与公告导致的认知模型线性组合,从而在时态认知逻辑模型检测技术中扩展支持公告逻辑的建模与验证.该模型检测方法不仅可以用于搜索认知难题的所有解,而且可以验证相关的时态认知性质,这一特性是当前认知逻辑模型检测工具MCK、MCMAS和DEMO不能完全支持的.作者采用OBDD开发了相关的符号化模型检测工具MCTK并对和与积难题进行建模和验证,实验结果说明了文中方法的正确性和高效性.
-
关键词
模型检测
OBDD
公告逻辑
时态认知逻辑
和与积难题
-
Keywords
model checking
ordered binary decision diagram
public announcement logic
temporal epistemic logics
sum and product riddle
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名和与积数迷的符号化模型检测
- 2
-
-
作者
骆翔宇
古天龙
董荣胜
-
机构
桂林电子科技大学计算机与控制学院
-
出处
《计算机科学》
CSCD
北大核心
2008年第5期184-186,共3页
-
基金
国家自然科学基金(60763004)
广西青年科学基金(D200716).
-
文摘
和与积是一个著名的数迷问题。采用公告逻辑对该问题进行建模,将其Kripke模型符号化表示为多智能体有限状态程序,并在其上采用一种基于局部命题解释系统语义的知识逻辑符号化模型检测算法计算该问题的所有解。在时态逻辑模型检测器NuSMV基础上扩展实现了本文算法,然后在相同实验平台上用动态认知建模工具DEMO对该问题进行求解。实验表明,我们的算法不仅结果正确,而且在运行效率上与DEMO相比占有绝对优势。
-
关键词
符号化模型检测
多智能体系统
时态逻辑
公告逻辑
-
Keywords
Symbolic model checking, Multi-agent system, Temporal logic, Public announcement logic
-
分类号
TP301.6
[自动化与计算机技术—计算机系统结构]
TP212.02
[自动化与计算机技术—检测技术与自动化装置]
-