该文研究基于脱氧核糖核酸(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一般公式的(理论)检测能力.
模型检测、脱氧核糖核酸、线性时序逻辑、粘贴自动机、有穷状态自动机、DNA计算
39
TP301;TP384(计算技术、计算机技术)
国家自然科学基金61250007,U1204608,U1304606,61373043,61572444;中国博士后科学基金2012M511588,2015M572120;河南省高等学校青年骨干教师资助计划2014GGJS-001资助.This work is supported by the National Natural Science Foundation of China under Grant No.61250007,No.U1204608,No.U1304606,No.61373043,No.61572444,and the China Postdoctoral Science Foundation under Grant No.2012M511588,No.2015M572120,as well as F