CTL Property to Temporal Property

39 views

Paulina Maurer

Sep 14, 2021, 7:51:27 AMSep 14
to tlaplus
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

Sep 14, 2021, 9:33:58 AMSep 14
to tlaplus
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.