Changing the Rules of the Game: Reasoning about Dynamic Phenomena in Multi-Agent Systems
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909597432807424 |
|---|---|
| author | Galimullin, Rustam Gladyshev, Maksim Mittelmann, Munyque Motamed, Nima |
| author_facet | Galimullin, Rustam Gladyshev, Maksim Mittelmann, Munyque Motamed, Nima |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_11785 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Changing the Rules of the Game: Reasoning about Dynamic Phenomena in Multi-Agent Systems Galimullin, Rustam Gladyshev, Maksim Mittelmann, Munyque Motamed, Nima Logic in Computer Science Multiagent Systems F.4.1; I.2.4; I.2.11 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. |
| title | Changing the Rules of the Game: Reasoning about Dynamic Phenomena in Multi-Agent Systems |
| topic | Logic in Computer Science Multiagent Systems F.4.1; I.2.4; I.2.11 |
| url | https://arxiv.org/abs/2502.11785 |