10. – 14. August 2014, Dagstuhl-Seminar 14332

Formal Methods for Coordinating Multi-Agent Systems


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

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Report, Volume 4, Issue 8 Dagstuhl Report
Programm des Dagstuhl-Seminars [pdf]


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.

Summary text license
  Creative Commons BY 3.0 Unported license
  Thomas Agotnes and Nils Bulling


  • Semantics / Formal Methods
  • Verification / Logic


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


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.