多智能体系统的符号模型检测

论文摘要

模型检测作为一种有限状态系统的自动化验证技术已得到广泛应用，最近该技术在规划和多智能体系统(MAS)等人工智能领域的应用也越来越受到重视，MAS领域强调智能体的自治性和推理力，采用模态逻辑刻画智能体心智状态(包括智能体的知识，信念，愿望和意图)的演变过程。由于这些模态词的语义解释与标准时态算子不同，因此不能直接将当前的LTL或CTL时态逻辑模型检测工具应用到多智能体系统中。 本文重点研究多智能体系统的规范表示及其模型检测方法。根据智能体知识，信念，愿望和意图的表示和建模需求，提出新的Kripke语义模型，并在这一新的语义模型基础上研究多智能体系统的时态认知逻辑模型检测算法。这里提出的时态认知逻辑是在分支时态逻辑CTL~*语言中加入表示智能体知识，信念，愿望或意图的认知模态词后得到的。该时态认知逻辑有丰富的时态和认知表达能力，用户可以方便地检测智能体认知状态的演变过程。因此，本文研究成果在时态和认知两方面扩展并丰富了当前的多智能体系统模型检测技术。 另一方面，为了大幅缓解模型检测的状态爆炸问题，我们分别采用有序二叉判定图(OBDD)和可满足性(SAT)两种符号计算技术设计本文的符号模型检测算法，使得可验证问题的规模大大增加。 根据本文提出的理论，我们已实现两个高效的符号模型检测工具MCTK和MCKBDI，其中MCTK用于检测智能体的知识，而MCKBDI主要用于检测智能体的信念，愿望和意图。本文的研究成果主要体现在以下几方面： · 提出一个时态逻辑CTL~*的符号模型检测算法。该算法通过tableau构造方法和基于OBDD的不动点计算来判定一个有限状态系统是否满足CTL~*

论文目录

• 中文摘要
• 英文摘要
• 目录
• 第一章 绪论
• 1.1 时态逻辑的模型检测
• 1.2 多智能体系统的模型检测
• 1.3 论文大纲
• 第二章 预备知识
• 2.1 模型检测
• 2.2 符号计算技术
• 2.3 知识推理
• *的符号模型检测'>第三章 时态逻辑CTL^*的符号模型检测
• 3.1 引言
• *'>3.2 时态逻辑CTL^*
• *的符号模型检测'>3.3 CTL^*的符号模型检测
• 3.4 实验结果
• 3.5 小结
• *K的符号模型检测及其工具MCTK'>第四章 时态知识逻辑CTL^*K的符号模型检测及其工具MCTK
• 4.1 引言
• 4.2 带局部变量的解释系统中的知识
• *K的符号模型检测'>4.3 CTL^*K的符号模型检测
• *K符号模型检测工具'>4.4 CTL^*K符号模型检测工具
• 4.5 MCTK输入语言
• 4.6 小结
• 第五章 MCTK在基于信息论的安全协议验证中的应用
• 5.1 引言
• 5.2 就餐保密家协议
• 5.3 Herbivore匿名通信协议
• 5.4 俄罗斯牌协议
• 5.5 小结
• 第六章 同步多智能体系统时态认知逻辑的有界模型检测
• 6.1 引言
• 6.2 同步解释系统
• *K逻辑及其子集'>6.3 CTL^*K逻辑及其子集
• *K逻辑的有界语义'>6.4 ECTL^*K逻辑的有界语义
• *K逻辑有界语义的正确性'>6.5 ECTL^*K逻辑有界语义的正确性
• *K的有界模型检测'>6.6 ECTL^*K的有界模型检测
• 6.7 公式转换的正确性
• 6.8 实例:火车控制系统
• 6.9 小结
• 第七章 多智能体KBDI逻辑的符号模型检测及其工具MCKBDI
• 7.1 引言
• 7.2 KBDI逻辑
• 7.3 KBDI逻辑的模型检测
• 7.4 KBDI符号模型检测工具MCKBDI
• 7.5 实例研究:一个拍卖场景
• 7.6 小结
• 第八章 结论与展望
• 参考文献
• 攻读学位期间发表的论文
• 致谢
• 论文原创性声明