VaToMAS - Verification and Testing of Multi-Agent Systems

Summary

Multi-agent systems (MAS) are distributed computing systems in which the individual components, or agents, interact with each other by means of communication, negotiation, cooperation etc., in order to meet private and common goals. The agent model finds applications in a variety of key applications of high-impact to society including web-services, autonomous vehicles, and e-government. But if MAS are to deliver on their promise to drive future applications, they need to be reliable.

MAS are typically specified and reasoned about by a variety of modal formalisms, including a variety of different logics. There are presently several, compartmented communities tackling questions pertaining to the correctness of MAS: researchers in model checking, model based testing, and controller synthesis. There presently is very little personal interaction among the scientists from different communities. The aim of this seminar was to bring these communities together, get exposure to each others' solutions to similar aims, and ultimately enhance their future interaction.

The topics concentrated on the intersection of the fields:

• Model checking of temporal-epistemic logic, alternating logics, and BDI logics,
• Model based test generation for embedded systems,
• Controller synthesis for self-organizing systems.

In model checking, usually a model of the system and a property to be verified are given. In model based test generation, the goal is to construct a test suite from a model which establishes confidence in a certain property. In synthesis, a property and a model of computation are given, from which a strategy (a system model) is to be built. Both the test generation and the controller synthesis problem are closely related to model checking – in order to check the satisfiability of certain alternating time temporal logic (ATL) formulas in a model, one needs to construct a strategy for the participating agents.

The purpose of the seminar was to establish a common understanding of the problems in the different technologies of these application areas. It was expected that increased interaction between these three fields would stimulate new results and techniques of both theoretical relevance and practical usefulness.

Besides survey talks (60 minutes) on common technologies, attendees gave short contributions (30 minutes) and lightening presentations (15 minutes) on current research results and discussion rounds on open problems and research agendas. Additional technical sessions, including software demos, were organised spontaneously by the attendees for two of the evenings.

Attendees also contributed to the seminar by taking part in the lively discussions organised on topics of importance in the area. These were held in some of the afternoons but also at during informal occasions outside the usual seminar hours such as after dinner. This helped bridge some of the gaps between the subdisciplines and rectify some misconception about each other's work.

The goals of the seminar were

• to obtain a common understanding of base technologies and intersections between these topics
• to collect a state-of-the-art picture of recent research results in the fields
• to confront methods from model checking and test generation for MAS
• to clarify terminology, research agendas and open problems
• to define a set of benchmark problems for verification and testing of MAS
• to bring together different communities formerly not interacting.

The research topics were also discussed in relation with embedded systems applications such as:

• Verification of cyber-physical systems
• Validation of autonomous robots