LO1 to LTL

Question

In this question, the solution was F[¬a SU G(a&b)]. I am a bit confused why we have G(a&b) and not just a&b

Answer 1

Have a look at https://q2a.cs.uni-kl.de/2060/translation-between-different-logics?show=2061#a2061

Comments

why can't we also say the same for !a i.e. G !a since t0<= t2

---

I don't get you point, I am afraid. The formula ∀t2. (t0≤t2 ∧ t2<t1 → ¬a[t2]) does not mean G¬a at time t0, since it just says that a is false from t0 up to t1, but does not state that remains false afterwards. So, it is just an [¬a SU ...] at time t0. So why do you think it should be G¬a? The other part of the formula even states that a holds from t1 onwards.

---

oh i get it now, i misread initially. thanks