| 和与积数迷的符号化模型检测 |
| |
| 引用本文： | 骆翔宇,古天龙,董荣胜. 和与积数迷的符号化模型检测[J]. 中国药品标准, 2008, 0(5): 184-186 |
| |
| 作者姓名： | 骆翔宇 古天龙 董荣胜 |
| |
| 作者单位： | 骆翔宇（桂林电子科技大学计算机与控制学院,桂林,541004）;古天龙（桂林电子科技大学计算机与控制学院,桂林,541004）;董荣胜（桂林电子科技大学计算机与控制学院,桂林,541004） |
| |
| 基金项目： | 国家自然科学基金 , 广西青年科学基金 |
| |
| 摘 要： | 和与积是一个著名的数迷问题.采用公告逻辑对该问题进行建模,将其Kripke模型符号化表示为多智能体有限状态程序,并在其上采用一种基于局部命题解释系统语义的知识逻辑符号化模型检测算法计算该问题的所有解.在时态逻辑模型检测器NuSMV基础上扩展实现了本文算法,然后在相同实验平台上用动态认知建模工具DEMO对该问题进行求解.实验表明,我们的算法不仅结果正确,而且在运行效率上与DEMO相比占有绝对优势.
|
| 关 键 词： | 符号化模型检测 多智能体系统 时态逻辑 公告逻辑 |
Symbolic Model Checking for Sum and Product Riddle |
| |
| LUO Xiang-yu,GU Tian-long,DONG Rong-sheng. Symbolic Model Checking for Sum and Product Riddle[J]. , 2008, 0(5): 184-186 |
| |
| Authors: | LUO Xiang-yu GU Tian-long DONG Rong-sheng |
| |
| Abstract: | |
| |
| Keywords: | |
|
| 点击此处可从《中国药品标准》浏览原始摘要信息 |
|
点击此处可从《中国药品标准》下载全文 |
|
