Induction base w.r.t AG(Condition) and EG(Condition)

Question

While checking the induction rule on the Kripke structure, if the question asks for AG(condition),

Here for the induction base to hold, we check whether the condition is satisfied by "all" the initial states.

If the question asks for EG(condition), for the induction base to hold, does it need to satisfy any of the initial states present or all of the initial states present?

Answer 1

In general, a Kripke structure satisfies a state formula phi if and only if phi holds in all initial states of the Kripke structure. Hence, we have to check for both EG phi and AG phi whether they hold on all initial states if we want to know whether the formula holds for a given Kripke structure.

That means for EG phi that every initial state has an infinite path where phi holds. If phi is a state formula, this implies that phi must also hold on all initial states. For the induction step, it is then sufficient to prove that every state that satisfies phi has at least one successor state that also satisfies phi.