CTL formula for “for every computation it is always possible to return to the initial state”

Question

In the book 'Principles of Model Checking' by Christel Baier and Joost-Pieter Katoen they state that the CTL formula for " for every computation it is always possible to return to the initial state" as 'AGEF start'. I was wondering whether the formula 'AGF start' would also be a valid one ? Is this correct ?

Answer 1

$AGF start$ is not a well-formed CTL formula, since in CTL you cannot write GF. Every temporal quantifier must be preceded by a path quantifier.

However, $AGF start$ is a formula in CTL*, so we can ask your question about CTL*:

Is the formula $AGFstart$ equivalent to $AGEFstart$?

The answer to this question is no. The first formula says that in every path, you will visit start infinitely often, while the second one only claims that on every path, you can always find some way to get back to start.

Try constructing a system that satisfies one but not the other.

Hint: if $AGFstart$ holds, then $AGEF start$ also holds.