This text includes definitions of the Kripke structure, CTL (Computation Tree Logic), and verification of the basic algorithm for Model Checking based on CTL in [10].