Skip to main content
SpringerLink
Log in

Performing CTL model checking via DNA computing

  • Foundations
  • Published:
Soft Computing Aims and scope Submit manuscript

Abstract

The computation using deoxyribonucleic acid (DNA) molecules provides an enormous parallel method that breaks through the limitations of the efficiency of traditional electronic computers. Model checking is a standard formal verification technique, which has been widely used in many fields of computation. It is also a well-known complex problem in computing theory. Until now, there is only one basic formula in the computation tree logic (CTL), for which model checking via DNA computing can be conducted. To this end, Adleman’s model based on DNA computing is used in this paper, based on which a series of DNA-computing-based model-checking algorithms to check the four basic CTL formulas are proposed. As a result, a core of the DNA version of the CTL model-checking problem is solved. The simulated experimental results show that the new algorithms are valid and can be properly implemented in molecular biology.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16
Fig. 17
Fig. 18
Fig. 19

Similar content being viewed by others

References

  • Adleman LM (1994) Molecular computation of solutions to combinatorial problems. Science 266(5187):1021–1024

    Article  Google Scholar 

  • Adleman LM (1996) On constructing a molecular computer. Discrete Math Theor Comput Sci 27:1–21

    Article  MathSciNet  Google Scholar 

  • Andreas C, Maxime C, Pierre Y (2013) Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans Softw Eng 39(8):1069–1089

    Article  Google Scholar 

  • Barnat J, Brim L, Ivana C (2008) Parallel model checking large-scale genetic regulatory networks with DiVinE. Electron Notes Theor Comput Sci 194(3):35–50

    Article  MATH  Google Scholar 

  • Bhat G, Cleaveland R, Grumberg O (2002) Efficient on-the-fly model checking for CTL. In: IEEE symposium on logic in computer science, p 388

  • Brim L, Milan C, David S (2013) Model checking of biological systems. Formal methods for dynamical systems. Springer, Berlin, pp 63–112

    Book  MATH  Google Scholar 

  • Camilli M, Bellettini C, Capra L, Monga M (2015) CTL Model checking in the cloud using MapReduce. In: International symposium on symbolic and numeric algorithms for scientific computing, pp 333–340

  • Edmund MC, Doron AP, Orna G (1999) Model checking. MIT, Massachusetts

    MATH  Google Scholar 

  • Emerson EA, Edmund MC (1982) Using branching-time temporal logic to synthesize synchronization skeletons. Sci Comput Program 2(3):241–266

    Article  MATH  Google Scholar 

  • Emerson EA, Kristina DH, Jay HK (2006) Molecular model checking. Int J Found Comput Sci 17(04):733–742

    Article  MathSciNet  MATH  Google Scholar 

  • Iwashita H, Nakata T, Hirose F(1997) CTL model checking based on forward state traversal. In: IEEE/ACM international conference on computer-aided design, pp 82–87

  • Kensaku S, Hidetaka G, Ken K (2000) Molecular computation by DNA hairpin formation. Science 288(5469):1223–1226

    Article  Google Scholar 

  • Lakin M, Parker D, Cardelli L (2012) Design and analysis of DNA strand displacement devices using probabilistic model checking. J R Soc Interface 9(72):1470–1485

    Article  Google Scholar 

  • Li YM (2017) Quantitative model checking of linear-time properties based on generalized possibility measures. Fuzzy Sets Syst 320:17–39

    Article  MathSciNet  MATH  Google Scholar 

  • Li YM, Ma ZY (2015) Quantitative computation tree logic model checking based on generalized possibility measures. IEEE Trans Fuzzy Syst 23(6):2034–2047

    Article  Google Scholar 

  • Li YM, Huang SB, Lin JY (2015a) Data flow analysis and formal method. In: International conference of young computer scientists, engineers and educators, ICYCSEE 2015, intelligent computation in big data era, volume 503 of the series communications in computer and information science, Harbin, China, pp 398–406

  • Li YM, Li YL, Ma ZY (2015b) Computation tree logic model checking based on possibility measures. Fuzzy Sets Syst 262:44–59

    Article  MathSciNet  MATH  Google Scholar 

  • Lipton RJ (1995) DNA solution of hard computational problems. Science 268(5210):542–545

    Article  Google Scholar 

  • NUPACK (2015) http://www.nupack.org/partition/new

  • Ouyang Q, Peter DK, Liu S (1997) DNA solution of the maximal clique problem. Science 278(5337):446–449

    Article  Google Scholar 

  • Pnueli A (1977) The temporal logic of programs. In: Symposium on foundations of computer science, Washington, DC, USA, pp 46–57

  • Roberto C (2011) LTL model-checking for security protocols. AI Commun 24(3):281–283

    Google Scholar 

  • Shankara C, Das S, Vidyarthi A (2011) Homology modeling and function prediction of hABH1, involving in repair of alkylation damaged DNA. Interdiscip Sci Comput Life Sci 3(3):175–181

    Article  Google Scholar 

  • Shapiro E, Benenson Y, Adar R (2001) Programmable and autonomous computing machine made of biomolecules. Nature 414(6862):430–434

    Article  Google Scholar 

  • Wang YF, Cui GZ (2013) The design and optimization of DNA coding sequence. Publishing House of Electronics Industry, Beijing

    Google Scholar 

  • Wang YF, Sun JW, Cui GZ, Zhang XC, Zheng Y (2010) Basic logical operations using algorithmic self-assembly of DNA molecules. J Nanoelectron Optoelectron 5(1):30–37

    Article  Google Scholar 

  • Xu J (2013) The development programme of the Zhongzhou I DNA computer. Technical report TR-12. Beijing University, Beijing (in Chinese)

  • Xu J (2014) Forthcoming era of biological computer. Bull Chin Acad Sci 29(1):42–54 (in Chinese)

    Google Scholar 

  • Xu J (2016) Probe machine. IEEE Trans Neural Netw Learn Syst 27(7):1405–1416

    Article  MathSciNet  Google Scholar 

  • Yang J, Jiang SX, Liu XR, Pan LQ, Zhang C (2016) Aptamer-binding directed DNA origami pattern for logic gates. ACS Appl Mater Interfaces 8(49):34054–34060

    Article  Google Scholar 

  • Zhang C, Yang J, Jiang SX, Liu Y, Yan H (2016a) DNAzyme-mediated DNA origami pattern for logic gates. Nano Lett 16(1):736

    Article  Google Scholar 

  • Zhang C, Shen LJ, Liang C, Dong YF, Yang J, Xu J (2016b) DNA sequential logic gate using two-ring DNA. ACS Appl Mater Interfaces 8(14):9370–9376

    Article  Google Scholar 

  • Zhu WJ, Zhou QL, Zhang QX (2016) A LTL model checking approach based on DNA computing. Chin J Comput 39(12):2578–2597 (in Chinese)

    MathSciNet  Google Scholar 

  • Zimmermann KH, Israel MP, Zoya I (2008) DNA computing models. Springer, New York

    MATH  Google Scholar 

Download references

Acknowledgements

This study was partially funded by the National Natural Science Foundation of China under Grant Nos. U1204608 and 61572444 and China Postdoctoral Science Foundation under Grant No. 2015M572120.

Author information

Authors and Affiliations

  1. School of Information Engineering, Zhengzhou University, Zhengzhou, 450001, China

    Weijun Zhu, Yingjie Han & Qinglei Zhou

Authors
  1. Weijun Zhu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yingjie Han
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Qinglei Zhou
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Weijun Zhu.

Ethics declarations

Conflict of interest

The authors of this paper declare that they have no conflicts of interest.

Ethical standard

This article does not contain any studies with human participants or animals performed by the authors.

Additional information

Communicated by A. Di Nola.

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Zhu, W., Han, Y. & Zhou, Q. Performing CTL model checking via DNA computing. Soft Comput 23, 3945–3963 (2019). https://doi.org/10.1007/s00500-018-3314-7

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00500-018-3314-7

Keywords

Search

Navigation