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