CTL exam question

Question

I am solving the exam questions problem 4 (d) 2020.02.19.vrs.solutions.pdf (uni-kl.de). 

Question : A F E G a

Exam Solution :

My Approach :

In this I solved the inner part E G a which is {s2, s3, s6} intuitively.

But for AF which is "always finally" I get it wrong as shown in solution (Exam).

My intuition regarding A F phi is that in all paths eventually it reaches to states {s2, s3, s6} and as in the solution it says a counterexample of {s5,s4} but from what I understood that if we are in s5, AF phi means we can always finally reach to {s2, s3, s6} by taking a path s5 -> s4 -> s5 -> s2 (Reached). 

Could you please explain about A F phi i.e where I get it wrong ?

Comments

Interestingly, your intuition is right about F. A path that reaches the inner set eventually.

But AF means ALL paths from here (which means there is no other path from here).

The path that loops back and forth between S4 and S5 will never reach the said inner set. Hence, the A in AF is violated.

Answer 1

You are confused with quantification over paths and variables. The path quantifier A in AF phi asks whether for all infinite outgoing paths eventually phi holds. As the example solution explains, that is not the case since there is a path that violates this.

You believe that in s5, we can ALWAYS finally reach to {s2,s3,s6} which would be written as GF{s2,s3,s6}, and even EGF{s} but the exam problem asks for AF{s2,s3,s6}.

Comments

Thanks for the explanation.

Could you please briefly explain how path {s5,s4} is violating this so that I can understand the intuition behind this ?

---

The second line in the hand-written answer is precisely the answer to EF EG a without EG a.

In human words this would be “states from which at least one path reaches the inner set”. But the marked text in the solution says “every path …”.

---

So basically s5 and s4 is violating the A i.e every path because one path could always be in loop s5->s4 and never reach to the {s2, s3, s6}.

Thanks for this explanation.

---

While I was writing the comment (on the answer by KS), I did not see your comment yet. The second comment (the one on the question itself) includes the note on the infinite path looping between S4 and S5.

---

Yes now I saw your comment on the question.
Many thanks :)