LTL to LO2 doubt

Question

Hi, 

I have a doubt regarding LO2 ,

F[a WU b] to LO2 formula. The answer for this is given :

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

But i got, 

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

I'm not sure how can we give the time. 

What i have is , 

we have: Fa = ∃t1. t0≤t1 ∧ a[t1] 

so F[a WU b] = ∃t1. t0≤t1 ∧ [a WU b][t1] 

[a WU b] = ∀t1. (t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2≤t1 → ¬b[t2])) → a[t1]), but we are starting from the time t1, so i replaced the time accordingly. 

And finally 

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

but timing are little bit different from tool and what i got. Could you please help on this, how can i give the time?

Answer 1

The teaching tool uses as few variables as possible. Indeed, one can show that three variables are sufficient because of the special kind of predicate logic that corresponds with LTL. You have used other names to avoid the shadowing of existing variables, which is safer than what the tool does. So, yes, your solution is correct.

Comments

Thank you professor