Translating F[a U b] to L02

Question

As I see that Weak Until is not used in the algorithm in lecture slides, how do we come to the answer shown below 

Answer 1

You can ask the teaching tool https://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html that knows all the cases. For instance:

G a ==> ∀t1. (t0≤t1 → a[t1])

F a ==> ∃t1. t0≤t1 ∧ a[t1]

[a WU b] ==> ∀t1. (t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2≤t1 → ¬b[t2])) → a[t1])

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

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

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

All of these cases, however, just follow the given semantics of the temporal operators and describe that in LO1.

Comments

Thank you very much for the answer.