Verification of dynamic multi-agent systems: concepts, challenges and a concrete solution
Riccardo de Masellis
Date and Time
September 8th 2020, 13:15 - 14:00
The concept of Multi-Agent Systems (MASs) emerges when we consider autonomous agents interacting in a common arena. Sensor networks, robotic systems, social groups, financial markets and smart contracts are just a few practical examples of what can be considered a MAS. The field of MAS in computer science addresses the plethora of issues arising in such scenarios, from modeling paradigms, to software architectures and communication protocols.
In the talk we take the perspective of the logic and game-theoretical foundations of MAS. We start by discussing the well-known frameworks which model MASs as a set of agents which, at each step, take actions that make the system evolve in a new state. We call a sequence of such steps a play. The objective is to develop logic-based methods for verifying formal properties like: "Coalition of agents A can force all plays to reach state s regardless of what the other agents do". We will soon realize that in (almost) all established frameworks the set of agents is fixed, that is, it does not change during the plays. This assumption is arguably not realistic in many situations where agents can instead freely leave and join the system.
Dynamic MASs aim at formalizing MASs where the set of agents changes during plays. This aspect makes it quite challenging to properly design, formally specify and algorithmically verify the behaviour of these systems. We will go trough such challenges and discuss ideas and solutions to formalize dynamic MASs in their generality. Then, a specific framework for a restricted class of dynamic MAS will be presented, along with a formal language to specify properties for which model checking is decidable.