中文摘要：

线性时序逻辑模型检测被广泛应用于处理器设计与验证、网络协议验证、安全协议验证等领域.然而到目前为止,该技术只能在电子计算的平台上实现.为了以脱氧核糖核酸（Deoxyribo Nucleic Acid,DNA）为载体对线性时序逻辑（Linear Temporal Logic,LTL）实施模型检测,给出了使用粘贴自动机实现Until算子模型检测的方法.首先,使用粘贴自动机对Until公式的有穷状态自动机（Finite State Automata,FSA）模型进行编码;然后,将系统模型转换为粘贴自动机的输入字符串;最后,用粘贴自动机验证系统是否满足公式.仿真实验结果证实,新方法可实现对LTL逻辑时序算子的检测.

英文摘要：

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.