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

1.1k questions

1.2k answers

1.6k comments

529 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 (2.7k 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 (166k 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

0 votes
1 answer
asked Aug 24, 2022 in * TF "Emb. Sys. and Rob." by CS_E (2.9k points)
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...