Omega automata

Question

Can someone please explain:

1) Why G acceptance condition inplies F (yellow highligted part)?

2) which reduction formula of F are we using here? Because in none of the formulas of F intial state is 1. Also as per the reduction formulas of F, there is no reduction formula of F reducing to automata  with F acceptance condition. 

I am not able to understand. Can someone please explain?

Answer 1

Maybe we first make some equivalence transformations: 

    G(!b-> Xa) = G(b | Xa)

and second

    F(!b->(a | X a))
    = F(b | a | X a)
    = (F b) | (F a) | (F X a)

Hence, if we always have b | X a, we have at any point of time t either b or at t+1, we have a. If we should have b at time t, then we have (F b) at any time before t (hence, we have in particular F(b) at time 0). Otherwise, we have a at t+1, and thus, we have F(a) at any point before t+2, and also F(X a) at any point of time before t+1, in particular, (F a) and (F X a) hold therefore at time 0. 

Hence, at time 0, we can say that G(b | Xa) implies F(!b->(a | X a)).

Right?

Comments

Yes, I understood now. That's right. Thank you.
Can you please also explain my second doubt in the same question?
It would be really helpful.

---

The second point is due to the replacement of X a by a state variable q as explained on slide 72 of the temporal logic chapter. The transition relation enforces q to always behave as X a, so that we can replace X a by q. The next step that replaces the remaining F-formula is also due to such a rule given on the same slide.

---

okay. Got it. Thank you so much. It was really helpful.