2

I'm trying to create a valid CTL or LTL expression for model checking in NuSMV.

I have a variable in a game, with actors running around trying to catch each other. Variable is, State_Of_Game : {Win,Lose,Playing}

and I want to express that from every starting state the game can be both won or lost.

So, how would I implement this in CTL or LTL?

I was thinking something like AG (S_O_G = Win | S_O_G = Lose) but don't know how to implement that it is seen from every starting state.

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
Sven
  • 1,133
  • 1
  • 11
  • 22

2 Answers2

3

I'm not familiar with the SMV notation, so I am guessing about this, but the key points are:

  1. To avoid quantifying over all states at the outside: you don't want to say that all games can be either won or lost, but only the starting game. So just have a formula at the starting state with no outermost modality

  2. To use a conjunction, not disjunction: you want to assert both winnability and losability

  3. You need separate modalities wrapping each of the branches: winnability, losability is an existential claim, saying it is possible to attain a condition.

I think the formula you need is: (EG SOG=Win) & (EG SOG=Lose) at the root, which might mean in something like an init/start clause, or asserting at a named root clause. If SMV doesn't have the EG modality, you can translate into just AG using the equivalence EG p = !(AG !p), since the two are De Morgan duals.

Charles Stewart
  • 11,661
  • 4
  • 46
  • 85
-1

Try with this : AF(State_of_Game=Win| State_of_Game=Lose)

sam
  • 53
  • 4
  • This would be verified even by an initial state s.t. every possible path leads only to a state in which the game is lost (i.e. there is no possible winning strategy). The question asks for a property that is verified if every initial state admits both a winning and a loosing strategy. – Patrick Trentin Jun 11 '19 at 13:30