CTL Model Checking Based on Binary Classification of Machine Learning
|
Weijun Zhu School of Computer and Artificial Intelligence Zhengzhou University, China This email address is being protected from spambots. You need JavaScript enabled to view it. |
Huanmei Wu College of Public Health Temple University, USA This email address is being protected from spambots. You need JavaScript enabled to view it. |
Abstract: In this study, we establish and pioneer an approximate Computational Tree Logic (CTL) Model Checking (MC) technique, in order to avoid the famous State Explosion (SE) problem in the Computational Tree Logic Model Checking (CTLMC). To this end, some Machine Learning (ML) algorithms are introduced and employed. On this basis, CTL model checking is induced to binary classification of machine learning, by mapping all the two different results of CTL model checking into all the two different results of binary classification of machine learning, respectively. The experimental results indicate that the newly proposed approach has a maximal accuracy of 100% on our randomly generated data set, compared with the latest algorithm in the classical CTL model checking. Furthermore, the average speed of the new approach is at most 120 thousand times higher than that of the latest algorithm, which appears in the current version of a popular model checker called NuXMV, in the classical CTL model checking. These observations prompt that the new method can get CTL model checking results quickly and accurately, since the SE problem is avoided completely.
Keywords: Model checking, computational tree logic, machine learning, binary classification.
Received October 10, 2020; accepted October 14, 2021