Abstract:
This article is about defining a suitable logic for expressing classical game theoretical notions. We define an extension of alternating-time temporal logic (ATL) that enables us to express various rationality assumptions of intelligent agents. Our proposal, the logic ATLP (ATL with plausibility) allows us to specify sets of rational strategy profiles in the object language, and reason about agents' play if only these strategy profiles were allowed. For example, we may assume the agents to play only Nash equilibria, Pareto-optimal profiles or undominated strategies, and ask about the resulting behaviour (and outcomes) under such an assumption. The logic also gives rise to generalized versions of classical solution concepts through characterizing patterns of payoffs by suitably parameterized formulae of ATLP. We investigate the complexity of model checking ATLP for several classes of formulae: It ranges from Delta3 to PSPACE in the general case and from Delta3 to Delta4 for the most interesting subclasses, and roughly corresponds to solving extensive games with imperfect information.

Keywords: game theory, modal and temporal logic, reasoning about agents, rationality.

Individual and Collective Reasoning Group @ University of Luxembourg
Computational Intelligence Group @ Clausthal University of Technology	Last modified 2010-01-08