Doubt in induction

Question

In the above question, initial state satisfies the property p->q, then how does it not hold on the Kripke structure?
Are there any generalized steps to see the induction base and induction step?

Answer 1

Well, a state formula phi holds on a Kripke structure if and only it holds on all of its initial states. When we check whether a safety property AG phi holds on a Kripke structure, we therefore need to check whether AG phi holds in all of its initial states. This means that phi always holds on all infinite paths that start in one of the initial states.

To do this, we may check whether phi holds on all initial states, if not, then AG phi does also not hold in all initial states. If phi holds on all initial states, it may still be the case that AG phi does not hold in all initial states. Just think of a successor state of an initial state that violates phi. So, you were confused with the question whether phi or AG phi holds on all initial states.