TOP
Suche auf der Schloss Dagstuhl Webseite
Sie suchen nach Informationen auf den Webseiten der einzelnen Seminare? - Dann:
Nicht fündig geworden? - Einige unserer Dienste laufen auf separaten Webseiten mit jeweils eigener Suche. Bitte beachten Sie folgende Liste:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminare
Innerhalb dieser Seite:
Externe Seiten:
  • DOOR (zum Registrieren eines Dagstuhl Aufenthaltes)
  • DOSA (zum Beantragen künftiger Dagstuhl Seminare oder Dagstuhl Perspektiven Workshops)
Publishing
Innerhalb dieser Seite:
Externe Seiten:
dblp
Innerhalb dieser Seite:
Externe Seiten:
  • die Informatik-Bibliographiedatenbank dblp


Dagstuhl-Seminar 13181

VaToMAS – Verification and Testing of Multi-Agent Systems

( 28. Apr – 03. May, 2013 )

(zum Vergrößern in der Bildmitte klicken)

Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite: https://www.dagstuhl.de/13181

Organisatoren

Kontakt


Programm

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

Teilnehmer
  • 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]

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

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