# Experimental Study on CTL model checking using Machine Learning

## TL;DR

This paper explores machine learning techniques to improve CTL model checking by achieving high accuracy and significantly increasing efficiency, addressing the state explosion problem in existing tools.

## Contribution

It identifies optimal ML algorithms for CTL model checking, achieving near 99% accuracy and over 450 times efficiency improvement.

## Key findings

- LR-based approach achieves 98.8% accuracy
- BT-based approach achieves 98.7% accuracy
- Efficiency is 459 to 639 times higher than existing methods

## Abstract

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.