[DOUBT] Translation of temporal formula to LO2

Question

In paper 17.02.2021, the solution to the conversion of the formula to LO2 is given. However, I could not understand how the timesteps are assigned to the LO2 formula.

I came up with the below solution while solving, as my understanding was, that F(phi) assigns timestep t1 to phi. Is the answer written below an accepted one?.

Thanks for your help.

Answer 1

F[a WU b] is translated to

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

which has a free occurrence of t0 and also bound occurrences. You may rename the bound occurrences and then you get the following

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

If now now exchange t2 and t3, you get your formula.

Comments

Thanks a lot for the explanation. As you mentioned, that exchanging t2 and t3 would yield the equation I got, I wonder if the solution I got would still be accepted.

If so, could you please tell me if any of the 3 solutions would be accepted?

---

Renaming bound variables does not change the meaning of a formula unless names of free variables in the scope of the quantifier are chosen. Hence, all of the formulas discussed above are equivalent to each other.

---

Thanks a lot for the help. It makes sense.

---

May I know the rule that led to:

F[a WU b] is translated to

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

---

The rules are:

[a WU b]{t0}  <=> ∀t1. (t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2≤t1 → ¬b[t2])) → a[t1])
[F c]{t0} <=> ∃t1. t0≤t1 ∧ c[t1]

---

Thank you, Professor. Would you please let me know where I can find these rules in the lecture slides?

---

These are not really rules, that is just the semantics of the temporal logic operators. But you can also easily get that from the LTL tool https://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html:

[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]
[a SW b] := ∃t1. t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2<t1 → ¬b[t2])) ∧ a[t1] ∧ b[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 WW b] := ∀t1. (t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2<t1 → ¬b[t2])) → (b[t1] → a[t1]))