中文摘要：

社会法则是一种对多Agent系统进行协同的有效机制。社会法则通过其协同目标描述多Agent系统的目标属性，然后通过其规范系统修正多Agent系统的内部运行结构从而使协同目标得到满足。然而现有的社会法则采用的规范系统过于简陋，这导致其修正能力有限。注意到规范系统并不是社会法则的特有内容，而是一个人工智能领域的一个拥有较长历史的研究方向，本项目试图通过使社会法则更多地吸收规范系统的研究成果，改善其修正能力。对于新的规范系统约束下的多Agent系统，本项目将提出对应的逻辑系统来对其进行描述与验证；对于社会法则的自动合成问题，本项目将重点研究其相关判定问题的计算复杂度，并提出有效的合成算法。此外，本项目还将在网络攻防模拟平台上展开相关的应用研究，试图将我们提出的模型推向实际应用。

结论摘要：

多Agent系统是一种对开放系统及其环境的抽象。社会法则是一种对多Agent系统进行协同的有效机制。本项目把多Agent社会法则自动合成问题建模成一个模型修正问题，然后对其理论框架进行系统地研究。目的是充分分析与总结其与相关研究的联系与区别、形式化其涉及到的基本概念、证明一些具有一般性的结论，为开发适用于开放系统的自动验证技术和工具提供完备的理论基础。本项目的主要成果是把模型修正的研究由封闭系统推进到开放系统，这主要涉及到如下两个基本的问题一是，如何对开放系统进行描述和验证；二是，如何修正开放系统模型。主要取得了如下进展 1) 提出了一种自动修正的理论框架。将自动修正建模为一个包含描述、验证、模型修正与系统修正这四个环节的过程。充分分析了其与模型检测、理论变更与社会法则的内在联系。特别是首先指出社会法则合成问题研究实质上就是一个面向开放系统的模型修正问题的特例，这意味着我们在今后的研究中可以对这两个研究方向进行充分整合，互相借鉴其研究方法和成果。 2) 提出了一类用于描述与验证开放系统的逻辑ATLαβ。我们提出协同博弈结构用于建模开放系统，进而我们提出以协同博弈结构为语义结构，同时能对α-能力和β-能力的时态属性进行描述与验证的协同交互时态逻辑ATLαβ，并分析了其与ATL与CTL之间的关系。重点研究了ATLαβ的模型检测问题，证明了该问题和ATL模型检测问题一样是一个P-完全问题，并设计了一种多项式时间复杂度的模型检测算法。 3) 研究了ATL模型修正问题。为ATL模型修正定义了一套完备的基本修正操作，并且设计了一种目标属性的表示方法。在此基础上形式化了基本ATL模型修正问题以及相关的两个判定问题，并确定了这些问题的计算复杂度。在此基础上研究了ATLαβ模型修正问题。基于ATLαβ与ATL的联系与区别，将ATL模型修正的研究成果继续推进至ATLαβ模型修正问题, 定义了其基本理论框架，研究了相关问题的计算复杂性，并进行了充分的算法实验。 4) 总结了本项目的研究，并展望了后续的研究工作。初步研究了具有博弈论意义下的理性的Agent对社会法则的服从问题，尝试设计合适机制使Agent均服从社会法则成为其均衡策略；初步研究了社会网络的一系列分析与挖掘问题，及其与社会法则研究的联系。