Translate formulas to equivalent L02 formulas.

Question

Translate the following formulas to equivalent L02 formulas (From paper: August 27th, 2019).

Temporal to LO2

(a→(F¬b)) ⊕ (G(a↔b))

Automata to LO2:

A∀ ({q,p}, ¬q∧¬p , (Xq↔(¬q∧¬a))∧(Xp↔(¬p→q)),GFp)

my solution:

∃ q,p. ¬q ⁽⁰⁾ ∧ ¬p⁽⁰⁾ ∧ 

( ∀ t. ( q^(t+1) ↔ ¬ q ^(t) ∧ ¬a^(t) ) ∧ (p^(t+1) ↔ ¬p^(t) → q ^(t) ) ) ∧

 ∀ t₁ ∃ t₂. t₁ < t₂ ∧ p^(t2)

Questions:

1. can you please explain how to convert temporal to LO2, When I apply the algorithm of the chapter VRS08-PredLogic- slide# 48 it usually explodes the result into a very long formula but when I see the exam solutions they are very short.

    1.1. Also I get confuse when calling the method recursively with the new time like in the case of SU and PX where "t1" is passed but the input to the function is always "t0" which also propagates to the internal cases of the algo. For instance [PXφ SU ψ] may lead to the recursive time calls

   1.2 In general when to use "≤", "<" for time t1, t2, etc and quantifiers?. 

    1.3 Is there a better short approach to solve these kinds of questions?

2. Is the solution of automata to LO2 correct to the given automata (In the exam solutions it is explained using state transition diagram )?

3. In the algorithm " ΘLO2(t, Φ) " of the chapter VRS08-PredLogic slide# 25 the acceptance condition always uses "∀t1.∃t2.t1" but in the exam solution i also see it reversed in case of FG. I believe it should be "∀t1 ∃ t2. t1 < t2" for  GF and "∃ t1 ∀ t2. t1 <t2" for FG. Please correct me if I'm wrong.

3. In these type of questions when do we use "t1 ≤ t2" and "t1< t2". Is there any rule of thumb?

Link to the paper for the reference (Page 26).

https://es.cs.uni-kl.de/teaching/vrs/exams/2019.08.27.vrs/2019.08.27.vrs.solutions.pdf

Answer 1

To convert LTL to LO1 (or LO2 which is a superset of LO1), you really just follow the algorithm on the slide you mentioned. The teaching tool https://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html with option "translate given LTL formula to LO1" does the same. Maybe we sometimes simplified the formulas before or after translation, but apart from that, there is no further magic.

You can always use fresh variable names for the time, i.e., t0,t1,t2,t3,t4... but to emphasize that LO1 is a very special first order logic that only requires two free variables, the tool and the algorithm reuse variable names. There is no need to do so, feel free to use new names.

When to use ≤ or < depends on the temporal logic operator. Gp means that p holds now and also in the future; [a SU b] means that a has to hold up to the time where b holds, but not necessarily at that point of time. So, it depends on the operator.

I don't see a much better approach to solve that; but maybe you first try to simplify the formula.

2. I think that your solution of the automaton is correct. 

3. Slide 25 explains how to translate a Büchi automaton which has acceptance condition GFphi. In case you have a co-Büchi automaton with acceptance condition FGphi, it is the condition you mentioned.