Munyque Mittelmann
University of Naples Federico II
Tuesday May 13th, 2025, 10:00
Amphitheatre F107, Montbonnot
entrée libre
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 talk, 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.
Relevant paper https://arxiv.org/pdf/2502.11785 (accepted at AAMAS 2025)