|Dynamical multi-agent systems: modelling, algorithmic verification and synthesis|
Back to my home page
(Research project funded by the Swedish Research council (Vetenskapsrådet) during 2016-2019)
Short description of the project:
Multi-agent system is a generic concept covering a wide variety of phenomena in the technological society, such as interacting computer systems and open networks, robotic systems, social structures and networks, financial institutions, markets, etc. A multi-agent system (MAS) consists of several 'agents' (software, computers, robots, market investors, institution employees, etc.) that act autonomously and intelligently in a common environment, in pursuit of individual or collective goals, interacting with the environment and with each other by communication, planning and executing actions and strategies. Most multi-agent systems have a modular and dynamical nature: agents are represented by relatively autonomous modules and can enter or leave the system and can change their internal states, roles, abilities to act and interact, goals, etc. within the system. This dynamicity makes it quite challenging to properly design, formally specify and verify the behaviour of such systems. The main aim of the project will be to undertake that challenge and endeavour to resolve it. The main research tasks in the project include: development of a generic framework for modeling of modular and dynamical multi-agent systems, design of suitable formal logical languages for their specification and of practically implementable logic-based algorithmic methods solving the general problem of `dynamical verification'. A generic description of the `dynamical verification': given a partly described model M plus a formal specification S for its behaviour, the task is to update M by modifying its components (domain, agents, actions, transitions) so as to produce a completed model satisfying S, or to prove that such update is impossible. Dynamical verification subsumes both model checking and model synthesis as extreme cases, as well as controller synthesis. The project will aim to provide a general theory and methodology for its exploration and to provide algorithmic solutions in some more specific cases.
Last updated: December 2016