LTL model checking based on binary classification of machine learning

Weijun Zhu, Huanmei Wu, Miaolei Deng

Research output: Contribution to journalArticlepeer-review

Abstract

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.

Original languageEnglish (US)
Article number8845603
Pages (from-to)135703-135719
Number of pages17
JournalIEEE Access
Volume7
DOIs
StatePublished - 2019

Keywords

  • Binary classification
  • Linear temporal logic
  • Machine learning
  • Model checking

ASJC Scopus subject areas

  • Computer Science(all)
  • Materials Science(all)
  • Engineering(all)

Fingerprint Dive into the research topics of 'LTL model checking based on binary classification of machine learning'. Together they form a unique fingerprint.

Cite this