Computer Science ›› 2019, Vol. 46 ›› Issue (11): 25-31.doi: 10.11896/jsjkx.181102091

• Surveys • Previous Articles     Next Articles

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

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: Computation tree logic, DNA molecules, Model checking, Molecular computing

CLC Number: 

  • 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] RAN Dan, CHEN Zhe, SUN Yi, YANG Zhi-bin. SCADE Model Checking Based on Program Transformation [J]. Computer Science, 2021, 48(12): 125-130.
[2] CAI Yong, QIAN Jun-yan, PAN Hai-yu. Approximate Safety Properties in Metric Linear Temporal Logic [J]. Computer Science, 2020, 47(10): 309-314.
[3] XIA Nu-nu, YANG Jin-ji, ZHAO Gan-sen, MO Xiao-shan. Formal Verification of Cloud-aided Lightweight Certificateless Authentication Protocol Based on Probabilistic Model [J]. Computer Science, 2019, 46(8): 206-211.
[4] ZHOU Nv-qi, ZHOU Yu. Multi-objective Verification of Web Service Composition Based on Probabilistic Model Checking [J]. Computer Science, 2018, 45(8): 288-294.
[5] LI Yun-chou,YIN Ping. Research of Model Checking Application on Aerospace TT&C Software [J]. Computer Science, 2018, 45(6A): 523-526.
[6] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure [J]. Computer Science, 2018, 45(4): 71-75.
[7] NIE Kai, ZHOU Qing-lei, ZHU Wei-jun and ZHANG Chao-yang. Modeling for Three Kinds of Network Attacks Based on Temporal Logic [J]. Computer Science, 2018, 45(2): 209-214.
[8] YANG Hong, HONG Mei, QU Yuan-yuan. Approach of Mutation Test Case Generation Based on Model Checking [J]. Computer Science, 2018, 45(11A): 488-493.
[9] ZHAO Ying, PAN Hua, ZHANG Yun-meng, MO Qi, DAI Fei. Modeling and Behavior Verification for Collaborative Business Processes [J]. Computer Science, 2018, 45(11A): 597-602.
[10] LIU Shuang, WEI Ou, GUO Zong-hao. Infinite-horizon Optimal Control of Genetic Regulatory Networks Based on Probabilistic Model Checking and Genetic Algorithm [J]. Computer Science, 2018, 45(10): 313-319.
[11] DU Yi, HE Yang and HONG Mei. Application of Probabilistic Model Checking in Dynamic Power Management [J]. Computer Science, 2018, 45(1): 261-266.
[12] GAO Wan-ling, HONG Mei, YANG Qiu-hui and ZHAO He. Efficiency Analysis of Different Statistical Algorithms on Statistical Model Checking [J]. Computer Science, 2017, 44(Z6): 499-503.
[13] QU Yuan-yuan, HONG Mei and SUN Ning. Formal Verification of TAPE Strategy for Dynamic Temperature Management in Multi-core System [J]. Computer Science, 2017, 44(Z11): 542-546.
[14] GUO Zong-hao and WEI Ou. Optimal Control of Probabilistic Boolean Networks Using Model Checking [J]. Computer Science, 2017, 44(5): 193-198.
[15] LIU Bin-bin, LIU Wan-wei, MAO Xiao-guang and DONG Wei. Correctness Verification of Rules for Unmanned Vehicles’ Decision System [J]. Computer Science, 2017, 44(4): 72-74.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!