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.
翻译:在本文中,我们研究如何利用一些机器学习算法预测LTL模型检查的结果。一些Kripke结构和LTL公式及其模型检查结果由数据集组成。基于随机森林(RF)、K-Nearest邻居(KNN)、决定树(DT)和物流回归(LR)的方法被用于培训和预测。实验结果表明,如果每个LTL公式的长度为500,RF、KNN、DT和LLM方法的预测准确性分别为97.9%、98.2%、97.1%和98.2%,以及RF、KNN、DT和LR方法的平均计算效率分别为7102 500、598、4132364和5543415倍。