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

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

作　　者：邹蒙蒙[1] 骆翔宇[2] 骆灵洁[1] 

机构地区：[1]桂林电子科技大学计算机科学与工程学院,广西桂林541004 [2]华侨大学计算机科学与技术学院,福建厦门361021

出　　处：《桂林电子科技大学学报》2012年第3期227-232,共6页Journal of Guilin University of Electronic Technology

基　　金：国家自然科学基金(61170028);华侨大学中央高校基本科研业务项目(JB-GJ1001);华侨大学高层次人才科研启动项目(11BS108)

摘　　要：为了保证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.

关 键 词：KQML 多智能体系统 模型检测 MCMAS 

分 类 号：TP393.09[自动化与计算机技术—计算机应用技术]