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.