The design and application of multi-agent systems (MAS) require reasoning about the effects of modifications on their underlying structure. In particular, such changes may impact the satisfaction of system specifications and the strategic abilities of their autonomous components. In this paper, we are concerned with the problem of verifying and synthesising modifications (or \textit{updates}) of MAS. We propose an extension of the Alternating-Time Temporal Logic ($\mathsf{ATL}$) that enables reasoning about the dynamics of model change, called the \textit{Logic for $\mathsf{ATL}$ Model Building} ($\mathsf{LAMB}$). We show how $\mathsf{LAMB}$ can express various intuitions and ideas about the dynamics of MAS, from normative updates to mechanism design. As the main technical result, we prove that, while being strictly more expressive than $\mathsf{ATL}$, $\mathsf{LAMB}$ enjoys a P-complete model-checking procedure.

翻译：多智能体系统（MAS）的设计与应用需要对其底层结构修改所产生的影响进行推理。具体而言，此类改变可能影响系统规约的满足程度及其自主组件的策略能力。本文关注于多智能体系统修改（或称*更新*）的验证与综合问题。我们提出了一种交替时序逻辑（$\mathsf{ATL}$）的扩展形式，使其能够对模型变化的动态性进行推理，称为*$\mathsf{ATL$模型构建逻辑*（$\mathsf{LAMB}$）。我们展示了$\mathsf{LAMB}$如何表达关于多智能体系统动态性的各种直觉与构想，从规范性更新到机制设计。作为主要技术成果，我们证明了$\mathsf{LAMB}$在表达能力严格强于$\mathsf{ATL}$的同时，具有P完全复杂度的模型检测算法。