Query Regarding LO2

Question

I was trying to convert LTL to LO2, i used the Algorithm mentioned on the slide. On the left side, the solution I got by doing the algorithm but on the right side, the answer is given in the question paper. Can you help me to figure out what went wrong? [I have abbreviated big formulas to A , B and C respectively ]  

Answer 1

You have mixed up the weak and strong until operators. In the exam problem, it was a weak until, while your solution considers a strong until.

Comments

okay. But I have a question. The given question was F[a WU b]. First I found the LO1 for F and the remaining part was [a WU b]. I used the below syntactic sugar.
[ϕ WU ψ] := [ϕ SU ψ] ∨ Gϕ.
And I proceeded with this. So it will be a case for disjunction and did split these. After that, I found LO1 for [a SU b] and then Ga. And finally combined everything together. So will it have any other impact?

---

I see that is fine also. Of course, you can generate many equivalent formulas in different ways. The one you had in mind is fine also.

---

Thanks for the advice. I will stick with this kind of reduction rule and work on the algorithm. Thank you, Professor.

---

You can go many ways: If the formula F[a WU b] is translated directly, you get
∃t1. t0≤t1 ∧ (∀t0. (t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2≤t0 → ¬b[t2])) → a[t0]))

If you replace it with the equivalent formula F([a SU b] | G a), you get
∃t1. (
        (∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → a[t2])) ∧ b[t0]) ∨
        (∀t0. (t1≤t0 → a[t0]))) ∧ t0≤t1

---

Φ = F([a SU b] | G a)

Step 1: Tp2Od(t0, F([a SU b] | G a)), which is FΦ
             Ψ := ∃t1. t0≤t1 ∧ Φ ;
             ΨA := ∃t1. t1≤t0 ∧ ([a SU b] | G a) ;

Step 2: Tp2Od(t0, [a SU b] | G a), which is ϕ ∨ ψ
             Ψ := Tp2Od(t0, [a SU b]) ∨ Tp2Od(t0, G a);

Step 3: Tp2Od(t0, [a SU b]), which is [ϕ SU ψ]
            Ψ := ∃t1. t0 ≤ t1 ∧ Tp2Od(t1, b) ∧ interval((t0, 1,t1, 0), a)
                    Tp2Od(t1, b) = b(t1)
                    interval((t0, 1,t1, 0), a) = ∀t2. t0 ≤ t2 ∧ t2 < t1 → Tp2Od(t2, a);
                    Tp2Od(t2, a) = a(t2)
                  ΨB := ∃t1. t0 ≤ t1 ∧ b(t1)   ∧ ∀t2. t0 ≤ t2 ∧ t2 < t1 →a(t2)

Step 4: Tp2Od(t0, G a), which is Gϕ
             Ψ :=  ∀t1. t0 ≤ t1  ∧ Φ
              ΨC:=  ∀t1. t0≤ t1  ∧ a(t0)

Step 5: Combining all :
            ΨA  ∧ (ΨB ∨ ΨC)(t0)

My final solution is :
∃t1. t0≤t1 ∧ ((∃t1. t0 ≤ t1 ∧ b(t1)  ∧ ∀t2. t0 ≤ t2 ∧ t2 < t1 →a(t2) )∨ (∀t1. t0≤ t1  ∧ a(t0)))
     
Is this formula in reduced form? Or are they different? I am not sure how to give the numbering for "t".
∃t1. (
        (∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → a[t2])) ∧ b[t0]) ∨
        (∀t0. (t1≤t0 → a[t0]))) ∧ t0≤t1

---

Your formula is not correct; you have to use new variables since otherwise the free variables are bound which not not be the case.

Your formula is as follows

∃t1. t0≤t1 ∧ ((∃t1. t0≤t1 ∧ b(t1) ∧ ∀t2. t0≤t2 ∧ t2<t1 → a(t2) ) ∨ (∀t1. t0≤t1  ∧ a(t0)))

but should be rather

∃t1. t0≤t1 ∧ ((∃t3. t1≤t3 ∧ b(t3) ∧ ∀t2. t0≤t2 ∧ t2<t3 → a(t2) ) ∨ (∀t4. t1≤t4  ∧ a(t4)))

The above is then correct as far as I can see.

---

Are there any general rules for using new variables? [Is it okay to take t3<t2 like that?]
Can this be a valid one?
∃t1. t1≤t0 ∧ ((∃t2. t1 ≤ t2 ∧ b(t2)   ∧ ∀t3. t1 ≤ t3 ∧ t3 < t2 →a(t3)) ∨ (
∀t4. t1 ≤ t4  ∧ a(t4))

---

For any instance of Tp2Od that generates a formula with quantifiers, you need fresh variables in case that the body formula would have already that variable that would be used for quantification.

---

okay..I got it now..Thank you, professor.