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.

  • $\begingroup$ Will AGFstart in CTL* be AGAFstart in CTL? $\endgroup$ Dec 8 '19 at 16:20
  • $\begingroup$ @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. $\endgroup$
    – Shaull
    Dec 8 '19 at 19:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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