基于KQML的多智能体系统建模与验证

A modeling and verification method to multi-agent system based on KQML

为了保证MAS相关属性的可满足性、有效性以及验证的高效性,提出了一种基于KQML通信语言的MAS建模以及能够实现自动验证相关规范的方法。设计并实现了KQML语言转化为完整描述状态转换关系的一组状态迁移七元组的算法,以及从七元组到多智能体模型检测工具MCMAS输入语言ISPL的转化算法,从而实现多智能体系统的自动形式化建模,并用MCMAS对多智能体系统规范的正确性进行验证。实验结果表明,所提出的算法不仅能够验证多智能体系统的时态规范,还能验证其特有的认知规范。

To ensure the satisfiability and the validation of the related properties and the high efficiency in the multi- agent system, a method for realizing the automatic verification of the related properties and the MAS mode based on the knowledge query manipulate language are introduced. It is designed and realized to translate KQML into seven- tuple which can describe completely the state transition relationship and translate seven-tuple into the input language ISPL of the model checker MCMAS, so as to realize the automatically formal modeling and verify the correctness of the multi-agent system specifications via MCMAS. The experimental result shows that the proposed algorithm can verify not only the temporal specifications but also the epistemic specifications of the multi-agent system.