Abstract
Agent, composition is the problem of realizing a "virtual" agent by suitably directing a set of available "concrete", i.e., already implemented, agents. It is a synthesis problem, since its solution amounts to synthesizing a controller that suitably directs the available agents. Agent composition has its roots in certain forms of service composition advocated for SOA, and it has been recently actively studied by AI and Agents community. In this paper, we show that agent composition can be solved by ATL (Alternating-time Temporal Logic) model checking. This results is of interest for at least two contrasting reasons. First, from the point of view of agent composition, it gives access to some of the most modern model checking techniques and state of the art tools, such as MCMAS, that have been recently developed by the Agent community. Second, from the point of view of ATL verification tools, it gives a novel concrete problem to look at, which puts emphasis on actually synthesize winning policies (the controller) instead of just checking that they exist.