Doubt in translating to CTL

Question

Exam : 17.02.2021 : Q 8 d : 2021.02.17.vrs.solutions.pdf (uni-kl.de)

Q. How XX is removed in first step ?

I came up with below solution :

Could you please explain this ?

Answer 1

Your solution is also correct. The LTL formula X X G F[a SU b] is equivalent to the LTL formula  G F b, so that the X-operators are not that meaningful here. You may also add further ones, since X ... X G F phi is equivalent to G F phi, since if phi holds infinitely often, it will do so also after some finite time. The other thing that you used and the example solution used as well is that F[a SU b] is equivalent to F b: If F[a SU b]  holds at some time t, then there is a point of time t+delta where b holds, and therefore also F b holds. Conversely, if F b holds, then there is a point of time t where b holds, and at that time also [a SU b] holds, since b implies [a SU b].

Still confused?

Comments

Thank you for the detailed explanation.

The first part regarding X X G F[a SU b] is clear, just one question is it same for .. X F G phi as eventually globally phi holds, so at some point of time phi will hold infinitely ?

For second part F[a SU b] :
So it means that, as this is SU hence when b holds eventually, F [a SU b] holds, so in future time t if b holds then it is same as F b both results in same.
Because if b never holds then both F [a SU b] and Fb doesn't hold. So in short as you have said b implies [a SU b].

---

Yes, also (F G a) <=> (X F G a) is valid. And no comment to the second part, that is fine.

---

Thanks a lot :)
It is clear now.