基于DNA计算的线性时序逻辑模型检测方法  

A LTL Model Checking Approach Based on DNA Computing

作　　者：朱维军[1] 周清雷[1] 张钦宪[2] 

机构地区：[1]郑州大学信息工程学院,郑州450001 [2]郑州大学基础医学院,郑州450001

出　　处：《计算机学报》2016年第12期2578-2597,共20页Chinese Journal of Computers

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

摘　　要：该文研究基于脱氧核糖核酸(Deoxyribonucleic Acid,DNA)计算的线性时序逻辑(Linear Temporal Logic,LTL)模型检测问题.为此,该文给出了使用粘贴自动机实现LTL模型检测的方法.首先,使用3′-5′型单链DNA分子对LTL公式的有穷状态自动机(Finite State Automata,FSA)模型进行编码,从而获得实现公式的粘贴自动机;其次,使用5′-3′型单链DNA分子对系统模型进行编码,从而获得粘贴自动机的输入字符串;最后,对表征粘贴自动机的DNA单链分子和表征输入字符串的DNA单链分子实施一系列生化反应,即可判定系统是否满足公式.分子生物学仿真实验结果表明:给出的DNA编码序列能达到99.9%的碱基配对正确率,且新方法成功地对所有4种LTL基本公式与5种LTL常见公式实施了检测;与之对照,已有的方法只能有效检测1种LTL基本公式与0种LTL常见公式.在此基础上,对本实验给出的DNA编码方案直接作位数扩展即可拥有对任意给定LTL一般公式的(理论)检测能力.This paper investigates the Linear Temporal Logic （LTL） model checking problem under the circumstance of Deoxyribonucleic Acid （DNA） computing. To address this problem, we presented a method for checking LTL formulas via some sticker automata. Firstly, 3′-5′ single-stranded DNA molecules are applied to encoding a Finite State Automaton （FSA） model for the given LTL formula, so that a sticker automata which is a DNA model of the formula can be obtained. Secondly, the given system model is encoded by 5′-3′ single-stranded DNA molecules, by which the input strings of sticker automata can be generated. Finally, a series of biochemical reactions are implemented on the single-stranded DNA molecules characterizing sticker automata or input strings, in order to determine whether the system meets the formula or not. The experimental results show that the generated DNA coding sequences achieve in 99.9% by accuracy for base pairing. Furthermore, the proposed method successfully checks four kinds of basic LTL formulas and five kinds of popular LTL formulas, whereas the existing methods can only check one kind of basic LTL formula and none popular LTL formula, as shown in the experiments. By extending more bits on presented DNA encoding scheme, the proposed method can check any given LTL formulas theoretically.

关 键 词：模型检测 脱氧核糖核酸 线性时序逻辑 粘贴自动机 有穷状态自动机 DNA计算 

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