Dynamic logic on games with structured strategies
R. Ramanujam, Sunil Simon · 2008
We consider a propositional 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 oppo-nent 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 ax-iomatization of the logic and prove its decidability. The tools used combine techniques from PDL, CTL and game logics. Overview Strategies are the unsung heroes of game theory. Johan van Benthem. In one sense, game theory is all about strategic reasoning. Games are defined by sets of rules that specify what moves are available to each player, and according to her own pref-erences over the possible outcomes, every player plans her strategy. If the game is rich enough, the player has access to a wide range of strategies, and the choice of what strat-egy to employ in a game situation depends not only on the player’s understanding of how the game can proceed from then on, but also based on his expectation of what strategies other players are following. While this observation holds true of much of game play-ing, we find such reasoning hardly typical of analysis in game theory. In this respect game theory largely consists of reasoning about games rather than reasoning in games. It is assumed that the entire structure of the game is laid out in front of us, and we reason from above, predicting how rational players would play, and such predictions are sum-marised into assertions on existence of equilibria. This type of study mostly suffices to focus on existence of strategies forcing certain outcomes. And yet, as Aumann and Dreze (2005) point out, this is not how game theory started. The seminal work of von Neu-Copyright c © 2008, Association for the Advancement of Artificial