| 和与积数迷的符号化模型检测 |
| |
| 引用本文： | 骆翔宇 古天龙 董荣胜. 和与积数迷的符号化模型检测[J]. 计算机科学, 2008, 35(5): 184-186 |
| |
| 作者姓名： | 骆翔宇 古天龙 董荣胜 |
| |
| 作者单位： | 桂林电子科技大学计算机与控制学院,桂林,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]. Computer Science, 2008, 35(5): 184-186 |
| |
| Authors: | LUO Xiang-yu GU Tian-long DONG Rong-sheng |
| |
| Affiliation: | LUO Xiang-yu GU Tian-long DONG Rong-sheng (Sheool of Computer&Control,Guilin University of Electronic Technology,Guilin 541004,China) |
| |
| Abstract: | The Sum-and-Product Riddle is a famous number puzzle.The riddle is modeled in a modal logic called public announcement logic,which is interpreted on multi-agent Kripke model.The model is symbolically represented as a multi-agent finite state program.Based on the semantics of the logic,a symbolic model checking approach to the riddle is developed by using the symbolic model checking algorithm for logic of knowledge under the semantics of interpreted systems with local propositions.The approach is then implem... |
| |
| Keywords: | Symbolic model checking Multi-agent system Temporal logic Public announcement logic |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
