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
CTL* query evaluation order
logic;model checking;computation tree logic;temporal logic
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.