Doubt in Temporal logic lecture

Question

slide 41 - chapter 7 - temporal logic

I have seen this part of lecture (2-3 times) where this slide has been explained but I am still confused. On left hand side we have CTL form and on right hand side we have non-CTL form?

Answer 1

Just to make sure that we talk about the same slide: 

Now, the answer to your question: If you assume that phi and psi would be CTL formulas, then all the left hand sides would also be CTL formulas and there would not be a problem. However, the slide discusses the problem that in front of a temporal operator we might miss a path quantifier. So, assume you have EF Gp which is not a CTL formula. Then, this slide tells you that you can add for any formula EFphi a path quantifier to obtain EFE phi and that make then EFGp a CTL formula EFEGp. The slide does not say whether the left or right hand side is a CTL formula, but it does say where you can add path quantifiers that you may miss to transform a formula which is not in CTL syntax (but equivalent to a CTL formula) to the CTL syntax.

Comments

Ok. Now I understand. The example you provided is really helpful. Thank you so much.