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

912 questions

1k answers


441 users

0 votes

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?

in # Study-Organisation (Master) by (1.1k points)

1 Answer

+1 vote
Best answer

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

by (142k points)
selected by
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.

Related questions

Imprint | Privacy Policy