Translation between different logics

Question

Q. EF¬ [a B Gb]

EF[¬ a SU Gb]   

EGb  // F[a SU Gb] = Gb

Could you please let me know if this is correct ?

Answer 1

Almost, I think, there are these two ways to generate a CTL formula

    EF¬[a WB Gb] = EF[¬a SU Gb] = EF E[¬a SU Gb] = EF E[¬a SU EGb]

or

    EF¬[a WB Gb] = EF[¬a SU Gb] = EFGb = EF EGb

Comments

Thank you for the explanation.

For the second part  
EF¬[a WB Gb] = EF[¬a SU Gb] = EFGb = EF EGb

In this you have replaced F[¬a SU Gb] to FGb, so does it mean F[¬a SU Gb] = FGb or you are seeing whole context of EF[¬a SU Gb] ?

I have read that F[¬a SU Gb] = Gb, could you please correct me ?

---

We have F[¬a SU G b] <-> F G b, but not F[¬a SU G b] <-> G b. Here is a little proof, but you may also use https://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html to check:

F[¬a SU G b] = F(Gb | ¬a & X[¬a SU G b]) = FGb | F(¬a & X[¬a SU G b]) = FGb

The latter is seen as follows: if FGb holds, both FGb | F(¬a & X[¬a SU G b]) and  FGb are true. Otherwise, we have GF¬b, so that infinitely often b is false, and therefore Gb must be always false. But then [phi SU Gb] is also always false.

---

I got your point.
Thank you for the explanation.