Short answer: No, that slide is correct.

More about that: In general, Kripke structures are allowed to have deadend states, and even initial states may have in general no outgoing transitions. `Allowed' means that we can define the meaning of temporal logic formulas on such structures. In particular, model checking properties of the ยต-calculus is no problem on all kinds of Kripke structures, and can even detect such deficiencies.

Why did we then bother you will all of these problems? By personal experience, I can tell you that if these deficiencies are there, something is wrong with the system that you are modeling, and if you would just check LTL properties (which state that on all infinite paths starting in all initial states something holds), you could prove everything on broken structures where there are no infinite paths at all. This way, you may "verify" those LTL properties, but these would just be vacuously satisfied as if you would prove some formula false->phi where phi is some very large formula.

So, while no "sanity checks" have to be made on Kripke structures to perform verification, it is strongly recommended to do so to make sure that the system model is not broken.