April 28 – May 3 , 2013, Dagstuhl Seminar 13181

VaToMAS - Verification and Testing of Multi-Agent Systems


Alessio R. Lomuscio (Imperial College London, GB)
Sophie Pinchinat (IRISA / CNRS, FR)
Holger Schlingloff (HU Berlin, DE)

1 / 2 >

For support, please contact

Dagstuhl Service Team


Dagstuhl Report, Volume 3, Issue 4 Dagstuhl Report
Aims & Scope
List of Participants
Shared Documents
Dagstuhl Seminar Schedule [pdf]


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
  Creative Commons BY 3.0 Unported license
  Alessio R. Lomuscio and Sophie Pinchinat and Holger Schlingloff


  • Artificial Intelligence / Robotics
  • Semantics / Formal Methods
  • Verification / Logic


  • Model checking
  • Specification-based testing
  • Multi-agent systems
  • Controller synthesis
  • Temporal logic

Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, ground floor, during the seminar week.


In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.