# 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?

• could you explain what's square and diamond in your formalism of CTL? if i am not mistaken, necessity in modal logic means AX and possibility means EX, so what does exists mean here? anyways, I believe EF Win_1 should say it, naming exists a path, eventually Win_1. – Jason Hu Aug 19 '18 at 16:59
• @HuStmpHrrr There are two notational systems for CTL. You are using the one described in wiki. I am using "$\exists$" ($E$) to mean "there exists a path", $\forall$ ($A$) to mean "for all paths", $\Box$ ($G$) to mean "globally or always", and $\Diamond$ ($F$) to mean "finally or eventually". – hengxin Aug 20 '18 at 1:04
• i see. do you have a reference to the notations you are using? – Jason Hu Aug 20 '18 at 2:22
• @HuStmpHrrr Section 6.2.1 of the book "Principles of Model Checking" by Christel Baier and Joost-Pieter Katoen. – hengxin Aug 20 '18 at 3:22

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)$?
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$.