计算机科学 ›› 2019, Vol. 46 ›› Issue (11): 25-31.doi: 10.11896/jsjkx.181102091

• 综述 • 上一篇    下一篇

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

韩英杰, 周清雷, 朱维军   

  1. (郑州大学信息工程学院 郑州450001)
  • 收稿日期:2018-11-14 出版日期:2019-11-15 发布日期:2019-11-14
  • 通讯作者: 周清雷(1962-),男,博士,教授,CCF高级会员,主要研究方向为模型检测、自动机理论和信息安全等,E-mail:ieqlzhou@zzu.edu.cn
  • 作者简介:韩英杰(1976-),女,硕士,讲师,CCF会员,主要研究方向为形式化方法与模型检测、DNA计算,E-mail:ieyjhan@zzu.edu.cn;朱维军(1976-),男,博士,副教授,主要研究方向为DNA计算、模型检测和形式化方法等。
  • 基金资助:
    本文受国家自然科学基金项目(61572444)资助。

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

HAN Ying-jie, ZHOU Qing-lei, ZHU Wei-jun   

  1. (School of Information Engineering,Zhengzhou University,Zhengzhou 450001,China)
  • Received:2018-11-14 Online:2019-11-15 Published:2019-11-14

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

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

Abstract: 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 checkingin 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 modelchecking 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.

Key words: Model checking, Computation tree logic, DNA molecules, Molecular computing

中图分类号: 

  • TP301
[1] BARNAT J,BAUCH P,BRIM L,et al.Designing fast LTLmodel checking algorithms for many-core GPUs[J].Journal of Parallel and Distributed Computing,2012,72(9):1083-1097.
[2] CARBONE R.LTL model-checking for security protocols [J].AI Communications,2011,24(3):281-283.
[3] FU S,TAYSSIR T.Efficient CTL model-checking for pushdown systems [J].Theoretical Computer Science,2014,549(3):127-145.
[4] BRIM L,ČEŠKA M,ŠAFRÁNEK D.Model checking of biological systems[M]∥Formal Methods for Dynamical Systems.Berlin:Springer-Verlag,2013:63-112.
[5] HOU G,ZHOU K J,YONG J W,et al.Survey of state explosion problem in model checking [J].Computer Science,2013,40(S1):77-86.(in Chinese)侯刚,周宽久,勇嘉伟,等.模型检测中状态爆炸问题研究综述[J].计算机科学,2013,40(S1):77-86.
[6] XU J.Forthcoming era of biological computer [J].Bulletin ofChinese Academy of Sciences,2014,29(1):42-54.(in Chinese)许进.生物计算机时代即将来临[J].中国科学院院刊,2014,29(1):42-54.
[7] EMERSON E A,HAGER K D,KONIECZKA J H.Molecularmodel checking [J].International Journal of Foundations of Computer Science,2006,17(4):733-741.
[8] CLARKE E M,GRUMBERG O,HIRAISHI H,et al.Verification of the futurebus+ cache coherence protocol[J].Formal Methods in System Design,1995,6(2):217-232.
[9] ANDERSON R J,BEAME P,BURNS S,et al.Model checking large software specifications [J].IEEE Transactions on Software Engineering,1998,24(7):498-520.
[10] CLARKE E M,EMERSON E A.Design and synthesis of synchronization skeletons using branching-time temporal logic[C]∥The Workshop on Logic of Programs.Berlin:Springer,1981,131:52-71.
[11] QUEILLE J P,SIFAKIS J.Specification and verification of concurrent systems in CESAR[C]∥Colloquium on International Symposium on Programming.Berlin:Springer-Verlag,1982:337-351.
[12] CLARKE E M,GRUMBERG O,PELED D A.Model checking [M].Massachusetts:The MIT Press,1999:35-36.
[13] HAN Y J,ZHU W J,JIAO L F,et al.DNA computing methodsof LTL model checking on Xp [J].Mini-Micro Systems,2017,38(3):553-558.(in Chinese)韩英杰,朱维军,焦林枫,等.线性时序逻辑公式Xp模型检测的DNA计算方法[J].小型微型计算机系统,2017,38(3):553-558.
[14] MARTÍNEZ-PÉREZ I M,ZIMMERMANN K H,IGNATOVA Z.An autonomous DNA model for finite state automata [J].International Journal of Bioinformatics Research & Applications,2009,5(1):81-96.
[15] ZIMMERMANN K H,ISRAEL M P,ZOYA I.DNA computing models [M].New York:Springer,2008:127-128.
[16] ZHU W J,HAN Y J,ZHOU Q L.Performing CTL model checking via DNA computing [J/OL].https://doi.org/10.1007/s00500-018-3314-7.
[17] ZHU W J,WANG Y F,ZHOU Q L,et al.Model checking computational tree logic using sticker automata[M]∥Bio-Inspired Computing-Theories and Applications.Singapore:Springer,2016:12-20.
[18] ZHU W J,ZHOU Q L,ZHANG Q X.A LTL model checking approach based on DNA computing [J].Chinese Journal of Computers,2016,39(12):2578-2597.(in Chinese)朱维军,周清雷,张钦宪.基于DNA计算的线性时序逻辑模型检测方法[J].计算机学报,2016,39(12):2578-2597.
[19] KUPFERMAN O,PNUELI A.Once and for all[C]∥Procee-dings of Tenth Annual IEEE Symposium on Logic in Computer Science.New Jersey:IEEE Computer Society Press,1995:25-35.
[20] LICHTENSTEIN O,PNUELI A,ZUCK L.The glory of thepast[M]∥Logics of Programs.Berlin:Springer,1985:196-218.
[21] EMERSON E A.Temporal and modal logic[M]∥Handbook ofTheoretical Computer Science.Massachusetts:The MIT Press,1990:995-1072.
[22] HAN Y J,ZHOU Q L,JIAO L F,et al.Model checking forcomputation tree logic with past based on DNA computing[M]∥Bio-Inspired Computing-Theories and Applications.Singapore:Springer,2017:131-147.
[23] ZHU W J,ZHOU Q L,LI Y L.LTL model checking based on DNA computing[J].Acta Electronica Sinica,2016,44(6):1265-1271.(in Chinese)朱维军,周清雷,李永亮.以DNA 为载体的线性时序逻辑模型检测[J].电子学报,2016,44(6):1265-1271.
[24] ZHU W J,FENG C,WU H M.Model checking temporal logic formulas using sticker automata[J].BioMed Research International,2017,2017(3):1-33.
[25] MARTÍNEZ-PÉREZ I M,ZHANG G,IGNATOVA Z,et al.Computational genes:a tool for molecular diagnosis and therapy of aberrant mutational phenotype [J].BMC Bioinformatics,2007,8(1):365-365.
[26] ADLEMAN L M.On constructing a molecular computer[M]∥Lipton R J,Baum E B,eds.DNA Based Computers.American Mathematical Society,1996:1-21.
[27] LIU Q,WANG L,FRUTOS A G,et al.DNA computing on surfaces [J].Nature,2000,403(6766):175-178.
[28] ROWEIS S,WINFREE E,BURGOYNE R,et al.A stickerbased model for DNA computation [J].Journal of ComputationalBiology,1998,5(4):615-629.
[29] HEAD T.Splicing Schemes and DNA[C]∥Lindenmayer Systems:Impacts on theoretical computer science,computer graphics and developmental biology.Heidelberg:Springer,1992:371-383.
[30] ADLEMAN L M.Molecular computation of solutions to combinatorial problems [J].Science,1994,266(5187):1021-1023.
[31] LIPTON R J.DNA solution of hard computational problems[J].Science,1995,268(5210):542-545.
[32] BRAICH R S,CHELYAPOV N,JOHNSON C,et al.Solution of a 20-variable 3-SAT problem on a DNA computer [J].Science,2002,296(5567):499-502.
[33] OUYANG Q,KAPLAN P D,LIU S,et al.DNA solution of the maximal clique problem[J].Science,1997,278(5337):446-449.
[34] GAO L,XU J.DNA solution of vertex cover problem based on sticker model[J].Chinese Journal of Electronics,2002,11(2):280-284.
[35] LI K L,ZHOU X,XU J.An O(2n) Volume molecular solutionsfor the 3-colorable problem on DNA—based supercomputing [J].Acta Electronica Sinica,2008,36(11):2096-2101.(in Chinese)李肯立,周旭,许进.图3-着色问题的O(2n)链数DNA计算机算法[J].电子学报,2008,36(11):2096-2101.
[36] WINFREE E,LIU F,WENZLER L A,et al.Design and self-assembly of two-dimensional DNA crystals [J].Nature,1998,394(6693):539-544.
[37] SAKAMOTO K,GOUZU H,KOMIYA K,et al.Molecularcomputation by DNA hairpin formation [J].Science,2000,288(6469):1223-1226.
[38] BENENSON Y,PAZ-ELIZUR T,ADAR R,et al.Programmable and autonomous computing machine made of biomolecules [J].Nature,2001,414(6862):430-439.
[39] KURAMOCHI J,SAKAKIBARA Y.Intensive in vitro experiments of implementing and executing finite automata in test tube[M]∥DNA Computing.Berlin:Springer,2005:193-202.
[40] XIAO J H,XU J.The DNA computation model based on giant magnetoresistance for sat problem [J].Chinese Journal of Computers,2013,36(4):829-835.(in Chinese)肖建华,许进.可满足性问题的巨磁电阻型DNA计算模型[J].计算机学报,2013,36(4):829-835.
[41] XU J.Probe machine[J].IEEE Transactions on Neural Networks and Learning Systems,2016,27(7):1405-1416.
[42] LI K L,LUO X,WU F,et al.An algorithm in tile assembly model for maximum clique problem [J].Journal of Computer Research and Development,2013,50(3):666-675.(in Chinese)李肯立,罗兴,吴帆,等.基于自组装模型的最大团问题DNA计算算法[J].计算机研究与发展,2013,50(3):666-675.
[43] ZHANG G,IGNATOVA Z.Biomolecular autonomous solutionof the Hamiltonian path problem via hairpin formation [J].International Journal of Bioinformatics Research & Applications,2005,1(4):389-398.
[44] YANG J,DONG C,DONG Y F,et al.Logic nanoparticle beacon triggered by the binding-induced effect of multiple inputs[J].ACS Applied Materials & Interfaces,2014,6(16):14486-14492.
[45] YANG J,JIANG S X,LIU X R,et al.Aptamer-Binding Directed DNA Origami Pattern for Logic Gates[J].ACS Applied Materials & Interfaces,2016,8(49):34054-34060.
[46] PAN L Q,WANG Z Y,LI Y F,et al.Nicking enzyme-controlled toehold regulation for DNA logic circuits[J].Nanoscale,2017,9(46):18223-18228.
[47] YANG J,WU R F,LI Y F,et al.Entropy-driven DNA logic circuits regulated by DNAzyme[J].Nucleic Acids Research,2018,46(16):8532-8541.
[48] SHI X L,WANG Z Y,DENG C Y,et al.A novel bio-sensorbased on DNA strand displacement [J].Plos One,2014,9(10),e108856-e108856.
[49] LI X,SONG T,SHI X L,et al.A universal fast colorimetricmethod for DNA signal detection with DNA strand displacement and gold nanoparticles [J].Journal of Nanomaterials,2015(1/2):1-9.
[50] LI X,LI H,SONG T,et al.Highly biocompatible drug-delivery systems based on DNA nanotechnology [J].Journal of BiomedicalNanotechnology,2017,13(7):747-757.
[51] SHI X L,CHEN C Z,LI X,et al.Size controllable DNA nanoribbons assembled from three types of reusable brick single-strand DNA tiles [J].Soft matter,2015,11(43):8484-8492.
[52] SHI X L,WU X X,SONG T,et al.Construction of DNA nanotubes with controllable diameters and patterns by using hierarchical DNA sub-tiles [J].Nanoscale,2016,8(31):14785-14792.
[53] The NUPACK team.NUPACK[EB/OL].http://www.nupack.org.
[54] ZHU W J,HAN Y J,WU H M,et al.Predicting the results of molecular specific hybridization using boosted tree algorithm[J/OL].https://www.researchgate.net/publication/327760975_Predicting_the_results_of_molecular_specific_hybridization_using_boosted_tree_algorithm.
[55] XU J,TAN G J,FAN Y K,et al.DNA computer principle,advances and difficulties(IV):on the models of DNA computer[J].Chinese Journal of Computers,2007,30(6):881-893.(in Chinese)许进,谭钢军,范月科,等.DNA计算机原理、进展及难点(IV):论DNA计算机模型[J].计算机学报,2007,30(6):881-893.
[1] 骆翔宇, 许杭娜, 曾昊晟, 陈祖希, 杨帆. 离散实时线性动态逻辑的符号化模型检测[J]. 计算机科学, 2020, 47(9): 204-212.
[2] 蔡泳, 钱俊彦, 潘海玉. 基于度量线性时态逻辑的近似安全性[J]. 计算机科学, 2020, 47(10): 309-314.
[3] 夏奴奴, 杨晋吉, 赵淦森, 莫晓珊. 基于概率模型的云辅助的轻量级无证书认证协议的形式化验证[J]. 计算机科学, 2019, 46(8): 206-211.
[4] 周女琪, 周宇. 基于概率模型检测的Web服务组合多目标验证[J]. 计算机科学, 2018, 45(8): 288-294.
[5] 雷丽晖,王静. 可能性测度下的LTL模型检测并行化研究[J]. 计算机科学, 2018, 45(4): 71-75.
[6] 聂凯,周清雷,朱维军,张朝阳. 基于时序逻辑的3种网络攻击建模[J]. 计算机科学, 2018, 45(2): 209-214.
[7] 杨红, 洪玫, 屈媛媛. 基于模型检测技术的变异测试用例生成方法[J]. 计算机科学, 2018, 45(11A): 488-493.
[8] 赵莹, 潘华, 张云猛, 莫启, 代飞. 协同业务过程建模与行为验证[J]. 计算机科学, 2018, 45(11A): 597-602.
[9] 刘爽, 魏欧, 郭宗豪. 基于概率模型检测和遗传算法的基因调控网络的无限范围优化控制[J]. 计算机科学, 2018, 45(10): 313-319.
[10] 杜伊,何洋,洪玫. 概率模型检测在动态能耗管理中的应用[J]. 计算机科学, 2018, 45(1): 261-266.
[11] 高婉玲,洪玫,杨秋辉,赵鹤. 统计算法选择对统计模型检测效率的影响分析[J]. 计算机科学, 2017, 44(Z6): 499-503.
[12] 曾赛文,文中华,戴良伟,袁润. 基于不确定攻击图的攻击路径的网络安全分析[J]. 计算机科学, 2017, 44(Z6): 351-355.
[13] 屈媛媛,洪玫,孙琳. 多核系统动态温度管理TAPE策略的形式化验证[J]. 计算机科学, 2017, 44(Z11): 542-546.
[14] 郭宗豪,魏欧. 使用模型检测解决概率布尔网络优化控制[J]. 计算机科学, 2017, 44(5): 193-198.
[15] 孙程,邢建春,杨启亮,韩德帅. 设备自动巡检控制逻辑的层级时间自动机建模与验证[J]. 计算机科学, 2017, 44(4): 66-71.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[1] 雷丽晖,王静. 可能性测度下的LTL模型检测并行化研究[J]. 计算机科学, 2018, 45(4): 71 -75 .
[2] 孙启,金燕,何琨,徐凌轩. 用于求解混合车辆路径问题的混合进化算法[J]. 计算机科学, 2018, 45(4): 76 -82 .
[3] 张佳男,肖鸣宇. 带权混合支配问题的近似算法研究[J]. 计算机科学, 2018, 45(4): 83 -88 .
[4] 伍建辉,黄中祥,李武,吴健辉,彭鑫,张生. 城市道路建设时序决策的鲁棒优化[J]. 计算机科学, 2018, 45(4): 89 -93 .
[5] 史雯隽,武继刚,罗裕春. 针对移动云计算任务迁移的快速高效调度算法[J]. 计算机科学, 2018, 45(4): 94 -99 .
[6] 周燕萍,业巧林. 基于L1-范数距离的最小二乘对支持向量机[J]. 计算机科学, 2018, 45(4): 100 -105 .
[7] 刘博艺,唐湘滟,程杰仁. 基于多生长时期模板匹配的玉米螟识别方法[J]. 计算机科学, 2018, 45(4): 106 -111 .
[8] 杨羽琦,章国安,金喜龙. 车载自组织网络中基于车辆密度的双簇头路由协议[J]. 计算机科学, 2018, 45(4): 126 -130 .
[9] 施超,谢在鹏,柳晗,吕鑫. 基于稳定匹配的容器部署策略的优化[J]. 计算机科学, 2018, 45(4): 131 -136 .
[10] 韩奎奎,谢在鹏,吕鑫. 一种基于改进遗传算法的雾计算任务调度策略[J]. 计算机科学, 2018, 45(4): 137 -142 .