Dagstuhl Seminar 14332
Formal Methods for Coordinating Multi-Agent Systems
( Aug 10 – Aug 14, 2014 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/14332
Organizers
- Thomas Agotnes (University of Bergen, NO)
- Nils Bulling (TU Clausthal, DE)
- Sascha Ossowski (University Rey Juan Carlos, ES)
Contact
- Susanne Bach-Bernhard (for administrative matters)
Schedule
Self-interest is a key characteristic of multi-agent systems. Agents pursue their individual objectives. These objectives – which may be consistent but can just as well be completely contradicting – often require cooperation between agents, and in particular, often cannot be solely ensured by individual agents. As a consequence, actions and behaviors need to be coordinated to satisfy the agents' objectives, but they also have to be controlled to meet the global system specification. Formal methods have been successfully applied to coordinate and control multi-agent systems. Among other things, an advantage of formal methods in comparison to non-formal ones is that they allow for rigorous system specification, verification and automation.
In particular, logic-based approaches have been used for the modeling of intelligent agents and for automatic reasoning: epistemic logics allow to talk about knowledge; temporal logics to reason about the evolution of system states; and strategic logics enable reasoning about abilities of agents and coalitions. What they all have in common is their descriptive flavor. Although cognitive models of agents, as well as agent communication languages, are heavily influenced by multi-agent logics, logic-based approaches are most often used directly to describe and to reason about the system from the outside, as opposed to actively change the state of the system or to reach agreements by agents inside the system.
Interaction between rational decision makers in general, and coordination problems in particular, has also been studied in game theory for decades. There are strong ties between these two fields; in particular, strategic logics and formal methods for multi-agent systems often make use of game theoretical concepts.
Agreement technologies are tailor-made for allowing agents to arrive at agreements. For example, norms and social laws can be used to coordinate the agents' behavior – often only with little interaction of agents with their peers. A key problem is the synthesis of appropriate norms and social laws. Their acceptance affects the behavior of the agents and depends on the way norm violations are detected and sanctioned. However, there are many more aspects that influence agents' behavior, including:
- strategic power
- argumentation abilities,
- ressource limitations,
- social dependencies, and
- roles and institutions.
Due to the heterogeneity of multi-agent systems a single approach focussing on one of these issues is often not enough. This seminar aims at opening up new directions of research into the coordination and control of multi-agent systems, by bringing together researchers working in different areas.
Goals and research topics. Research topics that will be tackled at the seminar:
- agreement technologies
- formal verification and specification of multi-agent systems
- multi-agent logics
- game logics
- models of coordination and control in multi-agent systems
In particular, the seminar will focus on possible intersections between these areas. Specific goals of the seminar include the following:
- Identification of coordination and control problems in agreement technologies, game theory and multi-agent logic, and what they have in common.
- Identification of implicit assumption made in strategic logics wrt. the inter-agent coordination.
- Strengthening of the ties between logics, game theory and agreement technologies.
- Computational methods for the coordination of multi-agent systems.
- Development of benchmark coordination problems.
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.
Creative Commons BY 3.0 Unported license
Thomas Agotnes and Nils Bulling
- Thomas Agotnes (University of Bergen, NO) [dblp]
- Markus Brill (Duke University - Durham, US) [dblp]
- Jan M. Broersen (Utrecht University, NL) [dblp]
- Nils Bulling (TU Clausthal, DE) [dblp]
- Natalia Criado Pacheco (John Moores University - Liverpool, GB) [dblp]
- Mehdi Dastani (Utrecht University, NL) [dblp]
- Louise A. Dennis (University of Liverpool, GB) [dblp]
- Catalin Dima (University Paris-Est - Créteil, FR) [dblp]
- Valentin Goranko (Technical University of Denmark - Lyngby, DK) [dblp]
- Maaike Harbers (TU Delft, NL) [dblp]
- Andreas Herzig (Paul Sabatier University - Toulouse, FR) [dblp]
- Max Knobbout (Utrecht University, NL) [dblp]
- Ho-Pun Lam (NICTA - Brisbane, AU) [dblp]
- Beishui Liao (Zhejiang University, CN) [dblp]
- Brian Logan (University of Nottingham, GB) [dblp]
- Marin Lujak (University Rey Juan Carlos, ES) [dblp]
- Nir Oren (University of Aberdeen, GB) [dblp]
- Julian Padget (University of Bath, GB) [dblp]
- Truls Pedersen (University of Bergen, NO) [dblp]
- Joshua Sack (University of Amsterdam, NL) [dblp]
- Marija Slavkovik (University of Bergen, NO) [dblp]
- Bas J. G. Testerink (Utrecht University, NL) [dblp]
- Nicolas Troquard (National Research Council - Povo (Trento), IT) [dblp]
- Paolo Turrini (Imperial College London, GB) [dblp]
- Birna Van Riemsdijk (TU Delft, NL) [dblp]
- Marc Van Zee (University of Luxembourg, LU) [dblp]
- Laurent Vercouter (INSA - St- Etienne-du-Rouvray, FR) [dblp]
Classification
- semantics / formal methods
- verification / logic
Keywords
- Strategic logic
- game theory
- social laws
- normative systems
- argumentation theory
- multi-agent systems
