An Argumentative Approach for Modelling Coalitions Using ATL

During the last decade argumentation has evolved as a successful approach to formalize commonsense reasoning and decision making in multiagent systems. In particular, recent research has shown that argumentation can be used to provide a framework for reasoning about

coalition formation

, formalizing the adoption of coalitions by the agents in association with different argumentation semantics. At the same time

Alternating-time Temporal Logic

(

atl

for short) has been successfully used to reason about the behavior and abilities of coalitions of agents. However, an important limitation of

atl

operators is that they account only for the

existence of successful strategies

of coalitions, not considering whether coalitions can be actually formed.

This paper is an attempt to combine both frameworks in order to develop a logical system through which we can reason at the same time (1) about abilities of coalitions of agents and (2) about the formation of coalitions. In order to achieve this, we provide a formal extension of

atl

, called

Coalitional

atl

(

coalATL

for short), in which the actual computation of the coalition is modelled in terms of argumentation semantics. Moreover, we integrate goals as agents’ incentive to join coalitions. We show that

coalATL

’s proof theory can be understood as a natural extension of the model checking procedure used in

atl

.