Doubt in Local Model Checking

Question

In the above solution, why didn't we solve for initial state s1 as well. For local model checking, we need to solve for all the initial states right?

Answer 1

Yes, a property holds on a Kripke structure if the property holds on all initial states of that structure. As it does not hold on the one state used in the local model checking tree, we already know that it does not hold for the structure and there is no need to check for the other initial states.