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

I can't still see how we were able to tell (∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → ¬a[t2])) ∧ alpha(t0)) is a template of the SU operator.
The SU operator is given as = ∃t1. t0 ≤ t1 ∧ Tp2Od(t1, ψ) ∧ interval((t0, 1,t1, 0), ϕ);
How do we know that the recursive Tp20d call is !a and also why is the interval in the template for the SU operator is replaced by alpha(t0)

---

If we evaluate a formula [beta SU alpha] at time t1, then it means that there must be a point of time t0 so that alpha(t0) holds and for all points of time t2 with t1≤t2 ∧ t2<t0, we must have beta(t2). Having read this, compare it with the formula you are asking for. Matching beta with ¬a makes these statements identical, right?

While I used the semantics of the SU operator to explain this, you get exactly the same when you expand the call to the function Interval where Phi takes the rule of my beta and Psi the role of alpha.

---

thanks for the clarification, i understand how the formula is a template of the SU operator. In general, to solve questions like this are we meant to find betas and alphas and match them to the templates provided ?

---

More or less, yes. However, you may also need to rewrite the formula now and then a bit so that a suitable template comes out. So, at first have a look at the formula, try to find such templates, and if not, think about which one is closest and whether that might do here also.

---

i think you skipped my first question,
Is there a precedence when translating between formulas, e.g. what is the precedence when we have !,(),[]
I have doubts about the precedence of operations.

in this question ¬A(GXFb ∧ FXb) the negation was applied at the end after simplifying the inner formula

In this question ¬AXXGF¬E[1 U (Ab)] the negation was applied at the beginning

So is the precedence (),! ?

---

In the solution, the answer to the question below was F[a SB b] / F(a & !b). Can i also say F[!b SU a] as F[a SB b] -> F[!b SU a] or am i wrong ?

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

---

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