LTL Model Checking Based on Binary Classification of Machine Learning

• Main Authors: Weijun Zhu, Huanmei Wu, Miaolei Deng
• Format: Article
• Language: English
• Published: IEEE 2019-01-01
• Series: IEEE Access
• Subjects: Machine learning; model checking; linear temporal logic; binary classification
• Online Access: https://ieeexplore.ieee.org/document/8845603/

Linear Temporal Logic (LTL) Model Checking (MC) has been applied to many fields. However, the state explosion problem and the exponentially computational complexity restrict the further applications of LTL model checking. A lot of approaches have been presented to address these problems. And they work well. However, the essential issue has not been resolved due to the limitation of inherent complexity of the problem. As a result, the running time of LTL model checking algorithms will be inacceptable if a LTL formula is too long. To this end, this study tries to seek an acceptable approximate solution for LTL model checking by introducing the Machine Learning (ML) technique. And a method for predicting LTL model checking results is proposed, using the several ML algorithms including Boosted Tree (BT), Random Forest (RF), Decision tree (DT) or Logistic Regression (LR), respectively. First, for a number of Kripke structures and LTL formulas, a data set A containing model checking results is obtained, using one of the existing LTL model checking algorithm. Second, the LTL 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 given machine learning algorithm, where formulas and kripke structures are the two features, and model checking results are the one label. On the basis of it, a ML model M is obtained to predict the results of LTL model checking. As a result, an approximate LTL model checking technique occurs. The experiments show that the new method has the similar max accuracy with the state of the art algorithm in the classical LTL model checking technique, while the average efficiency of the former method is at most 6.3 million times higher than that of the latter algorithms, if the length of each of LTL formulas equals to 500. These results indicate that the new method can quickly and accurately determine LTL model checking result for a given Kripke structure and a given long LTL formula, since the new method avoids the famous state explosion problem.