I'm currently trying to evaluate a CTL* expression and am not sure how to stepwisely evaluate the queries. For example I have EFG p. This means something like 'there is a path where eventually there exists a state s where from there on, globally p holds true'.

Globally means that for all successors of a state on all paths starting at this state a certain property holds true.

Applied to the example above, this would mean when evaluating EFGp on a model with init-state s0, that there exists a path from s0 to a state s' where from there on all succeeding paths have the property p. But wouldn't this imply that this is equivalent to EFAG p?

Is it in general possible to evaluate such queries stepwise (operator by operator) or do I have to consider all operators at once?

best regards

  • $\begingroup$ In class you were taught the semantics of CTL* expressions. The semantics tell you the meaning of every possible expression. $\endgroup$ – Yuval Filmus Mar 7 '17 at 17:29

Your interpretation of the $G$ modality is incorrect; it does not inherently talk about all paths. In particular, the example you give specifies that there is a path such that from some point on, all states on that path satisfy $p$.

As you suspect, for CTL* it is in general not possible to use a simple bottom-up evaluation, as you would for CTL, the reason being the LTL-like nested temporal operators.

  • $\begingroup$ ok so for the previous example EFGp the subterm FGp is evaluated with respect to a single path (and E obviously looks for one path that satisfies this property). in the other example EFAGp, EF looks for some state s and for this state s, all possible successor states s' (on all paths starting at s) assert property p. Is this interpretation correct? $\endgroup$ – hubsi Mar 7 '17 at 15:03
  • $\begingroup$ @hubsi Yes, that is correct. $\endgroup$ – Klaus Draeger Mar 7 '17 at 15:14

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.