Research On Computation Tree Logic Model Checking Algorithms Based On DNA Computing Models

Computation tree logic(CTL)model checking is a formal verification technology that can ensure the correctness of systems.Deoxyribonucleic acid(DNA)computing is a novel computational paradigm that uses DNA molecules and biological enzymes as the materials and applies biochemical reactions as computational means.Studying CTL model checking algorithms based on DNA computing can not only solve the problem of state space explosion,but also have great significance for the development of DNA computers.Since the Turing Award winner Professor Emerson raised the problem of DNA model checking,the problem of CTL model checking has not been completely solved.Moreover,existing algorithms leave the following problems unsettled,including failure to provide counter-examples,inability to check general CTL formulas and CTL with past-time operator(CTLP)formulas,inability to achieve it in cells,and weak robustness and nonreusable reactive material caused by using nucleases.Aiming at the above problems,this paper studies CTL model checking algorithms based on the non-autonomous,autonomous and intracellular DNA computing models.The main research contents and innovations are as follows:1)A non-autonomous algorithm for CTL model checking(AM-CTLMC)is proposed.First,a DNA encoding scheme for a to-be-checked system model is designed,and a DNA algorithm for generating paths of the system model is constructed.Second,DNA algorithms for checking basic,general and CTLP formulas are proposed.Last,the validity of the algorithms is verified by simulations.The proposed algorithms settle the problem that counter-examples can't be provided when the system model does not satisfy a CTL formula,and solve the model checking problem for general and CTLP formulas which can't be checked before.At the same time,the robustness and the reusability of reaction material are guaranteed without using nucleases.2)Two autonomous DNA computing algorithms for CTL model checking are proposed,namely the molecular beacon-based algorithm(MB-CTLMC)and the length-encoding automaton-based algorithm(LEA-CTLMC).First,a self-assembly encoding scheme for a to-be-checked system model is designed and encoding schemes of molecular beacons and length-coding automata for a basic CTL formula are constructed.Second,the molecular self-assembly environment of the system paths and the basic CTL formula are studied and the self-assembly algorithms based on molecular beacons and length-encoding automata are presented.Last,the validity of the algorithms is verified by simulations and experiments.These algorithms solve the problems of weak robustness and non-reusable reactive materials.At the same time,LEA-CTLMC has scalability in implementing temporal logic model checking due to programmability and generality.3)An intracellular algorithm for CTL model checking(IN VIVO-CTLMC)is proposed.First,a messenger ribonucleic acid(m RNA)encoding scheme for paths of a system model and a transfer RNA(t RNA)encoding scheme for a finite state automaton of a basic CTL formula are designed.Second,the m RNAs and the t RNAs are inserted into plasmids,and the plasmids are transfected into E.coli cells,where model checking is performed by an autonomous protein synthesis mechanism.Last,the validity of the algorithm is proved.The proposed algorithm solves the problem of lacking intracellular CTL model checking algorithms,and explores dynamic,intelligent,and accurate methods for diagnosis and treatment of genetic diseases at the molecular level.4)A method for analyzing the effectiveness of DNA molecular hybridization based on machine learning is proposed.First,a data set for analyzing the effectiveness of DNA molecular hybridization is constructed,and four machine learning algorithms including gradient boosting trees(GBDT),logistic regression,support vector machine and random forests are chosen according to preliminary experiments.Second,the four classifiers are trained using the data set.According to the performance indexes,the classifier based on GBDT is selected as the core of the method.Last,the results of a comparative experiment show that the F1 value of the method based on GBDT is 0.1% lower than that of NUPACK,but the efficiency is 142,013 times higher.Furthermore,the analysis time does not change on the order of magnitude as the number of single-stranded DNA molecules involved in the hybridization increases.This method solves the problem of low efficiency,and provides an alternative tool for analyzing the effectiveness of DNA molecular hybridization.