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?

  • $\begingroup$ 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. $\endgroup$ – Jason Hu Aug 19 '18 at 16:59
  • $\begingroup$ @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". $\endgroup$ – hengxin Aug 20 '18 at 1:04
  • $\begingroup$ i see. do you have a reference to the notations you are using? $\endgroup$ – Jason Hu Aug 20 '18 at 2:22
  • $\begingroup$ @HuStmpHrrr Section 6.2.1 of the book "Principles of Model Checking" by Christel Baier and Joost-Pieter Katoen. $\endgroup$ – hengxin Aug 20 '18 at 3:22

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

| cite | improve this answer | |

You can't express it in LTL. Have a look at the slides by Katoen (https://moves.rwth-aachen.de/wp-content/uploads/lec18-2.pdf), slide 108. From that and theorem 6.18 from book Principles of Model Checking, you know, that no equivalent LTL formula exists.

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

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.