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.

[1] Abdelrazaq D., Abu-Soud S., and Awajan A., “A Machine Learning System for Distinguishing Nominal and Verbal Arabic Sentences,” The International Arab Journal of Information Technology, vol. 15, no. 3A, pp. 576-584, 2018.

[2] Abe T., Ugawa T., and Maeda T., “Reordering Control Approaches to State Explosion in Model Checking with Memory Consistency Models,” in Proceedings of Working Conference on Verified Software: Theories, Tools, and Experiments, Heidelberg, pp. 170-190, 2017.

[3] Apple Incorporation, “apple/turicreate: Turi Create simplifies the development of custom machine learning models,” Retrieved from: https://github.com/apple/turicreate/, Last Visited, 2020.

[4] Attie A., “Synthesis of Large Dynamic Concurrent Programs from Dynamic Specifications,” Formal Methods in System Design, vol. 48, no. 1-2, pp. 94-147, 2016.

[5] Ball T., Cook B., Levin V., and Rajamani S., “SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsof,” in Proceedings of International Conference on Integrated Formal Methods, Canterbury, pp 1-20, 2004.

[6] Behjati R., Sirjani M., and Ahmadabadi M., “Bounded Rational Search for on-the-Fly Model Checking of LTL Properties,” in Proceedings of International Conference on Fundamentals of Software Engineering, Kish Island, pp. 292-307, 2009.

[7] Belzner L. and Gabor T., “Bayesian Verification under Model Uncertainty,” in Proceedings of EEE/ACM 3rd International Workshop on Software Engineering for Smart Cyber-Physical Systems, Buenos Aires, pp. 10-13, 2017.

[8] Benari-Ari M., Pnueli A., and Manna Z., “The Temporal Logic of Branching Time,” Acta Informatica, vol. 20, no. 3, pp. 207-226, 1983.

[9] Benjamin B., Marco B., Roberto C., Alessandro C., Michele D., Marco G., Alberto G., Ahmed I., Cristian M., Andrea M., Sergio M., Marco R., Mirko S., Stefano T., Gianni Z.,“The Nuxmv Model Checker,” FBK, https://es-static.fbk.eu/tools/nuxmv/, Last Visited, 2020.

[10] Bortolussi L., Milios D., and Sanguinetti G., “Machine Learning Methods in Statistical Model Checking and System Design-Tutorial,” in Proceedings of 6th International Conference Runtime Verification, Vienna, pp. 323-341, 2015.

[11] Bortolussi L. and Sanguinetti G., “Learning And Designing Stochastic Processes from Logical Constraints,” in Proceedings of International Conference on Quantitative Evaluation of Systems, Buenos Aires, pp. 89-105, 2013.

[12] Bortolussi L. and Silvetti S., “Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models,” in Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, pp. 396-413, 2018.

[13] Brázdil T., Chatterjee K., Chmelík M., Forejt V., Křetínský J., Kwiatkowska M., Parker D., and Ujma M., “Verification of Markov Decision Processes using Learning Algorithms,” in Proceedings of International Symposium on Automated Technology for Verification and Analysis, Sydney, pp. 98-114, 2014.

[14] Clarke E., “Model Checking: My 30 Year Quest to Conquer the State Explosion Problem,” Retrieved from: http://www.cs.cmu.edu/~emc/15414-f11/lecture/l ec27_MC.pdf, Last Visited, 2020.

[15] Clarke E., “Model Checking Overview,” Retrieved from: http://www.cs.cmu.edu/~emc/15-398/lectures/ove rview.pdf, Last Visited, 2020.

[16] Clarke E. and Emerson E., “Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic,” in Proceedings of Workshop on Logic of Programs, Yorktown Heights, pp. 52-71, 1981.

[17] Clarke E., Khaira M., and Zhao X., “Word Level Model Checking-Avoiding the Pentium FDIV Error,” in Proceedings of 33rd Design Automation Conference Proceedings, Las Vegas, pp. 645-648, 1996.

[18] Clarke E., Klieber W., Nováček M., and Zuliani P., Tools for Practical Software Verification, Springer Link, 2012.

[19] Dobrikov I. and Leuschel M., “Optimising The Prob Model Checker for B Using Partial Order Reduction,” Formal Aspects of Computing, vol. 28, no. 2, pp. 295-323, 2016.

[20] Dutra A., “Software Model Checking: CTL Model Checking Based on Binary Classification of Machine Learning 259 High-Assurance Software Design,” NASA, Retrieved from: https://ti.arc.nasa.gov/tech/rse/vandv/software-m odel-checking/, Last Visited, 2020.

[21] Elkader K., Grumberg O., Pas˘areanu˘ C., and Shoham S., “Automated Circular Assume-Guarantee Reasoning,” Formal Aspects of Computing, no. 30, pp. 571-595, 2018.

[22] Emerson E. and Clarke E., “Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons,” Science of Computer Programming, vol. 2, no. 3, pp. 241-266, 1982.

[23] Emerson E., Hager K., and Konieczka J., “Molecular Model Checking,” International Journal of Foundations of Computer Science, vol. 17, no. 04, pp. 733-742, 2006.

[24] Fabian P., Gaël V., Alexandre G., Vincent M., Bertrand T., Olivier G., Mathieu B., Peter P., Ron W., Vincent D., Jake V., Alexandre P., David C., Matthieu B., Matthieu P., Édouard D., “Scikit-Learn: Machine Learning in Python,” retrieved from: https://scikit-learn.org/stable/, Last Visited, 2021.

[25] Groefsema H., Van-Beest N., and Aiello M., “A Formal Model for Compliance Verification of Service Compositions,” IEEE Transactions on Services Computing, vol. 11, no. 3, pp. 466-479, 2016.

[26] Haim S. and Walsh T., “Restart Strategy Selection Using Machine Learning Techniques,” in Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, Swansea, pp. 312-325, 2009.

[27] Halleux P., Rajamani S., Ball T., and Hoare T., Microsoft Research, “SLAM,” Retrieved from: https://www.microsoft.com/en-us/research/projec t/slam/, Last Visited, 2020.

[28] Kojima H., Nagashima Y., and Tsuchiya T., “Model Checking Techniques for State Space Reduction in Manet Protocol Verification,” in Proceedings of IEEE International Parallel and Distributed Processing Symposium Workshops, Chicago, pp. 509-516, 2016.

[29] Liang J., Ganesh V., Poupart P., and Czarnecki K., “Learning Rate Based Branching Heuristic for SAT Solvers,” in Proceedings of International Conference on Theory and Applications of Satisfiability Testing, Bordeaux, pp. 123-140, 2016.

[30] Liang J., Oh C., Mathew M., Thomas C., Li C., and Ganesh V., “Machine Learning-Based Restart Policy for CDCL SAT Solvers,” in Proceedings of International Conference on Theory and Applications of Satisfiability Testing, Oxford, pp. 94-110, 2018.

[31] Musuvathi M., Park D., Chou A., Engler D., and Dill D., “CMC: A Pragmatic Approach to Model Checking Real Code,” ACM SIGOPS Operating Systems Review, vol. 36, pp. 75-88, 2002.

[32] Pedro A., Crocker P., and Simão M., “Learning Stochastic Timed Automata from Sample Executions,” in Proceedings of International Conference on Leveraging Applications of Formal Methods, Heraklion, pp. 508-523, 2012.

[33] Pnueli A., “The Temporal Logic of Programs,” in Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Providence, pp. 46-57, 1977.

[34] Ročkai P., Barnat J., and Brim L., “Improved State Space Reductions for LTL Model Checking of C and C++ Programs,” in Proceedings of NASA Formal Methods Symposium, Moffett Field, pp. 1-15, 2013.

[35] Sack H., SciHi BlogSciHi Blog, “The Pentium FDIV Bug,” Retrieved from: http://scihi.org/the-pentium-fdiv-bug/, Last Visited, 2015.

[36] Sanguinetti G ., “Machine Learning Methods for Model Checking in Continuous Time Markov Chains,” https://www.cs.ox.ac.uk/seminars/1195.html, Last Visited, 2020.

[37] Tulsian V., Kanade A., Kumar R., Lal A., and Nori A., “MUX: Algorithm Selection for Software Model Checkers,” in Proceedings of the 11th Working Conference on Mining Software Repositories, New York, pp. 132-141, 2014.

[38] Zheng H., Zhang Z., Myers C., Rodriguez E., and Zhang Y., “Compositional Model Checking of Concurrent Systems,” IEEE Transactions on Computers, vol. 64, no. 6, pp. 1607-1621, 2015.

[39] Zhu W., Feng C., and Wu H., “Model Checking Temporal Logic Formulas Using Sticker Automata,” BioMed Research International, 2017.

[40] Zhu W., Han Y., and Zhou Q., “Performing Ctl Model Checking Via Dna Computing,” Soft Computing, vol. 23, no.12, pp. 3945-3963, 2019.

[41] Zhu W., Wu H., and Deng M., “LTL Model Checking Based on Binary Classification of Machine Learning,” IEEE Access, vol. 7, pp. 135703-135719, 2019.

[42] Zhu W., Zhou Q., and Zhang Q., “A LTL Model Checking Approach Based on DNA Computing,” Chinese Journal of Computers, vol. 39, no. 12, pp. 2578-2597, 2016.