有限资源智能体联盟能力的逻辑规范及模型检测研究

Having been extensively applied to various security-critical systems, a crucial challenge for designing Multiple Agent Systems (MAS) is to guarantee and show the consistency between agents’ behaviors and the objective requirements. It is known that model-checking is a feasible technique for verifying the correctness of a system. However, most of the classical study on model checking multi-agent systems focuses on ideal cases where optimal response can always be ensured. Concerning the fact that agents’ behaviors are always influenced by the restriction of resources which may lead to their failure to compute optimal strategies, this project proposes to study the logical modelling and model-checking of agents’ coalitional ability in MAS with bounded resources. This research explores resource-sharing and behavior-coordination for groups of agents, as well as the update of their strategies with the change of resources. By extending classical temporal logics, logical specification for properties related to resources can be established. Symbolic model checking algorithm based on OBDDs will finally be developed, in the hope of providing a way for the automatic verification of MAS under bounded resources and thus avoiding potential accidents due to design efficiency, of offering theoretical guidance on specifying the resource requirements during system design, and of pushing forward the development of model checking technique and the research of AI.

多智能体技术广泛应用于各种安全攸关系统，其设计中的一个关键挑战是保障智能体行为与预期目标一致。模型检测是一种切实可行的自动验证技术，但传统的多智能体模型检测研究大都关注于能够保证最优响应的理想智能系统。针对实际系统中主体行为往往受制于资源（如时间、内存等）的有限性而可能无法计算最优策略的事实，本项目拟研究有限资源多智能体系统中联盟能力的逻辑建模及模型检测方法。重点研究资源有限的情况下，智能体间的资源共享和协同规划，以及可用资源动态变化时智能体的策略调整。通过扩展和丰富经典时序逻辑，建立面向资源相关属性的逻辑描述，并提出基于OBDDs的符号模型检测算法。以期实现有限资源场景中多智能体系统正确性的自动验证，为系统设计中明确资源需求提供理论指导，避免设计缺陷带来的安全隐患和灾难，并推动模型检测技术和人工智能学科的发展。

多智能体理论为全面研究和准确刻画分布计算系统提供了合理的概念模型，为复杂问题求解提供了行之有效的思路。随着智能体技术在安全攸关系统中的广泛使用，验证和保障系统行为与目标一致成为亟待解决的问题。明确资源需求并对资源进行合理配置是智能体系统设计的重要环节，是使智能体可以有效行动的必要条件。因此，研究资源相关性质的模型检测问题对于保障多智能体系统的正确性具有非常关键的实际意义。..围绕有限资源多智能体系统资源的可靠性问题，项目主要从理论模型、优化算法两个方面着手开展研究。在理论模型方面的主要进展包括：（1）提出基于人工神经网络的多主体博弈主体的交互认知模型，特别是对于对手策略的刻画及相应的博弈算法。（2）基于时序逻辑对多主体系统的资源需求和联盟能力进行形式化刻画。通过扩展传统的时序逻辑ATL，提出了一种可以表示资源需求和动作约束的新的逻辑系统。特别地，通过引入一个新的逻辑算子，可表示主体遵循的动作协议。因此，该逻辑系统可以描述主体在特定动作协议的约束下和特定资源条件下的联盟能力。此外，研究了该逻辑的模型检测复杂度和算法，并将其应用于多主体面临动作和资源约束条件下的规划问题中。在优化方法方面的主要进展有：（1）提出了一种基于备份策略的对抗式搜索算法，该算法可以很好地消除状态节点的评估函数的不准确性，提高智能体决策的准确率和效率。基于五子棋这种博弈形式，对所提算法进行了实现。试验结果表明该算法的可行性。（2）运用图论方法，研究多主体关系中的可控性。将多主体系统中各主体间的关系建模成互连网络，通过研究网络的可靠性来实现对多主体系统可靠性的研究。..项目研究成果可为多智能体系统设计提供理论指导，消除系统安全隐患从而避免重大灾难和损失，一定程度上推动人工智能学科的发展。