Question

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

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top