If there are multiple initial states in the Kripke structure given for Local Model Checking.

Question

In the Local Model Checking questions, if there is one initial for a given Kripke structure we start the process with this initial node. 
If there are multiple initial nodes, it is being mentioned in the question with (K, initial node to be considered).
In the attached image (2021 Aug 4a question), though there are multiple initial nodes, the solution started working with the s1 initial state. As the given specification S1 did not hold on initial state s1 we stopped the process and came to a conclusion. 
If the specification holds on initial state s1, then do we need to check if the specification holds on the other initial state s6 also (i.e do we need to check for all initial states)?

Answer 1

A formula holds on a Kripke structure iff it holds on all initial states. Hence, to prove that formula holds on a Kripke structure with local model checking, you would have to check for all initial states that they satisfy the structure. To prove that the formula does not hold on the Kripke structure, it is sufficient to find one initial state that violates it.