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