Conduct Linear Te mporaI Logic ModeI Checking via DNA MoIecuIes

摘要

The linear temporal logic (LTL)model checking is widely used in processor design and verification,net-work protocol verification and security protocol verification.Up to now,this technique can only be realized on the platform of electronic computer.In order to conduct LTL model checking under the circumstance of deoxyribo nucleic acid (DNA), we proposed a method to check the Until constructor via a sticker automaton.We encode a finite state automaton (FSA) which is a model of the formula Until,with a DNA sticker automaton.And we convert a model of a system into its paths,as the input strings of the sticker automaton.We verify whether the system satisfies the formula or not,by using the sticker au-tomaton.In this way,the formula Until can be checked with the double strand DNA molecules.The simulation results show that the method can successfully check the basic temporal formulas.

关键词