作者：朱维军; 周清雷; 张钦宪模型检测脱氧核糖核酸线性时序逻辑粘贴自动机有穷状态自动机dna计算
摘要：该文研究基于脱氧核糖核酸（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一般公式的（理论）检测能力.
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
