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

TL;DR

This paper introduces LAMB, an extension of ATL, enabling reasoning about dynamic changes in multi-agent systems, with a focus on verification and synthesis of system modifications.

Contribution

It presents LAMB, a new logic that extends ATL to reason about MAS updates, and proves its model-checking problem is P-complete.

Findings

LAMB is more expressive than ATL.

Model-checking for LAMB is P-complete.

LAMB can express normative updates and mechanism design ideas.

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.