 So \(\Box_i A\) \((\Diamond_i A)\) is true in s provided that sentence \(A\) holds true in every (some) state that \(i\) can chose from state \(s\). Given that \(\bot\) is a contradiction (so \({\sim}\bot\) is a tautology), \(\Diamond_i {\sim}\bot\) is true at a state when it is \(i\)’s turn to move. For a two-player game \(\Box_1\bot\) &amp; \(\Box_2\bot\) is true of a state that ends the game, because neither 1 nor 2 can move. \(\Box_1\Diamond_2\)win\(_2\) asserts that player 1 has a loss because whatever 1 does from the present state, 2 can win in the following move. 