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

965 questions

1.1k answers

1.5k comments

451 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 https://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html

by (147k 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
...