CTL Property to Temporal Property

[Paulina Maurer]

I would like to model check this CTL specification as TP in TLA+

AG(SM1.state =s1) -> EF (SM1.state =s2)

Is this: (SM1 \ in s1) =>[] <> (SM1 \in s2) the correct translation?

[Willy Schultz]

To avoid any confusion, could you clarify what "SM1", "SM2", "s1" and "s2" are in your formula/specification? It's unclear to me what "(SM1 \ in s1)" and "(SM1 \in s2)" means given what you wrote. 

More generally, if you consider the following abstract CTL property (where P1 and P2 are state predicates):

AG(P1) => EF(P2)

I believe it is not possible to express this directly in TLA+ (or in LTL), since TLA+ can only express properties that hold for all behaviors of a system, whereas CTL formulas allow you to quantify over all behaviors of a system. (Or, at least, the formula is not expressible in a form that the model checker, TLC, can handle.) You may be able to use the model checker to check the above formula, though, with a bit of a "workaround". It would help to first be clear on the statement of your desired property, though. 

[Willy Schultz]

To follow up on this, you may be able to use TLC to check the CTL formula

AG(P1) => EF(P2)

with the following technique. You can check AG(P1) by simply checking that the formula []P1 holds. Separately, you can check EF(P2) via a simple "hack". The CTL formula EF(P2) is true iff there exists some system behavior such that F(P2) (written <>P2 in TLA+) holds. So, you can check the formula [](~P2) with TLC and see if the model checker returns a violation. If it does, then this means that there exists some behavior in which P2 holds at some point, so it means that EF(P2) must hold. If the model checker completes without a violation, it must mean that EF(P2) does not hold. So, this gives you a way to check EF(P2). I do not think you can do this in one step, though i.e. by checking a single temporal formula with TLC.