基于DNA计算的计算树逻辑模型检测方法研究进展

摘要：

计算树逻辑(CTL)模型检测是保证系统正确性和可靠性的重要手段,但严峻的时空复杂性问题制约着CTL模型检测在工业界的应用.DNA计算的大规模并行性和DNA分子巨大的存储密度为解决CTL模型检测的时空复杂性问题提供了新思路.文中介绍了基于DNA计算的CTL模型检测的背景,并概述了基于DNA计算的CTL模型检测方法的基本原理.从检测能力的提升、自治化程度的提升和相关问题的解决这3个方面综述了方法的研究进展.在方法检测能力的提升方面,分3个层次综述了研究进展,即从只能检测单个CTL基本公式到能够检测一般公式,从只能检测带未来时间算子的CTL公式到能够检测带过去时间算子的CTL公式,从只能检测CTL公式到能够检测线性时序逻辑、投影时序逻辑和区间时序逻辑公式,表明了方法的检测能力在公式数量和种类上均有大幅提升;在方法自治化程度的提升方面,综述了从基于无记忆过滤模型的人工操作的非自治方法到基于粘贴自动机的分子自治下的自治方法的研究进展,表明基于DNA计算的CTL模型检测方法已实现高度自治化;在相关问题的解决方面,阐述了提升DNA分子特异性杂交有效性预测的效率和构建CTL公式的DNA表示等的研究进展.最后,指出了基于DNA计算的CTL模型检测在研究新方法、构建专用的DNA计算模型和扩展应用领域等方面的研究趋势.

关键词：模型检测、计算树逻辑、DNA分子、分子计算

所属期刊栏目：46

分类号：TP301;TP384(计算技术、计算机技术)

资助基金：国家自然科学基金项目61572444

在线出版日期：2019-12-13（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：25-31