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