Global Model Checking Initial states

Question

If there are more than 1 initial states in given structure, does all the initial states should be present in the final set to prove the model holds or not, or even if one initial state is present it will satisfy the property?

Answer 1

By definition, a structure K satisfies a property phi, if and only if ALL initial states of K satisfy the property phi. Hence, all initial states must be found in the set of states of K satisfying phi.