软件学报

作者：王海洋,段振华,田聪

单位：王海洋，西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007111,段振华，西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007102,田聪，西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007103

关键词：交替投影时序逻辑;多智能体系统;模型检测

基金：国家自然科学基金（61732013，61420106004）

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

来源：2019年第2期

《软件学报》期刊编辑部

查看软件学报杂志2019年第2期