Exam August 21, 2018 Q.8(e)

Question

Hi,

I think the below solution is wrong or perhaps my understanding is not correct. All of the formulae is same except EGa and Ga, EGa, as far as I know, means that there must be one path which satisfies Ga. In the solution, there is a statement saying path looping in s2 satisfies S1. The path is a ,G b how does this satisfy E(Fb and EGa)? 

Answer 1

The solution is correct. 

Look, the formula E((F b) & EGa) can be rewritten to the equivalent formula (E F b)&(E G a) which is possible since EGa is a state formula and has to hold in the first state of the path that should satisfy (F b) & EGa for the entire formula E((F b) & EGa). However, the path that satisfies (F b) & EGa, and the path that satisfies Ga in EGa may not be the same. 

In the example, we have

    s0 |= E(F b & E G a)
    since s0s1∞ |= F b & E G a

    since s0s1∞ |= F b and s0s1∞ |= E G a

    since s0s1∞ |= F b and s0 |= E G a

    since s0s1∞ |= F b and s0s2∞ |= G a

However, 

    s0 |/= E(F b & G a)
    since neither s0s1∞ |= F b & G a nor s0s2∞ |= F b & G a
    since neither s0s1∞ |= F b  nor s0s2∞ |= G a

Clearly, I may continue to explain why the latter is the case, but I guess that you can agree from here. 

Comments

Thanks Professor, why does a has to hold in s0? Isnt s0 already satisfies Fb and EGa ? Does EG a means that first state has to satisfy a?

---

We need "a" to hold in s0 to have s0 |= E G a, since the latter means that "a" always holds on a path starting (and including) s0.

---

Understood thanks alot