社会法则是一种用于协同多agent系统的有效工具,是模型检测技术的延伸。一般而言,社会法则包括协同目标和规范系统这两个组件——用协同目标来描述希望多agent系统所能拥有的属性,并且用规范系统来改变多agent系统的内部结构从而实现协同目标。本文的目的是改良社会法则中的规范系统,用规范能力更强的联盟规范系统来替代原有的规范系统,以此增强社会法则对复杂协同问题的建模能力。区别于原始的规范系统,联盟规范系统不是对单个agent的行动的约束,而是对一个受控agent联盟的联合行动的约束。基于这种思想,在本文中我们先后提出了两种联盟规范系统,即(基本)联盟规范系统(Coalitional Normative System, CNS)和扩展状态空间的联盟规范系统(CNS which Extend the State Space, CNS*)。CNS*不仅能使行为约束作用于受控联盟的联合行动,而且能用一个执行上下文来记忆系统的状态转换历史。实际上这扩展了系统的状态空间,可在相同的系统状态根据不同的执行上下文设置不同的行为约束,从而获得更高的灵活性。我们仍然使用ATL语言来描述协同目标。但是我们发现在存在CNS的影响时我们必须重新对ATL公式进行解释。我们把所得的新的逻辑叫做协同交互时态逻辑(Coordinated ATL, Co-ATL).与ATL相比Co-ATL具有相同的语法,但是却具有不同的语义解释。我们证明Co-ATL模型检测问题(与ATL模型检测问题一样)仍是一个P-完全问题。为了界定CNS的规范能力的限度,我们为任意的受控联盟C找出Co-ATL语言的两个片段LC+和LC-,分别对应于“不能被确立的策略能力”和“不能被避免的策略能力”,并证明通过这两个片段可以“可靠”且“完备”地刻画CNS的规范能力。我们讨论了CNS所涉及到的三个基本计算问题,即有效性问题、可行性问题和合成问题,并证明它们分别P-完全、NP-完全、和FNP-完全的。我们定义了适用于CNS的三种最优化概念,即最小联盟规范系统、紧凑联盟规范系统以及最大效用联盟规范系统,并分别讨论了它们涉及到的计算复杂性。对于CNS*,我们证明虽然CNS*的规范能力严格比CNS要强,但是其规范能力限度同样可以用LC+和LC-来“可靠”且“完备”地刻画,并且CNS*所涉及到的三个基本计算问题的复杂度与CNS的相应问题相同。最后,我们基于模型检测定义了一种联盟规范系统合成算法,并讨论了算法的时间复杂度、正确性和完备性等形式化属性。