Experimental Study on CTL model checking using Machine Learning
This addresses computational bottlenecks in formal verification for software/hardware engineers, though it appears incremental over prior ML-based work.
The paper tackles the state explosion problem in CTL model checking by optimizing machine learning approaches, achieving 98.8% accuracy with Logistic Regression (459× faster than existing methods) and 98.7% accuracy with Boosted Trees (639× faster).
The existing core methods, which are employed by the popular CTL model checking tools, are facing the famous state explode problem. In our previous study, a method based on the Machine Learning (ML) algorithms was proposed to address this problem. However, the accuracy is not satisfactory. First, we conduct a comprehensive experiment on Graph Lab to seek the optimal accuracy using the five machine learning algorithms. Second, given the optimal accuracy, the average time is seeked. The results show that the Logistic Regressive (LR)-based approach can simulate CTL model checking with the accuracy of 98.8%, and its average efficiency is 459 times higher than that of the existing method, as well as the Boosted Tree (BT)-based approach can simulate CTL model checking with the accuracy of 98.7%, and its average efficiency is 639 times higher than that of the existing method.