# Doubt regarding converting to CTL

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?

edited

+1 vote

Looks fine to me, it is an alternative solution.
by (166k points)
selected by
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?