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

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