Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Changing the Rules of the Game: Reasoning about Dynamic Phenomena in Multi-Agent Systems

Rustam Galimullin, Maksim Gladyshev, Munyque Mittelmann, Nima Motamed

TL;DR

This work introduces LAMB, a logic for ATL Model Building, to reason about dynamic updates in multi-agent systems by combining hybrid logic features (nominals) with explicit model-modification operators. LAMB extends $\mathsf{ATL}$ via $\mathsf{HATL}$ and supports three primitive updates: valuation changes, edge redirections, and state additions, enabling both verification and synthesis of modular model changes. The authors establish that LAMB strictly extends the expressivity of $\mathsf{HATL}$ and $\mathsf{ATL}$, while maintaining a $PP$-complete model-checking problem; they further analyze bounded synthesis and normative updates, showing practical applicability to mechanism design and normative MAS. The paper also situates LAMB within related work in DEL-inspired updates and rational verification, and outlines avenues for future research, including satisfiability, cost-aware updates, and enhanced expressivity with richer base logics.

Abstract

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 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 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.

Changing the Rules of the Game: Reasoning about Dynamic Phenomena in Multi-Agent Systems

TL;DR

This work introduces LAMB, a logic for ATL Model Building, to reason about dynamic updates in multi-agent systems by combining hybrid logic features (nominals) with explicit model-modification operators. LAMB extends via and supports three primitive updates: valuation changes, edge redirections, and state additions, enabling both verification and synthesis of modular model changes. The authors establish that LAMB strictly extends the expressivity of and , while maintaining a -complete model-checking problem; they further analyze bounded synthesis and normative updates, showing practical applicability to mechanism design and normative MAS. The paper also situates LAMB within related work in DEL-inspired updates and rational verification, and outlines avenues for future research, including satisfiability, cost-aware updates, and enhanced expressivity with richer base logics.

Abstract

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 updates) of MAS. We propose an extension of the Alternating-Time Temporal Logic () that enables reasoning about the dynamics of model change, called the Logic for Model Building (). We show how 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 , enjoys a P-complete model-checking procedure.

Paper Structure

This paper contains 13 sections, 5 theorems, 12 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Reasoning About Strategic Abilities in the Changing Environment
  3. Models
  4. Hybrid $\mathsf{ATL}$
  5. Logic for $\mathsf{ATL}$ Model Building
  6. Dynamic MAS through the lens of $\mathsf{LAMB}$
  7. Normative Updates on CGMs
  8. Synthesis
  9. Mechanisms for Social Choice
  10. Expressivity
  11. Model checking
  12. Related work
  13. Discussion & Conclusion

Key Result

proposition 1

The bounded synthesis problem for $\mathsf{LAMB}$ is NP NP-complete.

Figures (3)

  • Figure 1: CGMs $M$ and $N$ for two agents and two actions. Propositional variable $p$ is true in black states, and nominals $\alpha$ and $\beta$ are true in their corresponding states.
  • Figure 2: Updated CGMs $M^{\alpha \xrightarrow{aa} \alpha}$ (top left), $M^{\pi_1 }$ (bottom left), $M^{\pi_2}$ (top right), and $M^{\mathit{SN}}$ (bottom right). Proposition $p$ is true in black states, and $\mathit{fine}$ is true in square states.
  • Figure 3: Overview of the expressivity results. An arrow from $\mathsf{L}_1$ to $\mathsf{L}_2$ means $\mathsf{L}_1 \preccurlyeq\mathsf{L}_2$. If there is no symmetric arrow, then $\mathsf{L}_1 \prec \mathsf{L}_2$. This relation is transitive, and we omit transitive arrows in the figure. The dashed arrow with the question mark denotes the open question.

Theorems & Definitions (15)

  • definition 1: Named CGM
  • definition 2: Strategies
  • Remark 1
  • definition 3: Syntax of $\mathsf{HATL}$
  • definition 4: Semantics of $\mathsf{HATL}$
  • definition 5
  • definition 6: Syntax of $\mathsf{LAMB}$
  • definition 7: Semantics of $\mathsf{LAMB}$
  • definition 8
  • proposition 1
  • ...and 5 more