I Would If I Could: Reasoning about Dynamics of Actions in Multi-Agent Systems
For researchers in multi-agent systems and formal verification, this work addresses the underexplored dynamic treatment of actions and knowledge, offering a new logical framework with theoretical foundations.
The paper introduces ATL-D and ATEL-D, logics that model dynamic changes in agents' available actions and knowledge in multi-agent systems, and provides expressivity, normative system relations, and complexity results.
Autonomous agents acting in realistic Multi-Agent Systems (MAS) should be able to adapt during their execution. Standard strategic logics, such as Alternating-time Temporal Logic (ATL), model agents' state- or history-dependent behaviour. However, the dynamic treatment of agents' available actions and their knowledge of required actions is still rarely addressed. In this paper, we introduce ATL with Dynamic Actions (ATL-D), which models the process of granting and revoking actions, and its extension ATEL-D, which captures how such updates affect agents' knowledge. Beyond the conceptual contribution, we provide several technical results: we analyse the expressivity of our logic in relation to ATL, study its relation to normative systems, and provide complexity results for relevant computational problems.