 There is also a kind of back-and-forth game that corresponds to our modal semantics above in the same way as Ehrenfeucht-Fraïssé games correspond to Hintikka’s game semantics for first-order logic. The players start with a state \(s\) in the structure \(A\) and a state \(t\) in the structure \(B\). Spoiler and Duplicator move alternately, as before. Each time he moves, Spoiler chooses whether to move in \(A\) or in \(B\), and then Duplicator must move in the other structure. A move is always made by going forwards along an arrow from the current state. If between them the two players have just moved to a state \(s\)´ in \(A\) and a state \(t\)´ in \(B\), and some predicate \(P_i\) holds at just one of \(s\)´ and \(t\)´, then Duplicator loses at once. Also she loses if there are no available arrows for her to move along; but if Spoiler finds there are no available arrows for him to move along in either structure, then Duplicator wins. If the two players play this game with given starting states \(s\) in \(A\) and \(t\) in \(B\), and both structures have just finitely many states, then one can show that Duplicator has a winning strategy if and only if the same modal sentences are true at \(s\) in \(A\) as are true at \(t\) in \(B\).