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.