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 textsfWin_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.
– HuStmpHrrr
Aug 19 at 16:59

AX

EX

EF Win_1

exists a path, eventually Win_1

@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 at 1:04

i see. do you have a reference to the notations you are using?
– HuStmpHrrr
Aug 20 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 at 3:22

1 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 $langlelangle A ranglerangle phi$ says that agent (or coalition) $A$ can enforce $phi$ to come about. In your case, $langlelangle P_1 ranglerangle textWin_1$.

In modal µ-calculus, it should definitely be doable. Something like $mu Z . big( textWin_1 lor Diamond Box Z big)$?

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

搜尋此網誌

Cyufjy