  The state explosion problem and the exponentially computational complexity
restrict the further applications of LTL model checking. 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
results of LTL model checking via the Boosted Tree (BT) algorithm is proposed
in this paper. First, for a number of Kripke structures and LTL formulas, a
data set A containing their model checking results is obtained, using 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 BT algorithm. 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 average accuracy of 98.0%, and its
average efficiency is 9.4 million times higher than that of the representative
model checking method, if the length of each of LTL formulas equals to 500.
