Translation between different logics

Question

Hi,

I have 2 questions 

1) Is there a precedence when translating between formulas, e.g. what is the precedence when we have !,(),[]

2) In the example above, how do we read  the LO1 formulas and how is it translated to LTL, in some of the previous answers you gave you mentioned there are given LTL templates but i am not sure how to proceed with that.

Answer 1

With templates, I meant the formulas that are generated in the recursive calls of algorithm Tp2Od on slide 48 in Chapter VRS-08-PredLogic.

For instance, consider the given formula where I have done some irrelevant variable renaming (since that form came out of my tool):

∃t1. t0≤t1 ∧ (∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → ¬a[t2])) ∧ (∀t1. (t0≤t1 → a[t1] ∧ b[t1])))

Looking at the above formula, we can clearly see that ∀t1. (t0≤t1 → a[t1] ∧ b[t1]) stems from G(a&b) applied at time t0, hence, we may now consider with alpha(t0) := ∀t1. (t0≤t1 → a[t1] ∧ b[t1]) the following formula:

∃t1. t0≤t1 ∧ (∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → ¬a[t2])) ∧ alpha(t0))

Again, (∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → ¬a[t2])) ∧ alpha(t0)) is the template of a SU operator with arguments ¬a and alpha, so that the above formula means with beta(t1) = ∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → ¬a[t2])) ∧ alpha(t0)

∃t1. t0≤t1 ∧ beta(t1)

The above means F beta (applied at time t0), and thus

F[¬a SU G(a&b)]

Comments

About operator precedences in the teaching tools, see https://q2a.cs.uni-kl.de/1774/questions-about-temporal-logic?show=1774#q1774. The quantifiers ∀ and ∃ are thereby treated like the fixpoint operators. If you are in doubt for a exam problem, better ask in these cases.

---

I guess you are now talking about another problem and you don't clearly say which one which makes it hard to discuss with you. It seems that there is another question for ∃t1. t0≤t1 ∧ (∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2≤t0 → ¬b[t2])) ∧ a[t0]) which has the equivalent LTL formula F[a SB b] and you are wondering whether you could list equivalent LTL formulas also.

If I am right that this is question, then let me say that I would be surprised to read F(a & !b) instead of F[a SB b] (even that is the same) so that you should definitely add a comment about this. Moreover, the formula you are listing has to be equivalent, and hence, F[!b SU a] is not a correct answer (it is just implied, but the other direction of the implication is not valid).

---

sorry i didnt make the question clear, the question is

∃ t0.0 ≤ t0 ∧ ∃ t1.t0 ≤ t1 ∧ (∀ t2. [(t0 ≤ t2 ≤ t1) → ¬bt2]) ∧ at1

The solution given in the past exam question was F[a SB b] / F(a & !b). Since we know that t2 <= t1 why cant we say F[!b SU a]

---

The solution is F[a SB b] which is not the same as F[!b SU a]. Look, for F[!b SU a], we would get

∃t1. t0≤t1 ∧ (∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → ¬b[t2])) ∧ a[t0])

while for F[a SB b], we get

∃t1. t0≤t1 ∧ (∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2≤t0 → ¬b[t2])) ∧ a[t0])

It looks almost the same, but the former has a t2<t0 while the latter has t2≤t0. That is the difference between the two formulas!

---

oh, just saw that. thanks