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

作者：王海洋; 段振华^*; 田聪^*

来源：软件学报, 2019, 30(02): 231-243.

DOI：10.13328/j.cnki.jos.005584

• 交替投影时序逻辑
• 多智能体系统
• 模型检测

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

• 单位
  综合业务网理论及关键技术国家重点实验室; 西安电子科技大学