On the Expressiveness and Complexity of ATL

TL;DR

This paper analyzes the computational complexity and expressiveness of ATL, a logic for multi-agent systems, establishing complexity bounds and showing the need for explicit modalities like 'Release' for full expressiveness.

Contribution

It precisely characterizes the complexity of ATL model-checking over ATS and CGS with varying agent counts and explores expressiveness limitations, including translations and modality extensions.

Findings

Model-checking complexity is ^P_2- and ^P_3-complete for ATS and CGS.

Translations between ATS and CGS preserve alternating bisimulation.

Standard ATL cannot express dual modalities without explicit 'Release' modality.

Abstract

ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. In this paper, we first precisely characterize the complexity of ATL model-checking over Alternating Transition Systems and Concurrent Game Structures when the number of agents is not fixed. We prove that it is \Delta^P_2 - and \Delta^P_?_3-complete, depending on the underlying multi-agent model (ATS and CGS resp.). We also consider the same problems for some extensions of ATL. We then consider expressiveness issues. We show how ATS and CGS are related and provide translations between these models w.r.t. alternating bisimulation. We also prove that the standard definition of ATL (built on modalities "Next", "Always" and "Until") cannot express the duals of its modalities: it is necessary to explicitely add the modality "Release".