Local Model Checking for multiple initial states

Question

If we are asked to perform a local model checking on a state transition diagram and it has more than 1 initial state and in the paper, an initial state is not specified. are we supposed to perform local model checking for ALL initial states?

Does that mean we will have as many trees as the number of initial states and all my satisfy to prove local model checking holds?

Answer 1

Yes, that is the case. For checking whether a structure satisfies a property, we need to make sure that ALL initial states satisfy the property. However, the proof trees of the initial states may have significant overlaps, but we need one proof tree per initial state.