 For a start, if one is interested in the properties a player can bring about through moves, a good choice of language is based on modalities \(\langle \move_i\rangle \varphi\), expressing that at least one of i’s available moves leads to a next stage satisfying \(\varphi\). The following illustrates how this language works in a given extensive form game.