Short answer to the first question: It is almost the definition of the semantics of F[a SU (G b)]. This is explained in detail as follows: According to the semantics of the temporal operators, F[a SU (G b)] evaluated at time t0 is equivalent to the following LO2 formula:
∃t1. t0≤t1 ∧ (∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → a[t2])) ∧ (∀t1. (t0≤t1 → b[t1])) )
Since (∀t2. phi) & (∀t2. psi) = ∀t2.(phi&psi), we can rewrite this:
∃t1. t0≤t1 ∧ (∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → a[t2]) ∧ (t0≤t2 → b[t2])) )
Let's compare it with the one given in the solution: First, we have there t0=0, so that we obtain
∃t1. 0≤t1 ∧ (∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → a[t2]) ∧ (t0≤t2 → b[t2])) )
Let's now rename t1<-t0 and t0<-t1:
∃t0. 0≤t0 ∧ (∃t1. t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2<t1 → a[t2]) ∧ (t1≤t2 → b[t2])) )
which is exactly what the example solution is. So the answer is that the given formula is almost what you get by the LTL semantics of the formula F[a SU (G b)] (evaluated at initial time 0). Note that t0 refers to the F operator, t1 to the even of the SU operator and t2 for the quantification to make sure that a holds until t1 and also that b holds from there. Note that binary operators like SU introduce two quantifiers; an existential one to make sure that the event will eventually hold, and a universal one to make sure that the other property will hold until then.
Second question: Looking at the formula, you can see that it demands that a time t0 shall come where something from there will happen. That means F phi, where phi is the property that shall hold at time t0 which is ∃t1. t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2≤t1 → ¬b[t2])) ∧ a[t1]. What does it say? There shall be a time t1 such that a holds there, and for all points of time t2 with t0≤t2 ∧ t2≤t1 we have ¬b[t2]. Hence, a holds before b holds when looking from t0 onwards into the future. Thus, we have F([a SB b]), since a must eventually hold.
