中文摘要：

多Agent系统是一种分布智能软件系统, 如何保证其正确性是困难而又迫切需要解决的问题. 模型检测是软硬件系统正确性验证的一种主流方法. 目前国际上将模型检测应用于多Agent系统以保证系统正确性的工作开始成为一个热点, 但已有工作是初步的, 用于模型检测的逻辑对智能性质和通讯性质的描述并不充分; 已有工作也未提出有特色的多Agent系统的模型检测算法, 主要应用已有的方法和工具. 本项目研究面向多Agent系统模型检测的逻辑和算法, 包括提出刻画多Agent系统时序性质, 智能特征和通讯行为的模态逻辑系统, 给出其推理系统和语义模型, 并研究可靠性完备性等性质. 同时针对所提出的逻辑系统, 借鉴符号化方法自动机方法等, 给出高效的模型检测算法, 研究其时空复杂性. 并实现相应原型系统, 通过实例验证所提的方法. 本项目将丰富多Agent系统和模型检测的研究, 也有很好的应用前景.

结论摘要：

本项目研究了面向多Agent系统模型检测的逻辑和算法。多Agent系统是一种复杂的智能软件系统，近年来在计算机的许多领域中被应用。如何保证多 Agent系统的正确性，是一个重要的课题。对于一般软件而言，模型检测方法是一种自动且高效的形式化方法，但对于多Agent系统而言，模型检测技术不能直接应用，因为多Agent系统除了有时序性质外，还有智能性质，如认知、合作等。本项目将一般的模型检测技术扩充到多Agent系统。为此本项目在时序逻辑中扩充了认知算子、概率认知算子、合作算子等。从而得到面向多Agent系统模型检测的若干逻辑系统，这类逻辑系统可作为描述多 Agent系统的理论工具。进一步本项目研究了这类逻辑系统的一些性质，如证明了可靠性、完备性等。在此基础上，本项目给出了面向多Agent系统模型检测的算法，并将已有的一些方法，如符号化方法等，应用于多 Agent系统模型检测中。本项目还进一步给出了模型检测算法的正确性和复杂性，实现了算法。最后，本项目将所给出的逻辑和算法应用于一些具体实例中，如用于验证一些具有多个主体的协议系统的正确性。