Problem 8(c)

Question

Hello,

I have some trouble interpreting the solution given to the problems in the exams. For example in the solution given below, I don't understand why did we add F!(a & b) as the formula itself looks like its equivalent to [!a SU (a & b)]. Generally, how should I start reading these formulas? also what does (to <= t2 < t1) & (!a t2) means? does it means that at time step t2  (!a) must hold whereas timestep t2<t1 which in turn can be interpreted as G(!a) ? 

Answer 1

I admit that this is not straightforward and requires a little trick. The solution given is correct which you can see as follows. 

At first we consider subformulas and try to match them with given "LTL templates". That does not work well here, but a formula which is close to the inner part would be

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

which is the LO1 semantics of the LTL formula [¬a SU a ∧ b]. To simplify matters, let us now introduce the following abbreviations:

•     alpha(t1)   := a[t1] ∧ b[t1]
•     beta(t0,t1) := (∀t2. (t0≤t2 ∧ t2<t1 → ¬a[t2]))

so that the above formula becomes

    ∃t1. t0≤t1 ∧ alpha(t1) ∧ beta(t0,t1)

As already written above, that is close to what we actually need, i.e.,:

    ∃t1. t0≤t1 ∧ (alpha(t1) -> beta(t0,t1))

It is however possible to rewrite the above formula into the equivalent following form:

    ∃t1. t0≤t1 ∧ (alpha(t1) -> beta(t0,t1))
    = ∃t1. t0≤t1 ∧ (¬alpha(t1) ∨ beta(t0,t1))
    = ∃t1. t0≤t1 ∧ (¬alpha(t1) ∨ alpha(t1) ∧ beta(t0,t1))
    = ∃t1. t0≤t1 ∧ ¬alpha(t1) ∨ t0≤t1 ∧ alpha(t1) ∧ beta(t0,t1))
    = (∃t1. t0≤t1 ∧ ¬alpha(t1)) ∨ (∃t1. t0≤t1 ∧ alpha(t1) ∧ beta(t0,t1))

You can now clearly see that the second disjunct is the formula that we mentioned above, i.e., [¬a SU a ∧ b] and that the former disjunct is clearly F¬alpha, i.e., F¬(a ∧ b) (all evaluated at time t0). 

Having seen this, we now have

    ∀t0. 0≤t0 -> [F¬(a ∧ b) ∨ [¬a SU a ∧ b]](t0)

and that is clearly

   G(F¬(a ∧ b) ∨ [¬a SU a ∧ b])