Document Open Access Logo

Modelling and Optimisation of a DNA Stack Nano-Device Using Probabilistic Model Checking

Authors Bowen Li , Neil Mackenzie, Ben Shirt-Ediss , Natalio Krasnogor , Paolo Zuliani

PDF

File

Thumbnail PDF
PDF
LIPIcs.DNA.28.5.pdf
  • Filesize: 2.3 MB
  • 22 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • probabilistic model checking
  • CTMC
  • DNA computing
  • DNA stack

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

A DNA stack nano-device is a bio-computing system that can read and write molecular signals based on DNA-DNA hybridisation and strand displacement. In vitro implementation of the DNA stack faces a number of challenges affecting the performance of the system. In this work, we apply probabilistic model checking to analyse and optimise the DNA stack system. We develop a model framework based on continuous-time Markov chains to quantitatively describe the system behaviour. We use the PRISM probabilistic model checker to answer two important questions: 1) What is the minimum required incubation time to store a signal? And 2) How can we maximise the yield of the system? The results suggest that the incubation time can be reduced from 30 minutes to 5-15 minutes depending on the stack operation stage. In addition, the optimised model shows a 40% increase in the target stack yield.

Cite As Get BibTex

Bowen Li, Neil Mackenzie, Ben Shirt-Ediss, Natalio Krasnogor, and Paolo Zuliani. Modelling and Optimisation of a DNA Stack Nano-Device Using Probabilistic Model Checking. In 28th International Conference on DNA Computing and Molecular Programming (DNA 28). Leibniz International Proceedings in Informatics (LIPIcs), Volume 238, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.DNA.28.5

Author Details

Bowen Li
  • Interdisciplinary Computing and Complex bioSystems (ICOS) Research Group, School of Computing, Newcastle University, Newcastle upon Tyne, UK
Neil Mackenzie
  • Interdisciplinary Computing and Complex bioSystems (ICOS) Research Group, School of Computing, Newcastle University, Newcastle upon Tyne, UK
Ben Shirt-Ediss
  • Interdisciplinary Computing and Complex bioSystems (ICOS) Research Group, School of Computing, Newcastle University, Newcastle upon Tyne, UK
Natalio Krasnogor
  • Interdisciplinary Computing and Complex bioSystems (ICOS) Research Group, School of Computing, Newcastle University, Newcastle upon Tyne, UK
Paolo Zuliani
  • Interdisciplinary Computing and Complex bioSystems (ICOS) Research Group, School of Computing, Newcastle University, Newcastle upon Tyne, UK

Funding

This work was partly funded by the EPSRC’s project "Synthetic Portabolomics: Leading the way at the crossroads of the Digital and the Bio Economies" (EP/N031962/1). Krasnogor was supported by the Royal Academy of Engineering under the Chairs in Emerging Technologies scheme.

Acknowledgements

The authors would like to thank Dr. Harold Fellermann for helpful advice.

Supplementary Materials

References

  1. Leonard M. Adleman. Molecular computation of solutions to combinatorial problems. Science, 266(5187):1021-1024, 1994. URL: https://doi.org/10.1126/science.7973651.
  2. Oana Andrei and Muffy Calder. A Model and Analysis of the AKAP Scaffold. Electronic Notes in Theoretical Computer Science, 268:3-15, 2010. Proceedings of the 1st International Workshop on Interactions between Computer Science and Biology (CS2Bio'10). URL: https://doi.org/10.1016/j.entcs.2010.12.002.
  3. Adnan Aziz, Kumud Sanwal, Vigyan Singhal, and Robert K. Brayton. Model-checking continous-time markov chains. ACM Trans. Comput. Log., 1(1):162-170, 2000. URL: https://doi.org/10.1145/343369.343402.
  4. Christel Baier, Edmund M. Clarke, Vasiliki Hartonas-Garmhausen, Marta Z. Kwiatkowska, and Mark Ryan. Symbolic model checking for probabilistic processes. In Pierpaolo Degano, Roberto Gorrieri, and Alberto Marchetti-Spaccamela, editors, Automata, Languages and Programming, 24th International Colloquium, ICALP'97, Bologna, Italy, 7-11 July 1997, Proceedings, volume 1256 of Lecture Notes in Computer Science, pages 430-440. Springer, 1997. URL: https://doi.org/10.1007/3-540-63165-8_199.
  5. Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Model-checking algorithms for continuous-time markov chains. IEEE Trans. Software Eng., 29(6):524-541, 2003. URL: https://doi.org/10.1109/TSE.2003.1205180.
  6. Muffy Calder, Vladislav Vyshemirsky, David Gilbert, and Richard Orton. Analysis of Signalling Pathways Using Continuous Time Markov Chains. In Corrado Priami and Gordon Plotkin, editors, Transactions on Computational Systems Biology VI, pages 44-67. Springer Berlin Heidelberg, 2006. URL: https://doi.org/10.1007/11880646_3.
  7. Luca Cardelli. Strand algebras for DNA computing. In Russell J. Deaton and Akira Suyama, editors, DNA Computing and Molecular Programming, 15th International Conference, DNA 15, Fayetteville, AR, USA, June 8-11, 2009, Revised Selected Papers, volume 5877 of Lecture Notes in Computer Science, pages 12-24. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-10604-0_2.
  8. Yuan-Jyue Chen, Neil Dalchau, Niranjan Srinivas, Andrew Phillips, Luca Cardelli, David Soloveichik, and Georg Seelig. Programmable chemical controllers made from DNA. Nature Nanotechnology, 8, September 2013. URL: https://doi.org/10.1038/nnano.2013.189.
  9. George M. Church, Yuan Gao, and Sriram Kosuri. Next-Generation Digital Information Storage in DNA. Science, 337(6102):1628-1628, 2012. URL: https://doi.org/10.1126/science.1226355.
  10. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, 2001. Google Scholar
  11. Parker Dave, Norman Gethin, and Kwiatkowska Marta. Prism user manual, 2017. URL: http://www.prismmodelchecker.org/manual/.
  12. Harold Fellermann, Annunziata Lopiccolo, Jerzy Kozyra, and Natalio Krasnogor. In vitro implementation of a stack data structure based on DNA strand displacement. In Martyn Amos and Anne Condon, editors, Unconventional Computation and Natural Computation - 15th International Conference, UCNC 2016, volume 9726 of Lecture Notes in Computer Science, pages 87-98. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-41312-9_8.
  13. Daniel T. Gillespie. A general method for numerically simulating the stochastic time evolution of coupled chemical reactions. Journal of Computational Physics, 22(4):403-434, 1976. URL: https://doi.org/10.1016/0021-9991(76)90041-3.
  14. John Heath, Marta Kwiatkowska, Gethin Norman, David Parker, and Oksana Tymchyshyn. Probabilistic model checking of complex biological pathways. Theoretical Computer Science, 391(3):239-257, 2008. URL: https://doi.org/10.1016/j.tcs.2007.11.013.
  15. Savas Konur, Marian Gheorghe, Ciprian Dragomir, Laurentiu Mierla, Florentin Ipate, and Natalio Krasnogor. Qualitative and quantitative analysis of systems and synthetic biology constructs using P systems. ACS Synthetic Biology, 4(1):83-92, 2015. URL: https://doi.org/10.1021/sb500134w.
  16. Jerzy Kozyra, Harold Fellermann, Ben Shirt-Ediss, Annunziata Lopiccolo, and Natalio Krasnogor. Optimizing nucleic acid sequences for a molecular data recorder. In Proceedings of the Genetic and Evolutionary Computation Conference, GECCO '17, pages 1145-1152. ACM, 2017. URL: https://doi.org/10.1145/3071178.3071345.
  17. Marta Kwiatkowska, Gethin Norman, and David Parker. Stochastic model checking. In Marco Bernardo and Jane Hillston, editors, Formal Methods for Performance Evaluation: 7th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2007, Bertinoro, Italy, May 28-June 2, 2007, Advanced Lectures, pages 220-270. Springer Berlin Heidelberg, 2007. URL: https://doi.org/10.1007/978-3-540-72522-0_6.
  18. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 585-591. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_47.
  19. Matthew R. Lakin, David Parker, Luca Cardelli, Marta Kwiatkowska, and Andrew Phillips. Design and analysis of dna strand displacement devices using probabilistic model checking. Journal of The Royal Society Interface, 9(72):1470-1485, 2012. URL: https://doi.org/10.1098/rsif.2011.0800.
  20. Annunziata Lopiccolo, Ben Shirt-Ediss, Emanuela Torelli, Abimbola Feyisara Adedeji Olulana, Matteo Castronovo, Harold Fellermann, and Natalio Krasnogor. A last-in first-out stack data structure implemented in DNA. Nature Communications, 12(1):4861, 2021. URL: https://doi.org/10.1038/s41467-021-25023-6.
  21. Lulu Qian, David Soloveichik, and Erik Winfree. Efficient Turing-Universal Computation with DNA Polymers. In Yasubumi Sakakibara and Yongli Mi, editors, DNA Computing and Molecular Programming, pages 123-140. Springer Berlin Heidelberg, 2011. URL: https://doi.org/10.1007/978-3-642-18305-8_12.
  22. Lulu Qian and Erik Winfree. A Simple DNA Gate Motif for Synthesizing Large-Scale Circuits. In Ashish Goel, Friedrich C. Simmel, and Petr Sosik, editors, DNA Computing and Molecular Programming, pages 70-89. Springer Berlin Heidelberg, 2009. URL: https://doi.org/10.1007/978-3-642-03076-5_7.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact