Exam 2020 8. d) [closed]

Question

1.) Why is the red marked "implies" not an "and"? I found no formulas to convert G and F to LO2 in the lecture slides. I thought one would an "and" there.

2.) Task 8. c) asked for a translation from LO1 to LTL.

Where can we find formulas for LO1 to LTL or do we have to figure them out ourselves by thinking logically? I saw that there is a "!a SU something" by looking at the LTL --> LO1 formulas but that was all I could figure out.

3.) Is there a way to let the teaching tool translate from LO2 to LTL and vice versa?

4.) In the lecture slides it says "even the first order fragment LO1 of LO2 is sufficient". Does this mean the translation from LTL to LO2 is exactly the same as LTL to LO1 or is there anything we need to do slightly different?

Answer 1

First question: it is an implication since (G p) evaluated at time t0 becomes ∀t1. (t0≤t1 → p[t1]). You can see that as follows: You know that (G p) = ¬(F ¬p) and you know that F p is equivalent to ∃t1. t0≤t1 ∧ p[t1]. Hence, Gp is equivalent to ¬∃t1. t0≤t1 ∧ ¬p[t1] which is equivalent to ∀t1. ¬(t0≤t1 ∧ ¬p[t1]), and that in turn is equivalent to ∀t1. ¬t0≤t1 ⋁ p[t1] which is the formulation above.

Second question: There is indeed an algorithm which translates any LO1 formula to LTL. You don't need that however in these exam questions. Instead, we usually hide some LTL formula behind it, so that you should read what is expressed there and try to say the same in LTL. You typically find the direct semantics of an LTL formula there.

Third question: There is currently no teaching tool for translating LO1 to LTL. The converse can be done with the teaching tool https://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html when you select the option "translate given LTL formula to LO1".

Fourth question: yes, the translation from LTL to LO2 is the same as the translation from LTL to LO1. There is never a need for a second order quantification when we translate LTL to LO1. In principle, you could translate LTL to omega-automata which could then be translated to LO2, and then try to reduce that to LO1. However, that would be overly complicated.

Answer 2

1. What we do here, is quantifying over a subset. For the existential quantification, we want to find an element (here a point in time) that is both in the specified subset (here the correct time interval) and satisfies a certain property. For the universal quantification, we want to check all elements. If an element is not in the specified subset, we ignore it without failing the forall check (i.e. evaluating to true). If the element is in the specified subset, we must check the certain property. This case distinction is implement by an implication.
2. The standard approach is just imagining the paths that fit here, and expressing them as LTL.

Comments

On 3: I don't know of any.
On 4: LO1 are LO2 as well. So translating to LO1 is a valid way to translate to LO2.

---

Bonus answer: The LTL tool can also help with translating CTL* formulas to CTL. For example, if you want to translate A( (G a) | (F b) ) to CTL, use the option "translate as much as possible to CTL", and you will find A (G a | F b) = A [b WB (!a & E G !b)]