• 主题
高级搜索  >
历史搜索 清空历史
首页> 中文学位 >基于动作的多智能体系统时态认知逻辑模型检测
【6h】

基于动作的多智能体系统时态认知逻辑模型检测

代理获取
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

多智能体系统模型检测在分布式系统分析领域越来越受到研究者们的重视。传统的时态逻辑模型检测可以建模和验证多智能体系统时间性质规范。但是多智能体系统的模型检测技术越来越趋向于拟人化方向发展。对于智能体群体通过策略合作保证某个系统性质的成立这一情景，传统的时态逻辑是无法描述的。另外，对智能体知识的建模和验证也是十分重要的科学问题。 本文提出的一种基于动作的时态认知逻辑(ATL*K)能够有效地描述多智能体系统协议和认知特性。此逻辑可分为时态部分和认知部分：时态部分有线性时态和基于动作的分叉时态；认知部分是对知识性质的扩展，加入全知和公共知识等知识形态。如何判定智能体合作保证系统性质的成立和智能体知识性质的成立是模型检测基于动作的时态认知逻辑的关键性问题。本文提出了一种混合迁移系统(Mixed Transition System,MTS)，在该系统模型M下提出验证各类ATL*K逻辑公式的模型检测算法。 总结文章给出的基于动作的多智能体系统时态认知逻辑模型检测的研究，主要的研究工作可概括如下： （1）基于传统的多智能体系统Kripke结构，提出基于动作的解释系统模型IS和推导模型M，给出了M的描述语言及其语法规范。 （2）提出了基于动作的时态认知逻辑ATL*K以及在M上的语义解释系统。此逻辑融合ATL逻辑，线性时态逻辑和认知逻辑，有着超过ATLK和CTL*K的强大表达能力。 （3）使用了一种后映射的方法把动作变量映射到状态变量中，形成全新的动作状态组(Action State Tuple，AST)，再基于AST提出了多智能体混合迁移系统模型MTS，这样形式模型M上的模型检测判定问题就转成了混合迁移系统模型是否能满足ATL*K公式的问题。我们根据MTS和不动点计算以及局部命题等理论，给出ATL*K模型检测算法理论证明和实现过程。 （4）把算法理论实现于我们的模型检测工具MCTK中。对“囚徒与灯泡”问题进行深入分析后，利用扩展后的MCTK工具验证了此问题中以ATL*K逻辑描述的系统规范。

著录项

  • 作者

    李勇;

  • 作者单位

    华侨大学;

  • 授予单位 华侨大学;
  • 学科 计算机系统结构
  • 授予学位 硕士
  • 导师姓名 骆翔宇;
  • 年度 2016
  • 页码
  • 总页数
  • 原文格式 PDF
  • 正文语种 中文
  • 中图分类 TN9;
  • 关键词

    动作; 多智能体系统; 时态认知逻辑;

相似文献

  • 中文文献
  • 外文文献
  • 专利
代理获取

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号