LTL to LO1

Question

I was trying to convert one LTL formula to LO1. Could you please check what I have done wrong? I have encountered one Term instead of a Variable, and in the LTL to LO1 algorithm I could not find a perfect match in the case statement. 

How could I proceed further?

Answer 1

You can just follow the semantics of the formulas, but the way to reduce the operators to Until operators to apply the algorithm on the slide should also work fine. If you move in the negation symbol (which you don't have to), you should get the following:

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

You can compute that also with https://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html

Comments

Okay...But for  Tp2od(t1,1) , in this  case "phi is 1" and which case statement i can use. Since it's a term, can i use the term itself?

---

Yes, that is the idea of the function, and the term should refer to the time t0 which is the other argument of the function. For constants like 1, that does not matter, however,

---

I got the point. Thanks for clarifying.