使用多种机器学习算法预测CTL模型检测
首发时间:2019-01-11
摘要:计算树逻辑(CTL)模型检测现已应用在多个领域。然而,状态爆炸问题限制了计算树逻辑模型检测的进一步应用。研究人员已经提出了许多方法来解决这些问题。但是,由于该问题本身固有的复杂性的限制,在传统的模型检测技术框架内,根本问题难以被有效解决。我们的前期工作使用BT算法来预测CTL模型检测,取得了准确率轻微下降而效率大幅提高的结果。采用其他机器学习算法是否可以获得更加准确更加快速的CTL模型检测预测结果?为此,本文又使用了另外四种机器学习方法。首先,对于一些Kripke结构和CTL公式,使用CTL模型检测算法获得包含模型检测结果的数据集A。其次,CTL模型检测问题可以归结为机器学习的二元分类问题。换句话说,A中的一些记录作为随机森林(Random Forest,RF)算法、逻辑回归(Logistic Regression,LR)算法、决策树(Decision Tree,DT)算法和支持向量机(Support Vector Machine,SVM)算法的训练集,并且获得相应的机器学习模型M,利用M来预测CTL模型检测的结果。实验表明,基于RF方法的平均准确率为95.6%,基于LR方法的平均准确率为91.1%,基于DT方法的平均准确率为95.1%,基于SVM方法的平均准确率为94.9%。而且,基于RF方法的平均效率比传统的模型检测方法的平均效率高122倍,基于LR方法的平均效率比传统的模型检测方法的平均效率高113倍,基于DT方法的平均效率比传统的模型检测方法的平均效率高81倍,基于SVM方法的平均效率比传统的模型检测方法的平均效率高91倍。这些结果表明,使用RF机器学习预测CTL模型检测结果,可以达到良好的准确预测效果。
For information in English, please click here
Predicting the Results of CTL Model Checking using Multiple Machine Learning Algorithms
Abstract:Computational Tree Logic (CTL) model checking has been applied to many fields. However, the state explosion problem restricts the further applications of CTL model checking. A lot of approaches have been presented to address these problems. However, the essential issue has not been resolved due to the limitation of the inherent complexity of the problem. We used the BT algorithm to predict CTL model detection and achieved a result that BT-based approach has a significant increase in efficiency with a slight decrease in accuracy,in our preliminary work. Can other machine learning algorithms obtain more accurate and faster result when used in CTL model detection prediction results? To this end, we use another four machine learning methods in this paper. First, for a number of Kripke structures and CTL formulas, a data set A containing model checking results are 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. In other words, some records in A form a training set for the Random Forest (RF) algorithm, Logistic Regression (LR) one, Decision Tree (DT) one and Support Vector Machine (SVM) one, and the corresponding model is obtained. On the basis of it, a ML model M is obtained to predict the results of CTL model checking. The experiments show that the RF-based one has the average accuracy of 95.6%, the LR-based one has the average accuracy of 91.1%, the DT-based one has the average accuracy of 95.1%, and the SVM-based one has the average accuracy of 94.9%. Furthermore, the average efficiency of the RF-based approach is 112 times higher than that of the existing one, the average efficiency of the LR-based approach is 113 times higher than that of the existing one, the average efficiency of the DT-based approach is 81 times higher than that of the existing one, and the average efficiency of the SVM-based approach is 91 times higher than that of the existing one. These results indicate that RF-based approach have a good prediction effect in determining the results of CTL model checking.
Keywords: Machine Learning Model Checking Computational Tree Logic Kripke Structure
引用
No.****
同行评议
勘误表
使用多种机器学习算法预测CTL模型检测
评论
全部评论0/1000