With the increasing complexity of systems, it is urgent to deal with the uncertain information in the systems. Besides, the state explosion problem is getting more and more serious. Existing model checking techniques are no longer suitable for the verification of such complex systems. We study symbolic CTL model checking based on possibility measure. Firstly, multiterminal binary decision trees (MTBDDs) and Boolean formula are respectively used to describe system models and properties to be verified. Secondly, the system models are normalized and simplified. Finally, system verification is completed by fixed point calculation. Our work is an integration of symbolic model checking and CTL model checking based on possibility measure, which can not only handle uncertain information in systems, but also maintain symbolic model checking's advantage of low demand for computation time and storage space. It is thus significant for the verification of complex systems.