As a contribution to the challenge of building game-playing AI systems, we develop and analyse a formal language for representing and reasoning about strategies. Our logical language builds on the existing general Game Description Language (GDL) and extends it by a standard modality for linear time along with two dual connectives to express preferences when combining strategies. The semantics of the language is provided by a standard state-transition model. As such, problems that require reasoning about games can be solved by the standard methods for reasoning about actions and change. We also endow the language with a specific semantics by which strategy formulas are understood as move recommendations for a player. To illustrate how our formalism supports automated reasoning about strategies, we demonstrate two example methods of implementation : first, we formalise the semantic interpretation of our language in conjunction with game rules and strategy rules in the Situation Calculus; second, we show how the reasoning problem can be solved with Answer Set Programming.
In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between open entities and express that the system is correct no matter how the environment behaves. An important contribution in this context is given by the modal logics for strategic ability, in the setting of multi-agent games, such as Atl, Atl (^ * ), and the like. Recently, Chatterjee, Henzinger, and Piterman introduced Strategy Logic, which we denote here by CHP-Sl, with the aim of getting a powerful framework for reasoning explicitly about strategies. CHP-Sl is obtained by using first-order quantifications over strategies and it has been investigated in the specific setting of two-agents turned-based game structures where a non-elementary model-checking algorithm has been provided. While CHP-Sl is a very expressive logic, we claim that it does not fully capture the strategic aspects of multi-agent systems. In this work, we introduce and study a more general strategy logic, denoted Sl, for reasoning about strategies in multi-agent concurrent systems. We prove that Sl strictly includes CHP-Sl, while maintaining a decidable model-checking problem. Indeed, we show that it is 2ExpTime-complete under a reasonable semantics, thus not harder than that for Atl (^ * ) and a remarkable improvement of the same problem for CHP-Sl. We also consider the satisfiability problem and show that it is undecidable already for the sub-logic CHP-Sl under the concurrent game semantics. The author discusses games of both perfect and imperfect information at two levels of structural detail: players' local actions, and their global powers for determining outcomes of the game. Matching logical languages are proposed for both. In particular, at the "action level", imperfect information games naturally model a combined "dynamic-epistemic language"--and correspondences are found between special axioms in this language and particular modes of playing games with their information dynamics. At the "outcome level", the paper presents suitable notions of game equivalence, and some simple representation results. Copyright 2001 by Blackwell Publishing Ltd and the Board of Trustees of the Bulletin of Economic Research We consider a prepositional dynamic logic whose programs are regular expressions over game - strategy pairs. At the atomic level, these are finite extensive form game trees with structured strategy specifications, whereby a player's strategy may depend on properties of the opponent's strategy. The advantage of imposing structure not merely on games or on strategies but on game - strategy pairs, is that we can speak of a composite game g followed by g′ whereby if the opponent played a strategy s in g, the player responds with s′ in g′ to ensure a certain outcome. In the presence of iteration, a player has significant ability to strategise taking into account the explicit structure of games. We present a complete axiomatization of the logic and prove its decidability. The tools used combine techniques from PDL, CTL and game logics.