 Structures of the following kind give rise to interesting games. The structure \(A\) consists of a set \(S\) of elements (which we shall call states, adding that they are often called worlds), a binary relation \(R\) on \(S\) (we shall read \(R\) as arrow), and a family \(P_1 ,\ldots ,P_n\) of subsets of \(S\). The two players \(\forall\) and \(\exists\) play a game G on \(A\), starting at a state \(s\) which is given them, by reading a suitable logical formula \(\phi\) as a set of instructions for playing and for winning. 