基于DNA计算的CTL模型检测方法研究

发布时间：2017-07-06 21:11

  本文关键词：基于DNA计算的CTL模型检测方法研究

  更多相关文章： 模型检测 计算树逻辑 DNA 计算

【摘要】：模型检测由图灵奖得主Clarke教授等人提出,是一种能够自动验证系统是否满足指定性质的技术,并且在系统不满足性质时提供反例,被广泛地应用于硬件验证、网络协议验证、安全协议验证、软件验证等领域,取得了令人瞩目的成果。另一方面,作为一种新的计算载体,DNA具有很高的信息存储密度和强大的并行处理能力,DNA计算为突破经典模型检测算法的效率限制提供了新的思路。2006年,著名的计算机科学家、图灵奖得主Ernest Allen Emerson首次把分子生物计算应用到模型检测领域,提出了一种用DNA分子对计算树逻辑(Computation Tree Logic,CTL)公式进行检测的方法。但是,Emerson教授只给出了一种CTL公式EFp的DNA检测算法,目前尚无其它基于DNA计算的CTL逻辑公式的检测算法,更没有DNA计算方法可以对全部的CTL逻辑公式进行检测。这是本文研究和要解决的问题。Emerson教授的方法存在一些不足之处:一,CTL公式EFp的DNA检测算法使用了DNA限制性内切酶和DNA连接酶,酶切反应和连接反应在同一生化环境中进行,对生化反应的环境要求苛刻,可靠性较低;二,当系统模型不满足公式EFp时,算法不能提供反例;三,只给出了一种CTL公式的检测方法,能够检测的公式类型单一。针对上述三个问题,首先,用带标签的有限状态自动机对系统建立模型;其次,探索合适的编码方式,用DNA分子编码系统模型;再次,经过研究和分析,把对系统模型的验证问题规约为对长度在阈值范围之内的运行的验证问题;然后,通过调用DNA分子的7种基本操作,给出了生成长度在阈值范围之内的运行的算法;最后,给出了4种CTL公式的DNA检测算法。对于公式EFp,新算法的反应试管中只含有一种核酸酶—DNA连接酶,对反应环境要求较低,可靠性较高;并且,当系统模型不满足公式时,新方法能给出反例;此外,新方法给出了另外三种公式的检测算法,能够检测的公式类型更多。新方法有效地弥补了Emerson方法中的不足。
【关键词】：模型检测 计算树逻辑 DNA 计算
【学位授予单位】：郑州大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TP38
【目录】：

• 摘要4-5
• ABSTRACT5-9
• 1 绪论9-24
• 1.1 研究背景与现状9-21
• 1.1.1 系统有效性证明9-11
• 1.1.2 模型检测11-17
• 1.1.3 DNA计算17-21
• 1.1.4 模型检测与DNA计算的关系21
• 1.2 当前存在的问题21-22
• 1.3 论文组织结构22-24
• 2 预备知识24-43
• 2.1 带标签的有限状态自动机24-26
• 2.2 CTL逻辑的语法和语义26-29
• 2.3 用CTL逻辑公式描述性质29
• 2.4 DNA基础知识29-34
• 2.4.1 DNA分子结构29-30
• 2.4.2 DNA操作技术30-34
• 2.5 DNA计算模型34-42
• 2.5.1 Adleman的首次实验34-37
• 2.5.2 分子模型检测37-40
• 2.5.3 粘贴系统40-41
• 2.5.4 粘贴自动机41-42
• 2.6 本章小结42-43
• 3 四种CTL公式的DNA检测算法43-51
• 3.1 与公式EGp、AGp、EFp和AFp相关的定理43-45
• 3.2 公式EGp、AGp、EFp和AFp的DNA检测算法45-49
• 3.2.1 生成集合X中的所有运行45-47
• 3.2.2 CTL公式EGp模型检测的DNA方法47-48
• 3.2.3 CTL公式AGp模型检测的DNA方法48
• 3.2.4 CTL公式EFp模型检测的DNA方法48-49
• 3.2.5 CTL公式AFp模型检测的DNA方法49
• 3.3 算法时间复杂度分析49-50
• 3.4 本章小结50-51
• 4 仿真实验51-57
• 4.1 实验环境与方法51-53
• 4.2 实验结果53-56
• 4.3 本章小结56-57
• 5 总结与展望57-58
• 5.1 总结57
• 5.2 展望57-58
• 参考文献58-63
• 个人简历、在学期间参加的科研项目及发表的论文63-64
• 致谢64-65

【参考文献】

中国期刊全文数据库 前5条

1 吴帆;李肯立;;基于自组装的N皇后问题DNA计算算法[J];电子学报;2013年11期

2 蒲飞;张文辉;;结合搜索空间划分和抽象进行LTL模型检测[J];中国科学(E辑:信息科学);2007年12期

3 徐亮;陈伟;徐艳艳;张文辉;;Improved Bounded Model Checking for the Universal Fragment of CTL[J];Journal of Computer Science & Technology;2009年01期

4 李肯立;罗兴;吴帆;周旭;黄鑫;;基于自组装模型的最大团问题DNA计算算法[J];计算机研究与发展;2013年03期

5 葛志磊;樊春海;YAN Hao;;DNA纳米自组装的研究进展及应用[J];科学通报;2014年02期

，

本文编号：527764