Abstract: To improve the description and verification ability of the Colored Petri Net, One Model-checking Method for Colored Petri Nets which is based on the Propositional projection temporal logic is proposed. Initially, Buchi automata is constructed, which is equivalent to the negative form of Propositional projection temporal logic. Followed by, the product graph of the Buchi automata and the ratability graph of Colored Petri Nets are created. This will detect whether the acceptable language of product graph is null. Subsequently, whether the system property is satisfied which is described by PPTL formula can be judged. PPTL is more expressive, so the method can effectively improve the description and verification ability of the Colored Petri Nets.