Depending on the depth you want to understand the topic, I can also recommend the (nicely written) article "an automata theoretic approach to branching time model checking" by Kupferman, Vardi, and Wolper. It presents a unified approach for model checking LTL, CTL, CTL*, and mu-calculus. I see this approach as a versatile set of tools to handle proof obligations on finite state systems. The article also contains many useful pointers to earlier approaches.
(In my oppinion, the book "principles of model checking", though perfectly fine for teaching, is a little too wordy to enter the material as a researcher. It also does not contain the approach of the article above, but relies on older approaches building solely on nondeterministic Büchi automata on words instead of alternating Büchi automata on trees.)
Merry Christmas.