An Approximate CTL Model Checking Approach

The state space explosion is the main bottleneck of Computational Tree Logic (CTL) model checking. In the framework of traditional model checking technique, this problem is difficult to be solved completely. To this end, a method is proposed for predicting the results for CTL model checking using several Machine Learning (ML) algorithms. First, the data set with a number of Kripke structures, CTL formulas and their model checking results are obtained, using the existing CTL model checking tool. Second, Random Forest (RF), Boosted Trees (BT), Decision Trees (DT) and Logistic Regression (LR) algorithms are employed to train the data set. On the basis of it, the four ML models are obtained to predict the results of CTL model checking. The experiments show that the best accuracy of the new method is same as the existing CTL model checking methods, and its average efficiency is 378 times higher than that of the existing method, if the length of each of CTL formulas equals to 500.