In these lectures, we study the mu-calculus, CTL* and some of its subsets such as LTL and CTL, from a computational viewpoint. Among others, we treat the symbolic (fixed point based) algorithms for CTL, and fair CTL. The mu-calculus is discussed and its complexity is analysed. Transformations of the mu-calculus model checking problem to the frameworks of Boolean equation systems and Parity Games are addressed, combined with advanced algorithms for solving the latter artefacts.