TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 13181

VaToMAS – Verification and Testing of Multi-Agent Systems

( Apr 28 – May 03, 2013 )

(Click in the middle of the image to enlarge)

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/13181

Organizers

Contact


Schedule

Motivation

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 is to bring these communities together, get exposure to each others' solutions to similar aims, and ultimately enhance their future interaction.

The topics will concentrate 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 is to establish a common understanding of the problems in the different technologies of these application areas. It is expected that increased interaction between these three fields will stimulate new results and techniques of both theoretical relevance and practical usefulness.

Besides survey talks (60 minutes) on common technologies, there will be short contributions (30 minutes) on current research results and discussion rounds on open problems and research agendas. Each participant is expected to contribute to the seminar by taking part in the discussions and presenting novel results in the context of the topics of the seminar as well as by presenting the key open problems he or she is currently working on.

Goals and research topics: Research topics which are to be tackled in this seminar:

  • Logics and specification formalisms for MAS.
  • Verification and model checking for interactive systems.
  • Model-based testing for MAS.
  • Explicit, symbolic, and SAT-based algorithms for module checking.
  • Test case generation and synthesis
  • Synthesis of winning strategies for games.

The goals of the seminar are

  • 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 will be discussed also in relation with embedded systems applications such as:

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

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
Copyright Alessio R. Lomuscio, Sophie Pinchinat, and Holger Schlingloff

Participants
  • Thomas Agotnes (University of Bergen, NO) [dblp]
  • Carlos Areces (Universidad Nacional de Córdoba, AR) [dblp]
  • Guillaume Aucher (INRIA Rennes - Bretagne Atlantique, FR) [dblp]
  • Alexandru Baltag (University of Amsterdam, NL) [dblp]
  • Ezio Bartocci (TU Wien, AT) [dblp]
  • Ioana Boureanu (EPFL - Lausanne, CH) [dblp]
  • Nils Bulling (TU Clausthal, DE) [dblp]
  • Louise A. Dennis (University of Liverpool, GB) [dblp]
  • Michael Fisher (University of Liverpool, GB) [dblp]
  • Tim French (The Univ. of Western Australia - Nedlands, AU) [dblp]
  • Valentin Goranko (Technical University of Denmark - Lyngby, DK) [dblp]
  • Stefan Gruner (University of Pretoria, ZA) [dblp]
  • Dimitar Guelev (Bulgarian Academy of Sciences, BG) [dblp]
  • Yuri Gurevich (Microsoft Corporation - Redmond, US) [dblp]
  • Andreas Herzig (Paul Sabatier University - Toulouse, FR) [dblp]
  • Wojtek Jamroga (University of Luxembourg, LU) [dblp]
  • Francois Laroussinie (University Paris-Diderot, FR) [dblp]
  • Alessio R. Lomuscio (Imperial College London, GB) [dblp]
  • Nicolas Markey (ENS - Cachan, FR) [dblp]
  • Bastien Maubert (INRIA Rennes - Bretagne Atlantique, FR) [dblp]
  • Stephan Merz (LORIA - Nancy, FR) [dblp]
  • Aniello Murano (University of Napoli, IT) [dblp]
  • Wojciech Penczek (Siedlce Univ of Natural Sciences and Humanities, PL) [dblp]
  • Sylvain Peyronnet (Caen University, FR) [dblp]
  • Jerzy Pilecki (Polish Academy of Science - Warsaw, PL) [dblp]
  • Sophie Pinchinat (IRISA / CNRS, FR) [dblp]
  • Franco Raimondi (Middlesex University, GB) [dblp]
  • Jean-Francois Raskin (Free University of Brussels, BE) [dblp]
  • Markus Roggenbach (Swansea University, GB) [dblp]
  • Ina Schaefer (TU Braunschweig, DE) [dblp]
  • Holger Schlingloff (HU Berlin, DE) [dblp]
  • Gerardo Schneider (University of Göteborg, SE) [dblp]
  • Henning Schnoor (Universität Kiel, DE) [dblp]
  • Francois Schwarzentruber (IRISA - Rennes, FR) [dblp]
  • Dmitry Shkatov (University of the Witwatersrand - Johannesburg, ZA) [dblp]
  • Ron van der Meyden (UNSW - Sydney, AU) [dblp]
  • Hans Van Ditmarsch (LORIA - Nancy, FR) [dblp]
  • Ramanathan Venkatesh (Tata Consultancy Services - Pune, IN)
  • Karsten Wolf (Universität Rostock, DE) [dblp]

Classification
  • artificial intelligence / robotics
  • semantics / formal methods
  • verification / logic

Keywords
  • Model checking
  • specification-based testing
  • multi-agent systems
  • controller synthesis
  • temporal logic