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

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 ?

$$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.

• Will AGFstart in CTL* be AGAFstart in CTL? – gateway2745 Dec 8 '19 at 16:20
• @physics123 - By coincidence (well, not really coincidence, but it's usually not the case), the formula $AGFstart$ is in fact equivalent to $AGAFstart$. But don't read too much into this. – Shaull Dec 8 '19 at 19:14