基于动作的多智能体系统时态认知逻辑模型检测
发布时间：2021-10-20 01:00
多智能体系统模型检测在分布式系统分析领域越来越受到研究者们的重视。传统的时态逻辑模型检测可以建模和验证多智能体系统时间性质规范。但是多智能体系统的模型检测技术越来越趋向于拟人化方向发展。对于智能体群体通过策略合作保证某个系统性质的成立这一情景,传统的时态逻辑是无法描述的。另外,对智能体知识的建模和验证也是十分重要的科学问题。本文提出的一种基于动作的时态认知逻辑（ATL*K）能够有效地描述多智能体系统协议和认知特性。此逻辑可分为时态部分和认知部分:时态部分有线性时态和基于动作的分叉时态;认知部分是对知识性质的扩展,加入全知和公共知识等知识形态。如何判定智能体合作保证系统性质的成立和智能体知识性质的成立是模型检测基于动作的时态认知逻辑的关键性问题。本文提出了一种混合迁移系统（Mixed Transition System,MTS）,在该系统模型M下提出验证各类ATL*K逻辑公式的模型检测算法。总结文章给出的基于动作的多智能体系统时态认知逻辑模型检测的研究,主要的研究工作可概括如下:（1）基于传统的多智能体系统Kripke结构,提出基于动作的解释系统模型IS和推导模型M,给出了M的描述语言及...
【文章来源】：华侨大学福建省
【文章页数】：63 页
【学位级别】：硕士
【文章目录】：
摘要
Abstract
第1章 引言
1.1 研究背景和意义
1.1.1 模型检测起源与意义
1.1.2 模型检测技术的应用和发展
1.2 国内外研究现状
1.2.1 多智能体系统基于动作的逻辑研究现状
1.2.2 多智能体时态认知逻辑模型检测
1.3 本课题的主要研究内容与创新点
1.3.1 研究内容
1.3.2 创新点
1.4 论文的框架结构
1.5 本章小结
第2章 基础理论
2.1 形式化验证技术
2.1.1 定理证明
2.1.2 模型检测
2.2 符号运算技术
2.2.1 OBDD
2.2.2 SAT
2.3 知识推理
2.3.1 语法和语义
2.3.2 可判定性及公理系统
2.3.3 完备性和复杂度
2.4 本章小结
第3章 时态认知逻辑ATL*K及其形式模型
3.1 多智能体系统Kripke模型
3.2 时态逻辑CTL*
3.3 时态认知逻辑ATL*K及其形式模型
3.3.1 动作的引入以及合作保证语义
3.3.2 基于动作的多智能体系统形式模型
3.3.3 ATL*K的语法语义
3.4 本章小结
第4章 ATL*K模型检测
4.1 不动点计算
4.2 基于OBDD的ATL*K模型检测
4.2.1 动作映射
4.2.2 带可观察变量的有限状态程序
4.2.3 全局可达状态集
4.2.4 基于动作的时态算子的模型检测
4.2.5 基于局部命题的知识算子模型检测
4.2.6 ATL*K符号模型检测算法实现框架
4.3 ATL*K模型检测的建模语言设计
4.3.1 环境的定义
4.3.2 智能体的定义
4.3.3 建模语言形式规范
4.4 本章小结
第5章 囚徒与灯泡问题
5.1 问题描述
5.2 解决问题的协议分析及其建模
5.3 基于MCTK的模型检测验证
5.4 本章小结
第6章 总结与展望
6.1 研究总结
6.2 展望未来工作
参考文献
致谢
个人简历、在校期间发表的学术论文和研究成果
【参考文献】：
期刊论文
[1]一种基于认知模型检测的Web服务组合验证方法[J]. 骆翔宇,谭征,苏开乐,吴立军. 计算机学报. 2011(06)
[2]一种求解认知难题的模型检测方法[J]. 骆翔宇,苏开乐,顾明. 计算机学报. 2010(03)
[3]基于自动推理技术的智能规划方法[J]. 吕帅,刘磊,石莲,李莹. 软件学报. 2009(05)
[4]符号化模型检测CTL[J]. 苏开乐,骆翔宇,吕关锋. 计算机学报. 2005(11)
博士论文
[1]多智能体系统的符号模型检测[D]. 骆翔宇.中山大学 2006
[2]多智能体模型、学习和协作研究与应用[D]. 于江涛.浙江大学 2003
硕士论文
[1]基于多智能体系统模型检测与抽象技术的Web服务组合验证[D]. 许兴旺.华侨大学 2014
[2]模型检测在安全协议验证中的研究与应用[D]. 王敏飞.南京航空航天大学 2009
[3]多Agent系统合作认知逻辑的研究[D]. 陆志浩.南京航空航天大学 2008
本文编号：3445940
【文章来源】：华侨大学福建省
【文章页数】：63 页
【学位级别】：硕士
【文章目录】：
摘要
Abstract
第1章 引言
1.1 研究背景和意义
1.1.1 模型检测起源与意义
1.1.2 模型检测技术的应用和发展
1.2 国内外研究现状
1.2.1 多智能体系统基于动作的逻辑研究现状
1.2.2 多智能体时态认知逻辑模型检测
1.3 本课题的主要研究内容与创新点
1.3.1 研究内容
1.3.2 创新点
1.4 论文的框架结构
1.5 本章小结
第2章 基础理论
2.1 形式化验证技术
2.1.1 定理证明
2.1.2 模型检测
2.2 符号运算技术
2.2.1 OBDD
2.2.2 SAT
2.3 知识推理
2.3.1 语法和语义
2.3.2 可判定性及公理系统
2.3.3 完备性和复杂度
2.4 本章小结
第3章 时态认知逻辑ATL*K及其形式模型
3.1 多智能体系统Kripke模型
3.2 时态逻辑CTL*
3.3 时态认知逻辑ATL*K及其形式模型
3.3.1 动作的引入以及合作保证语义
3.3.2 基于动作的多智能体系统形式模型
3.3.3 ATL*K的语法语义
3.4 本章小结
第4章 ATL*K模型检测
4.1 不动点计算
4.2 基于OBDD的ATL*K模型检测
4.2.1 动作映射
4.2.2 带可观察变量的有限状态程序
4.2.3 全局可达状态集
4.2.4 基于动作的时态算子的模型检测
4.2.5 基于局部命题的知识算子模型检测
4.2.6 ATL*K符号模型检测算法实现框架
4.3 ATL*K模型检测的建模语言设计
4.3.1 环境的定义
4.3.2 智能体的定义
4.3.3 建模语言形式规范
4.4 本章小结
第5章 囚徒与灯泡问题
5.1 问题描述
5.2 解决问题的协议分析及其建模
5.3 基于MCTK的模型检测验证
5.4 本章小结
第6章 总结与展望
6.1 研究总结
6.2 展望未来工作
参考文献
致谢
个人简历、在校期间发表的学术论文和研究成果
【参考文献】：
期刊论文
[1]一种基于认知模型检测的Web服务组合验证方法[J]. 骆翔宇,谭征,苏开乐,吴立军. 计算机学报. 2011(06)
[2]一种求解认知难题的模型检测方法[J]. 骆翔宇,苏开乐,顾明. 计算机学报. 2010(03)
[3]基于自动推理技术的智能规划方法[J]. 吕帅,刘磊,石莲,李莹. 软件学报. 2009(05)
[4]符号化模型检测CTL[J]. 苏开乐,骆翔宇,吕关锋. 计算机学报. 2005(11)
博士论文
[1]多智能体系统的符号模型检测[D]. 骆翔宇.中山大学 2006
[2]多智能体模型、学习和协作研究与应用[D]. 于江涛.浙江大学 2003
硕士论文
[1]基于多智能体系统模型检测与抽象技术的Web服务组合验证[D]. 许兴旺.华侨大学 2014
[2]模型检测在安全协议验证中的研究与应用[D]. 王敏飞.南京航空航天大学 2009
[3]多Agent系统合作认知逻辑的研究[D]. 陆志浩.南京航空航天大学 2008
本文编号：3445940
本文链接：https://www.wllwen.com/shekelunwen/ljx/3445940.html
