In general, <:> phi holds in a state if that state has a predecessor state which satisfies phi. Having computed the states S where phi holds, you can compute the states that satisfy <:>phi as suc∃(S).
Hence, if S={} holds, we have to compute suc∃({}) which means the set of states having at least one successor which is in {}. Since no state could be in {}, this is {}.
