
In the model I pasted above where $S_0$ and $S_1$ are starting states, is the $EXp$ formula satisfiable?
$$M,s\vDash EXp$$
Does it have to be satisfiable for all the starting states given the $M$, $s$? So to speak "There exists a next state in which the $p$ is satisfied" for both starting states or one of the states is enough, e.g. $S_0$ is satisfied while $S_1$ does not satisfy the formula. Is it the latter or the former?
$M, s \vDash EXp$ does not make sense since $s$ is not a state in the model.
However, $M, S_0 \vDash EXp$ is the case. Why?
Let us review the semantics of the formula.
$EXp$ means that there should exist a path from $s_0$ s.t the successor of $s_0$ in the given path satisfies the formula $p$ which is only the case of $p$ is included in the set of atomic propositions in the successor state.
I.e $M, S_2 \vDash p$ and therefore $M, S_0 \vDash EXp$.
As one of the states satisfy the formula, it is satisfiable.
Refer to the semantics given here or wikipedia