Sciweavers

ATAL
2006
Springer

On the complexity of practical ATL model checking

13 years 7 months ago
On the complexity of practical ATL model checking
We investigate the computational complexity of reasoning about multi-agent systems using the cooperation logic ATL of Alur, Henzinger, and Kupferman. It is known that satisfiability checking is EXPTIME-complete for "full" ATL, and PSPACE-complete (in the general case) for the fragment of ATL corresponding to Pauly's Coalition Logic. In contrast, the model checking problems for ATL and Coalition Logic can both be solved in time polynomial in the size of the formula and the size of model against which the formula is to be checked. However, these latter results assume an extensive representation of models, in which all states of a model are explicitly enumerated. Such representations are not feasible in practice. In this paper we investigate the complexity of the ATL and Coalition Logic model checking problems for a more "reasonable" model representation known as SRML ("Simple Reactive Modules Language"), a simplified version of the actual model represe...
Wiebe van der Hoek, Alessio Lomuscio, Michael Wool
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where ATAL
Authors Wiebe van der Hoek, Alessio Lomuscio, Michael Wooldridge
Comments (0)