logicctlnusmv

constructing valid CTL or LTL expression (in NuSMV)

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.

Solution

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