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...

• Type: Conference
• Year: 2006
• Where: ATAL
• Authors: Wiebe van der Hoek, Alessio Lomuscio, Michael Wooldridge
• Keywords: ATAL 2006, Coalition Logic, Intelligent Agents, Model Checking, Model Checking Problems