改变游戏规则：多智能体系统中动态现象的推理

多智能体系统（MAS）的设计与应用需要对其底层结构修改的影响进行推理。特别是，此类更改可能会影响系统规范的满足情况及其自主组件的战略能力。在本文中，我们关注的是验证和综合 MAS 修改（或更新）的问题。我们提出了交替时序逻辑（$\mathsf{ATL}$）的一种扩展，该扩展能够对模型变化的动态性进行推理，称为 $\mathsf{ATL}$ 模型构建逻辑（$\mathsf{LAMB}$）。我们展示了 $\mathsf{LAMB}$ 如何表达关于 MAS 动态的各种直觉和思想，从规范更新到机制设计。作为主要的技术结果，我们证明了，虽然 $\mathsf{LAMB}$ 的表达能力严格强于 $\mathsf{ATL}$，但它具有 P 完全的模型检测过程。