University Of Pretoria SA Coronavirus Website Computer Science Department

International Collaboration on Verification of Multi-Agent Systems

Posted by annar on Fri 10 Jul 2020, 09:33:51 Fri 10 Jul 2020, 09:33:51

Multi-agent systems (MAS) are computerized systems that consist of intelligent and autonomous agents. These agents collaborate in order to achieve goals or to solve problems. Multi-agent systems play an important role in the context of the Industry 4.0. Areas of application are the coordination and optimization of energy management, transportation and manufacturing. MAS technology has a great potential to enhance processes in these areas.

However, agent-based solutions require the assurance of the correctness of the underlying system. Design errors may have negative effects such as a failure of energy supply, a loss of productivity, or may be even harmful to human lives. Dr Nils Timm is the local principal investigator of a bilateral research project on the verification of multi-agent systems. In collaboration with scientists from the Stockholm University Sweden, he is developing techniques for automatically proving the correctness of multi-agent systems in terms of goal achievability. These techniques allow to ensure the quality and reliability of multi-agent systems, and thus, contribute to the maturation of MAS technology for industry purposes.

A common concept in most multi-agent systems is the competition of the agents for shared resources such as hardware devices or energy. Dr Timm and his team developed a modelling framework for resource allocation in multi-agent systems. The framework allows to represent many real-world scenarios of agents pursuing goals with regard to resources. Goal specifications can be automatically verified for MAS models within the framework. The outcome is either a proof that the system is capable of achieving the goal, or a counterexample that refutes goal achievability. The modelling framework has been presented in an article published in Multi-Agent Systems in 2019.

In January 2020 Dr Timm co-organised an international workshop on the Verification and Strategy Synthesis in Multi-Agent Systems. The aim of this workshop was to bring together leading researchers in the field to discuss the major challenges of MAS verification. One of the biggest challenges is to cope with the state space complexity of multi-agent systems. Real-world systems are mostly too large to be directly manageable by a verification tool. In his current research, Dr Timm is developing symbolic encodings of multi-agent systems that allow for a more compact representation, and therefore, for more efficient verification. Another challenge is the fact that in practice agents only have partial knowledge about each other and the environment they are acting in, which may affect whether the pursued goals can be achieved or not. Therefore, a second focus of the ongoing research project is to extend the modelling framework in order to enable verification under partial knowledge assumptions. The workshop brought Dr Timm's team together with scientists from the Université Paris-Est Créteil France, who will participate in the latter part of the project.


Published Conference Paper (LNCS):
Generalising the Dining Philosophers Problem: Competitive Dynamic Resource Allocation in Multi-agent Systems

Co-Organised Workshop:

International Mini-Workshop Verification and Strategy Synthesis in Multi-Agent Systems

All content copyright © Department of Computer Science, School of IT, University of Pretoria, South Africa