APTL模型检测方法及多智能体系统验证的研究

发布时间：2020-07-16 09:46

【摘要】：模型检测是一种应用于验证并发系统性质的自动化技术,其中系统性质规约用时序逻辑公式描述,检测过程依赖于高效灵活的基于图理论的可达问题算法。模型检测技术吸引了国内外学者的高度重视得到了飞速发展,并广泛应用到社会的各个领域,如电路设计、协议验证等。随着人工智能技术的发展,智能产品出现在人们的生活中,如智能家居、百度地图的智能路线规划、网站推荐和过滤商品、机器人足球赛。虽然这些智能产品给人们带来了极大便利,但是也引入了很多安全隐患。因此,近年来很多学者致力于研究如何保障智能产品的安全性问题,其中模型检测方法已经应用到人工智能领域中并取得了显著成果。模型检测中系统的性质用时序逻辑公式形式化描述,所以时序逻辑在模型检测方法中起着至关重要的作用。交替时序逻辑(Alternating Temporal Logic,简称ATL)是Alur提出的应用于验证反应系统性质的时序逻辑,其将反应系统的交互过程看作是开放系统与外界环境的博弈过程。命题投影时序逻辑(Proposition Projection Temporal Logic,简称PPTL)可以方便的描述有穷或无穷状态路径的性质;PPTL公式简洁直观并且可以表达完全正则性质,在模型检测领域起着举足轻重的作用。交替投影时序逻辑(Alternating Projection Temporal Logic,简称APTL)是PPTL的扩展逻辑,APTL不仅可以表达经典时序逻辑LTL可以表达的性质,而且可以表达与区间相关的顺序和循环性质以及开放系统和多智能体系统中与博弈相关的性质。本文完善了APTL的逻辑规则,研究改进了检查APTL公式可满足性的方法,并且设计了APTL符号模型检测算法。为了实现自动化验证,开发了APTL公式的可满足性检查工具和APTL模型检测器。具体工作包括以下四方面:第一,本文完善并证明了APTL的逻辑规则,基于APTL逻辑规则研究设计了将APTL公式转化为范式的算法并开发了转化器。接着改进了已有的APTL公式的可满足性检查方法,具体的检查过程为:(i)将APTL公式转化为范式,根据公式的范式构造范式图并且转化为自动机;(ii)将得到的自动机进行转化并化简;(iii)判断得到的最简自动机是否为空,如果自动机为空那么对应的APTL公式不可满足,反之亦然。第二,本文研究设计了APTL的基于BDD的符号模型检测算法,详细过程为:(i)用解释系统编程语言描述要验证的系统,用APTL公式描述要验证的系统性质;(ii)符号化表示系统并且将公式的‘非’转化为范式;(iii)计算所有满足公式的‘非’的路径的起始状态集合。如果得到的状态集合中包含系统的初始状态,说明系统不满足该APTL公式;反之则满足该公式。第三,APTL公式的可满足性检查是后续进行系统验证的前提。根据APTL公式可满足性检查算法开发实现了检查工具APTL2BCG,检查了三组代表性APTL公式以展示工具强大的工作能力。接着开发了APTL模型检测器MCMAS APTL实现了检测过程的自动化,由于从底层开发一个完整的模型检测器是很复杂的,因此MCMAS APTL利用了多智能体系统模型检测器MCMAS的系统符号化部分。第四,为了将APTL模型检测方法应用到更复杂的系统验证中,我们完善了检测器MCMAS APTL的功能并提高了检测效率。文中验证了云计算中的单点登录中的OpenID协议以及机器人足球赛的场景,说明了检测器MCMAS APTL具有较高的工作效率和实用性。
【学位授予单位】：西安电子科技大学
【学位级别】：博士
【学位授予年份】：2018
【分类号】：TP18;TP301.1

【相似文献】

相关期刊论文 前8条

1 方建印;谢欣欣;;具有饱和输入和通信约束的多智能体系统的包含控制[J];河南工程学院学报(自然科学版);2016年04期

2 李健;沈艳军;刘允刚;;线性多智能体系统一致性的自适应动态规划求解方法[J];系统科学与数学;2016年07期

3 杨瑞;叶冬;;多智能体系统一致性研究[J];山东工业技术;2017年07期

4 张晓娇;崔宝同;齐斌;;二阶多智能体系统一致性的几个条件（英文）[J];控制工程;2017年04期

5 姜香菊;纪志坚;孙方刚;李自强;;二阶多智能体系统的能观性[J];工业控制计算机;2017年05期

6 朱美玲;赵蕊;徐勇;;速度不可测的异构多智能体系统一致性分析[J];计算机工程与科学;2017年09期

7 莫立坡;于永光;;多智能体系统的有限时间旋转环绕控制（英文）[J];自动化学报;2017年09期

8 闻国光;黄俊;于玉洁;;异质多智能体系统在固定拓扑下的分组一致性[J];北京交通大学学报;2016年03期

相关会议论文 前10条

1 张文广;郭振凯;;一类高阶多智能体系统的一致控制研究[A];中国自动化学会控制理论专业委员会C卷[C];2011年

2 陈增强;;多智能体系统鲁棒编队跟踪控制及包容控制研究[A];2015年中国自动化大会摘要集[C];2015年

3 张馨元;陈中高;吉国华;;基于多智能体系统的建筑自动排布工具原型研究[A];数字技术·建筑全生命周期——2018年全国建筑院系建筑数字技术教学与研究学术研讨会论文集[C];2018年

4 杨洪勇;刘启明;;时延不同的二阶多智能体系统的编队控制[A];2009中国控制与决策会议论文集（1）[C];2009年

5 薛宏涛;沈林成;;基于协进化方法的多智能体系统及其符号演绎理论模型[A];第二十六届中国控制会议论文集[C];2007年

6 虞文武;;多智能体系统分布式协同控制与优化的新挑战[A];2015年中国自动化大会摘要集[C];2015年

7 杨洪勇;路兰;李晓;;时延多智能体系统的群集运动[A];第五届全国复杂网络学术会议论文（摘要）汇集[C];2009年

8 梁泉;许晓鸣;张钟俊;;多智能体系统智能体协作层的设计与实现[A];1995年中国智能自动化学术会议暨智能自动化专业委员会成立大会论文集（下册）[C];1995年

9 鄢昒易;何潇;王子栋;周东华;;一类LPV多智能体系统的分布式故障诊断[A];第25届中国控制与决策会议论文集[C];2013年

10 ;索引[A];2012-2013控制科学与工程学科发展报告[C];2014年

相关重要报纸文章 前1条

1 本报记者 常丽君;让人类与机器人联手[N];科技日报;2016年

相关博士学位论文 前10条

1 游秀;一类非匹配非线性多智能体系统的分布式一致性控制[D];燕山大学;2017年

2 万颖;时滞网络系统的动力学分析及采样控制[D];东南大学;2017年

3 马婧瑛;多智能体系统的性能优化[D];西安电子科技大学;2017年

4 张婷;几类多智能体系统量化学习一致性研究[D];西安电子科技大学;2017年

5 王海洋;APTL模型检测方法及多智能体系统验证的研究[D];西安电子科技大学;2018年

6 张卓;多智能体系统协同控制方法及在分布式卫星应用研究[D];哈尔滨工业大学;2017年

7 李平;复杂条件下多智能体系统的鲁棒一致性控制研究[D];电子科技大学;2017年

8 陈凯锐;多智能体系统一致性控制若干问题研究[D];广东工业大学;2017年

9 徐云剑;几类多智能体系统的一致性问题研究[D];广东工业大学;2017年

10 梁洪晶;多智能体系统的协同控制及输出调节问题研究[D];东北大学;2016年

相关硕士学位论文 前10条

1 杨东岳;存在外部扰动的线性多智能体系统分布式协调控制[D];哈尔滨工业大学;2017年

2 梁建;异质网络中二阶多智能体系统分布式协调控制[D];哈尔滨工业大学;2017年

3 刘洪明;复杂网络滞后同步与牵制控制多智能体系统一致性[D];杭州电子科技大学;2018年

4 张增英;多智能体系统群集行为动力学分析及控制方法研究[D];兰州交通大学;2017年

5 谢朝龙;基于Web的多智能体系统实验平台的设计与实现[D];哈尔滨工业大学;2018年

6 陈亚楠;异质多智能体系统基于事件的一致性和包围控制[D];青岛大学;2018年

7 付芳芳;高阶线性时滞多智能体系统的一致性[D];曲阜师范大学;2018年

8 陈春杨;带有随机延迟和拓扑的多智能体系统一致性研究[D];江南大学;2018年

9 李晓;多智能体系统L_2-L_∞一致性研究[D];安徽工业大学;2018年

10 桑成艳;几类随机多智能体系统的一致性研究[D];安徽工业大学;2018年

本文编号：2757845