Search

Some Magic Tricks (MT), such as many kinds of Card Magic (CM), consisting of human computational or logical actions. How to ensure the logical correctness of these MTs? In this paper, the Model Checking (MC) technique is employed to study a typical CM via a case study. First, computational operations of a CM called shousuigongcishi can be described by a Magic Algorithm (MAR). Second, the logical correctness is portrayed by a temporal logic formula. On the basis of it, this MT logical correctness problem is reduced to the model checking problem. As a result, the Magic Trick Model Checking (MTMC) technique aims to verify whether a designed MT meets its architect's anticipation and requirements, or not, in terms of logic and computations., Comment: 2 figures, 1 table and 11 pages

How to accurately classify and diagnose whether an individual has Coronary Stenosis (CS) without invasive physical examination? This problem has not been solved satisfactorily. To this end, the four machine learning (ML) algorithms, i.e., Boosted Tree (BT), Decision Tree (DT), Logistic Regression (LR) and Random Forest (RF) are employed in this paper. First, eleven features including basic information of an individual, symptoms and results of routine physical examination are selected, as well as one label is specified, indicating whether an individual suffers from different severity of coronary artery stenosis or not. On the basis of it, a sample set is constructed. Second, each of these four ML algorithms learns from the sample set to obtain the corresponding optimal classified results, respectively. The experimental results show that: RF performs better than other three algorithms, and the former algorithm classifies whether an individual has CS with an accuracy of 95.7% (=90/94)., Comment: 6 pages, 3 figure, 4 tables

The existing core methods, which are employed by the popular CTL model checking tools, are facing the famous state explode problem. In our previous study, a method based on the Machine Learning (ML) algorithms was proposed to address this problem. However, the accuracy is not satisfactory. First, we conduct a comprehensive experiment on Graph Lab to seek the optimal accuracy using the five machine learning algorithms. Second, given the optimal accuracy, the average time is seeked. The results show that the Logistic Regressive (LR)-based approach can simulate CTL model checking with the accuracy of 98.8%, and its average efficiency is 459 times higher than that of the existing method, as well as the Boosted Tree (BT)-based approach can simulate CTL model checking with the accuracy of 98.7%, and its average efficiency is 639 times higher than that of the existing method., Comment: 5 pages, 1 figure

In this paper, we study how to predict the results of LTL model checking using some machine learning algorithms. Some Kripke structures and LTL formulas and their model checking results are made up data set. The approaches based on the Random Forest (RF), K-Nearest Neighbors (KNN), Decision tree (DT), and Logistic Regression (LR) are used to training and prediction. The experiment results show that the predictive accuracy of the RF, KNN, DT and LR-based approaches are 97.9%, 98.2%, 97.1% and 98.2%, respectively, as well as the average computation efficiencies of the RF, KNN, DT and LR-based approaches are 7102500, 598, 4132364 and 5543415 times than that of the existing approach, respectively, if the length of each LTL formula is 500., Comment: 6 pages, 3 figures

How to identify the comprehensive comparable performance of various Intrusion Detection (ID) algorithms which are based on the Model Checking (MC) techniques? To address this open issue, we conduct some tests for the model-checking-based intrusion detection systems (IDS) algorithms. At first, Linear Temporal Logic (LTL), Interval Temporal Logic (ITL) and Real-time Attack Signature Logic (RASL) are employed respectively to establish formula models for twenty-four types of attacks. And then, a standard intrusion set, called Intrusion Set for Intrusion Detection based on Model Checking (ISIDMC) is constructed. On the basis of it, detection abilities and efficiency of the intrusion detection algorithms based on model checking the three logics mentioned above are compared exhaustively, Comment: 34 pages, 18 figures, 26 tables

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., Comment: 13 pages, 7 figures

In DNA computing, it is impossible to decide whether a specific hybridization among complex DNA molecules is effective or not within acceptable time. In order to address this common problem, we introduce a new method based on the machine learning technique. First, a sample set is employed to train the Boosted Tree (BT) algorithm, and the corresponding model is obtained. Second, this model is used to predict classification results of molecular hybridizations. The experiments show that the average accuracy of the new method is over 94.2%, and its average efficiency is over 90839 times higher than that of the existing method. These results indicate that the new method can quickly and accurately determine the biological effectiveness of molecular hybridization for a given DNA design., Comment: 11 pages, 5 figures