# LTL Model Checking

Can someone please explain why the answer is it is true for every state, even though our product kripke structure doesn't have any initial state also if we remove deadends then we don't have any transitions in product kripke structure. Since formula asks for all the paths that satisfy the formula why we are showing in the states? why the answer is not for any formula it won't satisfy?

Exam paper: question 7 (b) +1 vote
It is because we are asking for a A-quantified formula. Such formulas hold in all states that don't have infinite outgoing paths at all which is the case here.
by (147k points)
Ok, I understand now. Thank you so much.
+1 vote
As you said. If there are no infinite transitions, then the existential formula cannot be satisfied.

If the formula is not satisfied, then its negation is satisfied. The negation of the existential formula is a universal formula. That isn't surprising. If there are no infinite paths, then all (of the zero) infinite paths satisfy any arbitrary criterion.
by (25.6k points)
Ok, I understand now. Thank you so much.