When is the Induction Base valid?

Question

We want to prove whether AGp holds by means of induction. Check whether the property p is inductive (i.e. whether p -> [ ] p holds).

Property p should be inductive on this structure because the states {p} and {p,q} are universal predecessors of p.
However, I'm not sure whether the induction base is valid because the initial state does satisfy p -> [ ] p in the sense that we're in !p. Due to the missing transition from the initial state to the p-states however, the states satisfying p -> [ ] p cannot be reached which is why I'm not sure whether the induction base is valid.

If there needs to be a transition, the induction base should be satisfied by this structure, right?

Answer 1

To prove a property like AGp by means of induction, you have to prove

1. induction base: initial states -> p should be valid, i.e. the initial states should be included in p. However, this is not the case, since the only initial state s3 does not satisfy p. So, the induction base is wrong, and the initial state is already a counterexample.
2. Induction step: p->[]p should be valid which holds in this example. However, without a valid induction base it does not yet mean that AGp holds, and your example shows clearly the additional value of a valid induction base.