Wojciech Jamroga, Computational Intelligence Group, Clausthal University of Technology

Michael Wooldridge, Department of Computer Science, University of Liverpool

**Abstract:**

Rational strategic reasoning is the process whereby an agent reasons
about the best strategy to adopt in a given multi-agent scenario,
taking into account the likely behaviour of other rational
participants in the scenario, and in particular, how the agent's
choice of strategy will rationally affect the choices of others. We
present CATL, a logic that is intended to facilitate such
reasoning. CATL is an extension of ATL, the
Alternating-time Temporal Logic of Alur, Henzinger, and Kupferman,
which supports reasoning about the abilities of agents and coalitions
of agents in game-like multi-agent systems. CATL extends
ATL with a ternary *counterfactual commitment* operator of
the form *Ci(sigma,phi)*, with the intended reading "if it were
the case that agent *i* commited to strategy *sigma*, then
*phi* holds". By using this operator in combination with the ability
operators of ATL, it is possible to reason about the
implications of different possible choices by agents. We illustrate
the approach by showing how CATL may be used to characterise
properties of games such as Nash equilibrium and Pareto efficiency. We
also investigate the axiomatics of the logic, and show that the model checking problem for
CATL is tractable, and hence that efficient implementations of
strategic reasoners based on CATL are feasible.

**Keywords:** alternating-time logic, multi-agent systems, commitment, counterfactual reasoning, model update.

Computational Intelligence Group @ Technical University of Clausthal | |

Human Media Interaction Group @ University of Twente | |

Computer Science Group @ University of Gdansk | Last modified 2005-03-23 |