# Predicting the Results of LTL Model Checking using Multiple Machine Learning Algorithms

## TL;DR

This paper explores machine learning techniques like RF, KNN, DT, and LR to accurately predict LTL model checking results, significantly improving efficiency over traditional methods.

## Contribution

It introduces a novel approach using multiple ML algorithms to predict LTL model checking outcomes with high accuracy and efficiency.

## Key findings

- Random Forest achieved 97.9% accuracy
- K-Nearest Neighbors achieved 98.2% accuracy
- ML-based approaches vastly outperformed existing methods in computation efficiency

## Abstract

In this paper, we study how to predict the results of LTL model checking using some machine learning algorithms. Some Kripke structures and LTL formulas and their model checking results are made up data set. The approaches based on the Random Forest (RF), K-Nearest Neighbors (KNN), Decision tree (DT), and Logistic Regression (LR) are used to training and prediction. The experiment results show that the predictive accuracy of the RF, KNN, DT and LR-based approaches are 97.9%, 98.2%, 97.1% and 98.2%, respectively, as well as the average computation efficiencies of the RF, KNN, DT and LR-based approaches are 7102500, 598, 4132364 and 5543415 times than that of the existing approach, respectively, if the length of each LTL formula is 500.