Doubt regarding converting to CTL

Question

I have a doubt regarding converting a formula to CTL. 

The given question was: convert " EXF [AGXFa SU AFb]  " to CTL.

My approach is :

EXF[AGXFa SU AFb] =  EXEF[AGXFa SU AFb]      Since EXϕ = EXEϕ 

EXEF [AGXFa SU AFb] = EXEFAFb                   

                              Since F[ϕ  SU ψ] = Fψ , where ϕ  = AGXFa  and ψ = AFb

Is it a valid solution or should we proceed from EFϕ = EFEϕ again and so on?

Please help to solve this.

Answer 1

Looks fine to me, it is an alternative solution.

Comments

Thank you, Professor. I have a small question,
If we have a CTL formula like "AGAXAFb", how can we simplify it, should we start from left to right [AGAphi to AGphi and go on to the right side] or right to left [ AXAphi to AXphi and go on to left side]?

---

I don' think that there is a general recipe for this. Wherever you see something to simplify, do that first to reduce the overall complexity.

---

Thanks for the suggestion.

---

I have seen that,
EGFphi can not be converted to EGEFphi. But, also there is a formula, EF=E/F/EFE [I am not sure whether it's a valid formula or not! ]
So if I converted F to EF, then it will become  EGEFphi. Could you please confirm this?