Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

912 questions

1k answers

1.4k comments

441 users

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?

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