To settle various problems in computation tree logic possibility measure model validation process

such as high time complexity and low efficiency performance. The I-PM_CTL algorithm is proposed. The algorithm is based on the traditional model checking mark algorithm

so that it is adaptable to the need of mark detection of large-scale

highly complex formulas. The steps of the algorithm are as follows. Fristly

the logic tree formulas are calculated using relevant possibility measure

which is a preprocessing step to identify the uniqueness of the common sub-expressions. Secondly

it specifies the state of common sub-expressions and I-PM_CTL model

while maintaining the equilibrium of model checking space. Finally

this algorithm implements the verification

ensuring the I-PM_CTL formulas  verification to be completed in one time with high probability. The results of simulation experiments show that the IPM_CTL algorithm not only effectively reduces time complexity

but also improves the verification performance.