# Omega automata 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?

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?

by (142k points)
Yes, I understood now. That's right. Thank you.
Can you please also explain my second doubt in the same question?
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.