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?
AX
and possibility meansEX
, so what does exists mean here? anyways, I believeEF Win_1
should say it, namingexists a path, eventually Win_1
. $\endgroup$