Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

915 questions

1k answers


441 users

0 votes

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?

in * TF "Vis. and Sci. Comp." by (870 points)

1 Answer

0 votes

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)).


by (142k points)
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.

Related questions

0 votes
1 answer
asked Aug 17, 2020 in * TF "Vis. and Sci. Comp." by Anshu (870 points)
0 votes
1 answer
asked Aug 12, 2020 in * TF "Vis. and Sci. Comp." by Anshu (870 points)
0 votes
1 answer
asked Aug 11, 2020 in * TF "Vis. and Sci. Comp." by Anshu (870 points)
0 votes
1 answer
Imprint | Privacy Policy