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