用于验证多智能体系统的APTL模型检测器

• 作者: 段振华 王海洋 田聪
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 交替投影时序逻辑 多智能体系统 模型检测
• 年，卷（期）: 2019,（2）
• 所属期刊栏目: 系统软件与软件工程
• 页码范围: 231-243
• 页数: 13页
• 分类号: TP311
• 字数: 9101字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005584

摘要

由于经典的线性时序逻辑表达能力有限,设计并开发了基于交替投影时序逻辑(alternating projection temporal logic,简称APTL)的模型检测工具.根据王海洋等人提出的APTL符号模型检测方法,设计并实现了APTL模型检测器MCMAS_APTL.该工具可用于多智能体系统(multi-agent system,简称MAS)的性质验证.MCMAS_APTL检查MAS是否满足具体性质的过程如下:首先,用解释系统编程语言(interpreted system programminglanguage,简称ISPL)描述要验证的系统IS,用APTL公式P描述要验证的性质;然后,符号化表示系统IS,并将非P转化为范式;最后,计算所有满足非P的路径的起始状态集合.如果得到的状态集合中包含系统的初始状态,则说明系统不满足公式P;反之,则说明系统满足公式P.详细阐述了实现MCMAS_APTL的过程,并且通过验证机器人足球赛的例子展示了MCMAS APTL的性能.