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

915 questions

1k answers


441 users

0 votes

Convert LO2 to LTL formula :

In above question why are we using G in F[ a SU Gb]? 

In this question why are not we using G before b, in F[ a SB b]?

Because both have for all time t2 on b.

I getting confused which part of LO2 is providing G operator?

Thank you in advance 

in * TF "Vis. and Sci. Comp." by (870 points)

1 Answer

0 votes
Short answer to the first question: It is almost the definition of the semantics of F[a SU (G b)]. This is explained in detail as follows: According to the semantics of the temporal operators, F[a SU (G b)] evaluated at time t0 is equivalent to the following LO2 formula:

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

Since (∀t2. phi) & (∀t2. psi) = ∀t2.(phi&psi), we can rewrite this:

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

Let's compare it with the one given in the solution: First, we have there t0=0, so that we obtain

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

Let's now rename t1<-t0 and t0<-t1:

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

which is exactly what the example solution is. So the answer is that the given formula is almost what you get by the LTL semantics of the formula F[a SU (G b)] (evaluated at initial time 0). Note that t0 refers to the F operator, t1 to the even of the SU operator and t2 for the quantification to make sure that a holds until t1 and also that b holds from there. Note that binary operators like SU introduce two quantifiers; an existential one to make sure that the event will eventually hold, and a universal one to make sure that the other property will hold until then.

Second question: Looking at the formula, you can see that it demands that a time t0 shall come where something from there will happen. That means F phi, where phi is the property that shall hold at time t0 which is ∃t1. t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2≤t1 → ¬b[t2])) ∧ a[t1]. What does it say? There shall be a time t1 such that a holds there, and for all points of time t2 with t0≤t2 ∧ t2≤t1 we have ¬b[t2]. Hence, a holds before b holds when looking from t0 onwards into the future. Thus, we have F([a SB b]), since a must eventually hold.
by (142k points)
Imprint | Privacy Policy