| |
| The computation using Deoxyribonucleic Acid (DNA) molecules provides a huge parallel way that break through the limitations of efficiency of traditional electronic computers. The Model checking is a popular formal verification technique which has been widely used in many fields of computations, and it is also a famous complex problem in the computing theory. Up to now, the branching-time logics seems hardly to be conducted model checking via DNA computing. To this end, Adleman's model based on DNA computing is employed in this paper. On the basis of it, a series of DNA-computing-based model checking algorithms for checking some basic formulas in a representative branching-time logic is proposed. As a result, a core of the DNA version of this model checking problem is solved in this way. The simulated experimental results show that the new algorithms are valid in computational logic, and they can be properly implemented in molecular biology. |
|
| Keywords:DNA Computing; Model Checking; Branching Time Logic; DNA Molecules |
|
