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

Survey on DNA-computing Based Methods of Computation Tree Logic Model Checking

作　　者：韩英杰[1] 周清雷[1] 朱维军[1] HAN Ying-jie;ZHOU Qing-lei;ZHU Wei-jun(School of Information Engineering,Zhengzhou University,Zhengzhou 450001,China)

机构地区：[1]郑州大学信息工程学院

出　　处：《计算机科学》2019年第11期25-31,共7页Computer Science

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

摘　　要：计算树逻辑(CTL)模型检测是保证系统正确性和可靠性的重要手段,但严峻的时空复杂性问题制约着CTL模型检测在工业界的应用。DNA计算的大规模并行性和DNA分子巨大的存储密度为解决CTL模型检测的时空复杂性问题提供了新思路。文中介绍了基于DNA计算的CTL模型检测的背景,并概述了基于DNA计算的CTL模型检测方法的基本原理。从检测能力的提升、自治化程度的提升和相关问题的解决这3个方面综述了方法的研究进展。在方法检测能力的提升方面,分3个层次综述了研究进展,即从只能检测单个CTL基本公式到能够检测一般公式,从只能检测带未来时间算子的CTL公式到能够检测带过去时间算子的CTL公式,从只能检测CTL公式到能够检测线性时序逻辑、投影时序逻辑和区间时序逻辑公式,表明了方法的检测能力在公式数量和种类上均有大幅提升;在方法自治化程度的提升方面,综述了从基于无记忆过滤模型的人工操作的非自治方法到基于粘贴自动机的分子自治下的自治方法的研究进展,表明基于DNA计算的CTL模型检测方法已实现高度自治化;在相关问题的解决方面,阐述了提升DNA分子特异性杂交有效性预测的效率和构建CTL公式的DNA表示等的研究进展。最后,指出了基于DNA计算的CTL模型检测在研究新方法、构建专用的DNA计算模型和扩展应用领域等方面的研究趋势。Computation tree logic(CTL)model checking is an important approach to ensuring the correctness and reliability of systems.However,the severe spatio-temporal complexity problems restrict the application of CTL model checking in industry.The large-scale parallelism of DNA computing and the huge storage density of DNA molecules provide new ideas for resolving the problems.The background and the principle of DNA-computing based methods of CTL model checking were introduced.The research progress was reviewed from three aspects:the improvement of power,the improvement of autonomy and the resolution of related problems.Firstly,the research progress of methods in terms of power was summarized from checking only one basic CTL-formula to general CTL-formulas,from CTL-formulas with only future operators to CTL-formulas with past-time operators,and from CTL-formulas to linear temporal logic,projection temporal logic and interval temporal logic formulas.Secondly,the research progress of methods in terms of autonomy from non-autonomous methods based on manual operations of memory-less filtering models to autonomous methods based on molecular autonomy of sticker automata was reviewed,showing that the methods are highly autonomous.At last,relevant problems in improving the predictive efficiency of specific hybridization of DNA molecules and constructing DNA molecules of CTL-formulas were described.In the end,corresponding research directions were discussed by concerning different methods,new models and new applications.

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

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