3
$\begingroup$

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

Improve this question
$\endgroup$
1
  • $\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, 2017 at 17:29

1 Answer 1

Reset to default
4
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • $\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, 2017 at 15:03
  • $\begingroup$ @hubsi Yes, that is correct. $\endgroup$
    – Klaus Draeger
    Mar 7, 2017 at 15:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.