How to express the existence of winning strategy of the starter of a game in temporal logic? 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?
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)$?