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

Rustam Galimullin; Maksim Gladyshev; Munyque Mittelmann; Nima Motamed

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

Rustam Galimullin
, Maksim Gladyshev
, Munyque Mittelmann
, Nima Motamed

Sub Intelligent Systems

University of Bergen
University of Naples Federico II

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

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 (ATL) that enables reasoning about the dynamics of model change, called the Logic for ATL Model Building (LAMB). We show how 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 ATL, LAMB enjoys a P-complete model-checking procedure.

Original language	English
Title of host publication	Proceedings of the 24th International Conference on Autonomous Agents and Multiagent Systems
Subtitle of host publication	AAMAS 2025
Editors	Yevgeniy Vorobeychik, Sanmay Das, Ann Nowe
Publisher	International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS)
Pages	829-838
Number of pages	10
ISBN (Electronic)	9798400714269
Publication status	Published - 5 Jun 2025
Event	24th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2025 - Detroit, United States Duration: 19 May 2025 → 23 May 2025

Publication series

Name	Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS
ISSN (Print)	1548-8403
ISSN (Electronic)	1558-2914

Conference

Conference	24th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2025
Country/Territory	United States
City	Detroit
Period	19/05/25 → 23/05/25

Bibliographical note

Publisher Copyright:
© 2025 International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org).

Keywords

Formal Verification
Model Change
Strategy Logics

Access to Document

Changing the Rules of the Game: Reasoning about Dynamic Phenomena in Multi-Agent SystemsFinal published version, 1.09 MBLicence: CC BY

https://dl.acm.org/doi/10.5555/3709347.3743601

Cite this

Galimullin, R., Gladyshev, M., Mittelmann, M., & Motamed, N. (2025). Changing the Rules of the Game: Reasoning about Dynamic Phenomena in Multi-Agent Systems AAAI Track. In Y. Vorobeychik, S. Das, & A. Nowe (Eds.), Proceedings of the 24th International Conference on Autonomous Agents and Multiagent Systems: AAMAS 2025 (pp. 829-838). (Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS). International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS). https://dl.acm.org/doi/10.5555/3709347.3743601

Galimullin, Rustam ; Gladyshev, Maksim ; Mittelmann, Munyque et al. / Changing the Rules of the Game : Reasoning about Dynamic Phenomena in Multi-Agent Systems AAAI Track. Proceedings of the 24th International Conference on Autonomous Agents and Multiagent Systems: AAMAS 2025. editor / Yevgeniy Vorobeychik ; Sanmay Das ; Ann Nowe. International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS), 2025. pp. 829-838 (Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS).

@inproceedings{416468afda4a486c872283d9e2cbf331,

title = "Changing the Rules of the Game: Reasoning about Dynamic Phenomena in Multi-Agent Systems AAAI Track",

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 (ATL) that enables reasoning about the dynamics of model change, called the Logic for ATL Model Building (LAMB). We show how 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 ATL, LAMB enjoys a P-complete model-checking procedure.",

keywords = "Formal Verification, Model Change, Strategy Logics",

author = "Rustam Galimullin and Maksim Gladyshev and Munyque Mittelmann and Nima Motamed",

note = "Publisher Copyright: {\textcopyright} 2025 International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org).; 24th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2025 ; Conference date: 19-05-2025 Through 23-05-2025",

year = "2025",

month = jun,

day = "5",

language = "English",

series = "Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS",

publisher = "International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS)",

pages = "829--838",

editor = "Yevgeniy Vorobeychik and Sanmay Das and Ann Nowe",

booktitle = "Proceedings of the 24th International Conference on Autonomous Agents and Multiagent Systems",

}

Galimullin, R, Gladyshev, M, Mittelmann, M & Motamed, N 2025, Changing the Rules of the Game: Reasoning about Dynamic Phenomena in Multi-Agent Systems AAAI Track. in Y Vorobeychik, S Das & A Nowe (eds), Proceedings of the 24th International Conference on Autonomous Agents and Multiagent Systems: AAMAS 2025. Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS, International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS), pp. 829-838, 24th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2025, Detroit, United States, 19/05/25. <https://dl.acm.org/doi/10.5555/3709347.3743601>

Changing the Rules of the Game: Reasoning about Dynamic Phenomena in Multi-Agent Systems AAAI Track. / Galimullin, Rustam; Gladyshev, Maksim; Mittelmann, Munyque et al.
Proceedings of the 24th International Conference on Autonomous Agents and Multiagent Systems: AAMAS 2025. ed. / Yevgeniy Vorobeychik; Sanmay Das; Ann Nowe. International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS), 2025. p. 829-838 (Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Changing the Rules of the Game

T2 - 24th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2025

AU - Galimullin, Rustam

AU - Gladyshev, Maksim

AU - Mittelmann, Munyque

AU - Motamed, Nima

PY - 2025/6/5

Y1 - 2025/6/5

N2 - 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 (ATL) that enables reasoning about the dynamics of model change, called the Logic for ATL Model Building (LAMB). We show how 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 ATL, LAMB enjoys a P-complete model-checking procedure.

AB - 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 (ATL) that enables reasoning about the dynamics of model change, called the Logic for ATL Model Building (LAMB). We show how 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 ATL, LAMB enjoys a P-complete model-checking procedure.

KW - Formal Verification

KW - Model Change

KW - Strategy Logics

UR - https://www.scopus.com/pages/publications/105009818692

M3 - Conference contribution

AN - SCOPUS:105009818692

T3 - Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS

SP - 829

EP - 838

BT - Proceedings of the 24th International Conference on Autonomous Agents and Multiagent Systems

A2 - Vorobeychik, Yevgeniy

A2 - Das, Sanmay

A2 - Nowe, Ann

PB - International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS)

Y2 - 19 May 2025 through 23 May 2025

ER -

Galimullin R, Gladyshev M, Mittelmann M, Motamed N. Changing the Rules of the Game: Reasoning about Dynamic Phenomena in Multi-Agent Systems AAAI Track. In Vorobeychik Y, Das S, Nowe A, editors, Proceedings of the 24th International Conference on Autonomous Agents and Multiagent Systems: AAMAS 2025. International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS). 2025. p. 829-838. (Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS).

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

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this