Doubt in LO2 to LTL

Question

Exam : 14.02.2018 : Q 9 c part 2 : *2018.02.14.vrs.solutions.pdf (uni-kl.de)

Problem : Translate the following to LO2 :

I am trying to solve like this :

But I am little bit confused :

Q1. Can I apply distributive law to Universal quantifier like I did above ?

I came up with F[Xa SU Gb] but this is not right as per the solution and also I can see both a and b holds at the same time t2.

Also if I see interval part a is true in future and not at current time so I made it as Xa.

And the structure of Tp2Od looks like Gb.

Q2. Could you please let me know where am I wrong ?

Answer 1

The universal quantifier distributes over conjunctions, that is fine. If I am reading the exam problem correctly, the signals are applied to t1 instead of t2 which is unusual. At first I thought that this is a typo, but then I saw the in the same exam there is another problem with the other points of time.

For this one, I suggest the following reasoning: 

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

This suggests now F(b | XF(a&b))

Comments

@KS, I saw the lecture but couldn't find any direct formulas for the conversion involving LO1 and LO2. Am I missing something?

It would be great if you could help me with this.

---

LO1 is a subset of LO2, hence, there is no need for a conversion, and LO2 is strictly more powerful than LO1, so that there is no conversion that way. The above reasoning I made, was manually, and not done by an algorithm.