Translation between different logics

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 ?

+1 vote

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

by (142k points)
selected by
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.
Thank you for the explanation.