Translation from LO1/LO2 to LTL

Question

Exam : 13.02.2019 : Q 9 c : 2019.02.13.vrs.solutions.pdf (uni-kl.de)

I am using the algorithm presented on slide 48 of module 8 but I am unable to find the correct semantics there, I have solved other questions and I was able to find the correct LTL but this is not the case with this.

As the formula looks like LO2, could you please provide the slide no. where I can find the translation from LO2 to LTL ?

Could you please explain this ?

Answer 1

The translation of  G [b SW a] yields the following LO1 formula:

    ∀t1. (t0≤t1 → (∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → ¬a[t2])) ∧ b[t0] ∧ a[t0]))

We may use fresh variables for all quantified variables:

    ∀t1. (t0≤t1 → (∃t3. t1≤t3 ∧ (∀t2. (t1≤t2 ∧ t2<t3 → ¬a[t2])) ∧ b[t3] ∧ a[t3]))

replace t0 with 0

    ∀t1. (0≤t1 → (∃t3. t1≤t3 ∧ (∀t2. (t1≤t2 ∧ t2<t3 → ¬a[t2])) ∧ b[t3] ∧ a[t3]))

replace t1 with t0

    ∀t0. (0≤t0 → (∃t3. t0≤t3 ∧ (∀t2. (t0≤t2 ∧ t2<t3 → ¬a[t2])) ∧ b[t3] ∧ a[t3]))

replace t3 with t1

    ∀t0. (0≤t0 → (∃t1. t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2<t1 → ¬a[t2])) ∧ b[t1] ∧ a[t1]))

Comments

I can see that the last part of the translation provided by you is same as the one in question.
But I am unable to get how the result ended in G(F !(a&b) | [b SW a]).
As the given formula in the question is same as you have provided in the translation of G [b SW a].  
I didn't get about F !(a&b).

Also the Tp2Od(t0,phi) algo doesn't contain equivalent translation for SW.
Could you please also provide slide number where I can find this ?