Research On Method Of CTL Model Checking Based On DNA Computing

Model Checking was proposed by Clarke who is a Turing award winner and some other people. Model Checking is a technology that can verify whether a system satisfies the given property automatically, and when the system does not satisfy the given property, it can provide counter-examples. Model Checking is widely used in the fields of hardware verification、network protocol verification、security protocol verification、software verification et al, and has made remarkable achievements. On the other hand, as a new computing carrier, DNA has a high storage density and powerful parallel processing capabilities, DNA computing provides a new way of thinking to breakthrough the efficiency limit of classic model checking algorithm.In 2006, Ernest Allen Emerson, the famous computer scientist and the Turing award winner, applied DNA computing into Model Checking for the first time. He proposed a new Computation Tree Logic(CTL)Model Checking method which used DNA molecules. But, Emerson only given checking method of one CTL formula, there is no other CTL model checking method based on DNA computing now, but no DNA computing method can do CTL model checking completely, and this is the main problem that the paper to study and solve.There are some deficiences of professor Emerson’s method: Firstly, DNA checking method of CTL formula EFp uses DNA ligase and DNA restriction enzyme, digestion reaction and ligation reaction carried out in the same biochemical environment, so this method demand a restrict biochemical reaction environment, and it’s reliability is low; Secondly, when the system model does not satisfy the formula EFp, the method can not give counter-examples; Finally, Emerson only gives checking method of one type of CTL formula, and can only check a single type of CTL formula. In response to these three problems, firstly, use finite state automata modeling system; Secondly, explore appropriate encoding, use DNA encoding system model; Thirdly, through study and research, convert system’ checking problem to the checking problem of runs who’ length are in the range of a threshod; Then, by calling DNA’ seven kinds of basic operations, give the algorithm to generate the run who’ length are in the range of a threshod; And finally, give four types of CTL formula’ DNA detection algorithms.For formula EFp, The new algorithm uses only one enzyme-DNA ligase, so it’s requirements of reaction environment is low, but has high reliability; And when system model does not satisfy formula, the new method can give counter-examples. Further more, new method gives the other three types of formulas’ detection algorithms, it can check more types of CTL formula. Therefore, new method improves deficiencies of Emerson’s method effectively.