Key points are not available for this paper at this time.
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 participants in the scenario, and, in particular, how the agent's choice of strategy will affect the choices of others. We present CATL, a logic that is intended to facilitate such reasoning. CATL is an extension of Alternating-time Temporal Logic (ATL), which supports reasoning about the abilities of agents and their coalitions in game-like multi-agent systems. CATL extends ATL with a ternary counterfactual commitment operator of the form Ci(σ, ϕ), with the intended reading "if it were the case that agent i committed to strategy σ, then ϕ". 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 express properties of games such as Nash equilibrium and Pareto efficiency. We also show that the model checking problem for CATL is tractable, and hence that efficient implementations of strategic reasoners based on CATL are feasible.
Hoek et al. (Mon,) studied this question.