Dynamic Logic on Games with Structured Strategies

摘要

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 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.