以DNA为载体的线性时序逻辑模型检测  

Conduct Linear Temporal Logic Model Checking via DNA Molecules

作　　者：朱维军[1] 周清雷[1] 李永亮[1] 

机构地区：[1]郑州大学信息工程学院,河南郑州450001

出　　处：《电子学报》2016年第6期1265-1271,共7页Acta Electronica Sinica

基　　金：国家自然科学基金(No.61250007;No.U1204608;No.U1304606;No.61572444);中国博士后科学基金(No.2012M511588;No.2015M572120);河南省高等学校青年骨干教师资助计划项目(No.2014GGJS-001)

摘　　要：线性时序逻辑模型检测被广泛应用于处理器设计与验证、网络协议验证、安全协议验证等领域.然而到目前为止,该技术只能在电子计算的平台上实现.为了以脱氧核糖核酸(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.

关 键 词：模型检测 脱氧核糖核酸 线性时序逻辑 粘贴自动机 

分 类 号：TP301[自动化与计算机技术—计算机系统结构] TP384[自动化与计算机技术—计算机科学与技术]