| |
| The state explosion problem restrict the further applications of Computational Tree LogicCTL model checking. To this end, this study tries to seek an acceptable approximate solution for CTL model checking by introducing the Machine Learning (ML) technique, and a method for predicting results of CTL model checking via the Boosted Tree (BT) algorithm is proposed in this paper. First, for a number of Kripke structures and CTL formulas, a data set A containing model checking results is obtained, using the existing CTL model checking algorithm. Second, the CTL model checking problem can be induced to a binary classification problem of machine learning. As a result, an approximate CTL model checking technique occurs. The experiments show that the new method has the average accuracy of 96%, and its average efficiency is 210 times higher than that of the representative model checking method, if the length of each of CTL formulas equals to 500.These results indicate that the new method can quickly and accurately determine results of CTL model checking for a given Kripke structure and a given long CTL formula since the new method avoid the famous state explosion problem. |
|
| Keywords:Machine Learning; Boosted Tree; Model Checking; Computational Tree Logic; Kripke Structure |
|
