An Improved POCTL Model Checking Algorithm Based on Preprocess Mechanism

Abstract

In order to improve the defects of high time complexity and low efficiency in PoCTL model detecting, according to traditional model checking marker algorithm, an improved PoCTL model checking algorithm based on preprocess mechanism which could be applied in large scale and high complexity is proposed in this paper, e.i PM_LA algorithm. Uniqueness of public sub expression is preprocess marked through relative PoCTL formula firstly. Public sub express and PoCTL model status are assigned in balance status of keeping model detecting space secondly. And finally, validation is proceeded to guarantee that PoCTL formula validation being first-passed with very high probability. The simulation shows that PM_LA could reduce time complexity and improve validation performance.