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

Summary

This partial ingest is based on the extracted full PDF text. Galimullin et al. introduce LAMB, the Logic for ATL Model Building, which extends Hybrid ATL with explicit update operators for changing concurrent game models. LAMB can update proposition valuations at named states, redirect action-profile transitions, and add new named states. The paper uses these operators to reason about normative updates, bounded modification synthesis, and mechanism-design-style changes while retaining P-complete model checking.

Key Claims

• Many multi-agent systems need reasoning not only about strategic abilities in a fixed model, but about how strategic abilities change when the model is modified.
• Hybrid ATL adds nominals and @ operators so formulas can refer to named states.
• LAMB adds modular model-update operators and is strictly more expressive than ATL/HATL fragments that lack arrow updates.
• LAMB can express sanctioning norms, bounded repair/modification synthesis, and mechanism-design properties such as individual rationality and Pareto optimality.
• Full LAMB model checking is P-complete, matching ATL’s model-checking complexity despite higher expressivity.

Methods / Formalism

• A named concurrent game model is

$$M=⟨S,\tau ,L⟩,$$

where S is finite, tau:S x Act^Agt -> S is the transition function, and L names states with nominals.

• HATL adds formulas @_alpha phi, meaning phi holds at the state named alpha.
• LAMB adds update modalities [pi]phi, including proposition substitution at a named state, redirection of an action-profile arrow from one named state to another, and creation of a fresh named state.
• Bounded modification synthesis asks whether there exists an update sequence of size at most n such that M_s |= [pi]phi.
• ATL Model Building records the LAMB operators, expressivity facts, and model-checking/synthesis complexity.

Evidence / Experiments

• The paper is formal and example-driven.
• Examples show updates for sanctioning norms, model repair, and social-choice mechanisms.
• Main results: HATL is strictly more expressive than ATL; SLAMB is no more expressive than HATL but can be more succinct; arrow updates make ALAMB strictly more expressive; LAMB model checking is P-complete; bounded synthesis is NP-complete.

Connections

• Extends Alternating-Time Temporal Logic with named-state reasoning and explicit model changes.
• Connects to Dynamic Epistemic Logic because the update modality is DEL-inspired, but applied to concurrent game models rather than epistemic models.
• Supports Strategic Reasoning about agents whose institutional rules, norms, or mechanisms can be revised.
• Complements Varricchione2023 - Synthesising Reward Machines for Cooperative MARL, which also uses ATL-style strategic specifications but compiles them into reward machines.

Open Questions

• Satisfiability and constructive synthesis algorithms are left as future work.
• The paper assumes memoryless strategies and fixed agent/action sets.
• Future variants may add costs to updates, grant/revoke actions, change the number of agents, or use more expressive base logics such as ATL* or Strategy Logic.

Citation

Galimullin, R., Gladyshev, M., Mittelmann, M., and Motamed, N. (2025). Changing the Rules of the Game: Reasoning about Dynamic Phenomena in Multi-Agent Systems. AAMAS 2025 extended version, arXiv:2502.11785v2.