How to express the existence of winning strategy of the starter of a game in temporal logic?

Question

Consider a two-player game. A winning strategy of a player is a strategy following which the player can always beat his opponent, no matter how his opponent responds.

A game can be unfolded to a state space consisting of the possible ways of both sides of the game. How to express the existence of winning strategy of the starter of a game, say player 1, in temporal logic, defined on such a state space? The temporal logic formula can be used for model checking.

Using CTL, I get $\exists \Box (\exists \Diamond \textsf{Win}_1)$, meaning that there exists a path (from the initial state) such that from each state of this path there exists a path that eventually leads to a winning state for player 1. Is this correct?

Can it be expressed in LTL or any other variants of temporal logic?

Answer 1

I don't think it's possible in CTL nor LTL to model two competing players.

You would probably need ATL (Alternating-time Temporal Logic). In ATL, the formula $\langle\langle A \rangle\rangle \phi$ says that agent (or coalition) $A$ can enforce $\phi$ to come about. In your case, $\langle\langle P_1 \rangle\rangle \text{Win}_1$.

In modal µ-calculus, it should definitely be doable. Something like $\mu Z . \big( \text{Win}_1 \lor \Diamond \Box Z \big)$?

Answer 2

You can't express it in LTL. Have a look at the slides by Katoen (https://moves.rwth-aachen.de/wp-content/uploads/lec18-2.pdf), slide 108. From that and theorem 6.18 from book Principles of Model Checking, you know, that no equivalent LTL formula exists.

Intuitively, your CTL formula is correct. But keep in mind, that Player 1 can still lose if he chooses a wrong move every time. If you don't want that, change the second quantifier to "for all". With that you say: there exists a path, where always player 1 wins no matter what, i.e. $ \exists \square\forall \lozenge Win_1 $.