# Exam August 21, 2018 Q.8(e)

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)? +1 vote

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.

by (147k points)
selected by
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