arXiv subjects

Weijun Zhu

Publications and source records attributed to Weijun Zhu.

11 recordsLinked to original sources

arXiv2024

Model Checking Logical Actions in Magic Tricks

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.

cs.LO↗

arXiv2021

Auxiliary Diagnosing Coronary Stenosis Using Machine Learning

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).

q-bio.TO↗

arXiv2019

Predicting the Results of LTL Model Checking using Multiple Machine Learning Algorithms

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.

cs.LO↗

arXiv2019

Approximate LTL model checking

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.

cs.LO↗

arXiv2018

Analyzing DNA Hybridization via machine learning

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.

q-bio.QM↗

arXiv2018

On the model-checking-based IDS

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

cs.CR↗

arXiv2018

Some Issues on the Theory of the Mimic-Computing-Oriented Automata

A mimic computing oriented automaton can directly portray the behaviors of a mimic computing system. In this paper, we investigate the following theoretical problems on this type of automata: operational semantics and computational ability. First, we model a systematic structure of mimic computing via a mimic automaton. Second, we propose the operational semantics of the automaton in this scene. Third, the computational ability of this type of automata is studied.

cs.FL↗

arXiv2017

Aiming to Detect a malware of GSM frequency

In order to find a specific type of malware which is related to GSM frequency, we propose an algorithm according to the most essential characteristics of this malware. At first, detect whether or not there exists a specific thread in the memory. And then, the generated binary strings will be tried to be matched with the one in the target computer. At last, determine whether this threat occurs or not. Furthermore, we study the effective of the new method via some simulations.

cs.CR↗

arXiv2017

A novel type of Automata for dynamic, heterogeneous and random architectures

In this paper, the author aims to establish a mathematical model for a mimic computer. To this end, a novel automaton is proposed. First, a one-dimensional cellular automaton is used for expressing some dynamic changes in the structure of a computing unit, a sequential automaton is employed to describe some state transitions, a hierarchical automaton is employed to express the different granularities of some computing units, and a probabilistic automaton is used to depict some random changes of a computing unit. Second, the new automaton is obtained by combining the various types of automata mentioned above in the certain logical relationship. To the best of our knowledge, the new automaton model is the first automaton which can portray the operation semantics for a mimic computing system, and it can directly describe some behaviors of a mimic computer.

cs.FL↗

arXiv2017

Molecular Model Checking a Temporal Logic

The molecular computing has been successfully employed to solve more and more complex computation problems. However, as an important complex problem, the model checking are still far from fully resolved under the circumstance of molecular computing, since it is still a lack of method. To address this issue, a model checking method is presented for checking the basic constructs in a given temporal logic using molecular computing. Through the design of the new encoding and calling this process, we get a molecule-based approach for checking all of the basic constructs of this logic.

cs.LO↗

arXiv2005

Antenna array geometry and coding performance

This paper provides details about experiments in realistic, urban, and frequency flat channels with space-time coding that specifically examines the impact of the number of receive antennas and the design criteria for code selection on the performance. Also the performance characteristics are examined of the coded modulations in the presence of finite size array geometries. This paper gives some insight into which of the theories are most useful in realistic deployments.

cs.IT↗