http://www.dagstuhl.de/14332

August 10 – 14 , 2014, Dagstuhl Seminar 14332

Formal Methods for Coordinating Multi-Agent Systems

Organizers

Thomas Agotnes (University of Bergen, NO)
Nils Bulling (TU Clausthal, DE)
Sascha Ossowski (University Rey Juan Carlos, ES)


1 / 2 >

For support, please contact

Dagstuhl Service Team

Documents

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

Summary

Formal methods form an active and broad field of research in multi-agent systems, ranging from bottom-up to top-down approaches. Properties of individual agents, e.g., aspects related to decision making and knowledge representation, are rather low-level, while the specification and verification of multi-agent systems are higher-level. In particular, logic-based approaches have been successfully used for the modeling of intelligent agents and for reasoning about them: epistemic logics allow to talk about knowledge; temporal logics to reason about the evolution of actions; and strategic logics have been proposed to reason about abilities of agents and coalitions. Alternating-time temporal logics and STIT logics are prominent members of the latter type, and more expressive logics like Strategy Logic have recently been proposed. What they all have in common is their descriptive flavor. Typically, they are not used to actively change the state of the agent system but to talk and to reason about the system. Multi-agent logics are particularly relevant for the coordination problem. The latter is concerned with global properties of a system. Since the global behaviour of a system emerges from the individual behaviour of agents, it is not obvious what the global properties are. By specifying global properties using multi-agent logics, verification techniques can be employed to verify what of these properties are met by the system; thus, to find out what the global properties are. Interaction between rational decision makers in general, and coordination problems in particular, have been studied in game theory for decades. However, game theory is not concerned with computational or logical aspects of coordination: how we can represent and reason about coordination in computers. In contrast, many agreement technologies are used in an interactive way, e.g., for arriving at agreements about joint actions or coalition structures. Techniques like norms and social laws coordinate the agent's behavior and often require less interaction of agents with their peers. Agents have to decide whether to comply with the rules or not. A difficult problem is the synthesis of appropriate norms and social laws. Related issues important for appropriate control techniques include the detection of norm violations and sanctioning mechanisms.

The seminar aimed at opening up new directions of research into the coordination problem, by bringing together researchers working in different areas of multi-agent systems as well as related fields, and in particular, to combine insights from research in the following fields:

  • formal methods and verification, and multi-agent logics in particular,
  • game theory in multi-agent systems, and
  • agreement technologies.

The seminar took place between 10 and 14 August, 2014. This medium-size, four day seminar was highly international: the 27 participants came from 12 different countries. The scientific program consisted of presentations, discussions and working groups. We scheduled presentations of three different types: overview, medium, and short. The aim of the four one hour overview talks was to give a broad introduction of the main fields relevant to the seminar - to provide a common ground. They covered Argumentation Theory, Normative Systems, Judgement Aggregation, and Computational Social Choice. Then, we scheduled ten medium (20 minutes long) and ten short (15 minutes long) presentations. We encouraged the speakers to give rather informal, non conference-style talks focussing on high-level ideas in order to provide input for the discussion groups.

From the discussions, two working groups emerged which focused on one of the following topics (cf. Sections 4.1 and 4.2):

  • Concepts: conceptual definition and classification -- what is coordination, coordination problems, and solutions?
  • Formalisation of coordination

We organized three meetings for the working groups and two joint discussion sessions for presenting and discussing the results of the working groups.

In addition to the scientific program, we enjoyed a hike which was followed a Barbecue, and the unique atmosphere of Dagstuhl.

License
  Creative Commons BY 3.0 Unported license
  Thomas Agotnes and Nils Bulling

Classification

  • Semantics / Formal Methods
  • Verification / Logic

Keywords

  • Strategic logic
  • Game theory
  • Social laws
  • Normative systems
  • Argumentation theory
  • Multi-agent systems

Book exhibition

Books from the participants of the current Seminar 

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

Documentation

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).

Publications

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.