论文部分内容阅读
多Agent系统可以看作是多个独立自主的Agent通过相互通信、交互以及协作对同一个问题进行求解的分布式智能系统。由于通信的单个Agent具有动态性和自主性，如何保证多Agent系统的正确性及有效性便成了现阶段一大挑战。由此，形式化分析与验证多Agent系统越来越成为研究热点。 为了提高多Agent系统的自动化验证程度，支持时态、认知及合作等性质的验证，本文提出将描述多Agent系统通信语言KQML转化到符号模型检测工具MCMAS的输入语言ISPL的一系列转化算法。最后在MCMAS环境下对火车控制系统和虚拟旅行系统进行形式化建模和验证，证明本文所提算法的正确性及有效性。本文主要研究以下几个方面： (1)本文分析并研究了KQML行为原语的关键字及语义，同时考虑符号模型检测工具MCMAS的输入语言ISPL的特点，提出了便于KQML语言转化为MCMAS输入语言ISPL的的中间转化模型——状态迁移七元组，为实现多Agent系统的自动化验证打下基础。 (2)将KQML行为原语与能够反映系统状态迁移关系的迁移七元组一一映射，提出其转化算法K2T，从而实现KQML向形式化模型的自动转化。 (3)提出了迁移七元组自动生成MCMAS输入语言ISPL的转化算法T2I。该算法根据中间形式化模型状态迁移七元组的本身特性及解释系统建模语言ISPL的特性，实现了迁移七元组到ISPL的自动转化，减少了转化过程中的人工操作。 (4)运用符号模型检测工具MCMAS对火车控制系统及虚拟旅行系统的时态认知及合作等规范进行验证，显示了所提算法的正确性及有效性。