Skip to main content
SpringerLink
Log in
Book cover

International Conference on Applications and Theory of Petri Nets and Concurrency

PETRI NETS 2015: Application and Theory of Petri Nets and Concurrency pp 1–32Cite as

On Quantitative Modelling and Verification of DNA Walker Circuits Using Stochastic Petri Nets

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9115))

Abstract

Molecular programming is an emerging field concerned with building synthetic biomolecular computing devices at the nanoscale, for example from DNA or RNA molecules. Many promising applications have been proposed, ranging from diagnostic biosensors and nanorobots to synthetic biology, but prohibitive complexity and imprecision of experimental observations makes reliability of molecular programs difficult to achieve. This paper advocates the development of design automation methodologies for molecular programming, highlighting the role of quantitative verification in this context. We focus on DNA ‘walker’ circuits, in which molecules can be programmed to traverse tracks placed on a DNA origami tile, taking appropriate decisions at junctions and reporting the outcome when reaching the end of the track. The behaviour of molecular walkers is inherently probabilistic and thus probabilistic model checking methods are needed for their analysis. We demonstrate how DNA walkers can be modelled using stochastic Petri nets, and apply statistical model checking using the tool Cosmos to analyse the reliability and performance characteristics of the designs. The results are compared and contrasted with those obtained for the PRISM model checker. The paper ends by summarising future research challenges in the field.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Baier, C.: On algorithmic verification methods for probabilistic systems. Habilitation thesis, Fakultät für Mathematik & Informatik, Universität Mannheim (1998)

    Google Scholar 

  2. Baier, C., Katoen, J.-P., Hermanns, H.: Approximate symbolic model checking of continuous-time markov chains (extended abstract). In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, p. 146. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  3. Ballarini, P., Barbot, B., Duflot, M., Haddad, S., Pekergin, N.: HASL: A new approach for performance evaluation and model checking from concepts to experimentation. Performance Evaluation, 2015. To appear

    Google Scholar 

  4. Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: Cosmos: a statistical model checker for the hybrid automata stochastic logic. In: 2011 Eighth International Conference on Quantitative Evaluation of Systems (QEST), pp. 143–144. IEEE (2011)

    Google Scholar 

  5. Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: HASL: an expressive language for statistical verification of stochastic models. In: Samson Lasaulce, P.H., Fiems, D., Vandendorpe, L. (eds.) Proceedings of the 5th International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS’11), pp. 306–315. ICST, Cachan (2011)

    Google Scholar 

  6. Barbot, B., Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Efficient CTMC model checking of linear real-time objectives. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 128–142. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  7. Barbot, B., Haddad, S., Picaronny, C.: Coupling and importance sampling for statistical model checking. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 331–346. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  8. Bath, J., Green, S.J., Turberfield, A.J.: A free-running DNA motor powered by a nicking enzyme. Angewandte Chemie 44, 4358–61 (2005)

    Article  Google Scholar 

  9. Chandran, H., Gopalkrishnan, N., Phillips, A., Reif, J.: Localized hybridization circuits. DNA Computing and Molecular Programming 6937, 64–83 (2011)

    Google Scholar 

  10. Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Time-bounded verification of CTMCs against real-time specifications. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 26–42. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  11. Chen, Y.-J., Dalchau, N., Srinivas, N., Phillips, A., Cardelli, L., Soloveichik, D., Seelig, G.: Programmable chemical controllers made from DNA. Nature Nanotechnology 8(10), 755–762 (2013)

    Article  Google Scholar 

  12. Chow, Y.S., Robbins, H.: On the asymptotic theory of fixed-width sequential confidence intervals for the mean. The Annals of Mathematical Statistics, 457–462 (1965)

    Google Scholar 

  13. Ciocchetta, F., Hillston, J.: Bio-PEPA: A framework for the modelling and analysis of biological systems. Theoretical Computer Science 410(33–34), 3065–3084 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  14. Dannenberg, F., Hahn, E.M., Kwiatkowska, M.: Computing cumulative rewards using fast adaptive uniformisation. In: Gupta, A., Henzinger, T.A. (eds.) CMSB 2013. LNCS, vol. 8130, pp. 33–49. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  15. Dannenberg, F., Kwiatkowska, M., Thachuk, C., Turberfield, A.J.: DNA walker circuits: computational potential, design, and verification. In: Soloveichik, D., Yurke, B. (eds.) DNA 2013. LNCS, vol. 8141, pp. 31–45. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  16. Dannenberg, F., Kwiatkowska, M., Thachuk, C., Turberfield, A.: Dna walker circuits: Computational potential, design, and verification. Natural Computing (2014)

    Google Scholar 

  17. Diaz, M.: Petri Nets: Fundamental models, verification and applications. Wiley (2010)

    Google Scholar 

  18. Didier, F., Henzinger, T.A., Mateescu, M., Wolf, V.: SABRE: A tool for stochastic analysis of biochemical reaction networks. In: Seventh International Conference on the Quantitative Evaluation of Systems QEST 2010, Williamsburg, Virginia, USA, September 15–18, pp. 193–194 (2010)

    Google Scholar 

  19. Donatelli, S., Haddad, S., Sproston, J.: CSL TA: an expressive logic for continuous-time markov chains. In: Fourth International Conference on the Quantitative Evaluation of Systems, QEST 2007, pp. 31–40. IEEE (2007)

    Google Scholar 

  20. Eisentraut, C., Hermanns, H., Katoen, J.-P., Zhang, L.: A semantics for every GSPN. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 90–109. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  21. Dannenberg, E.M.H.F., Kwiatkowska, M.: Computing cumulative rewards using fast adaptive uniformisation. ACM Transactions on Modeling and Computer Simulation, Special Issue in Computational Methods in Systems Biology (2014)

    Google Scholar 

  22. Fox, B.L., Glynn, P.W.: Computing poisson probabilities. Commun. ACM 31(4), 440–445 (1988)

    Article  MathSciNet  Google Scholar 

  23. Gillespie, D.: Exact stochastic simulation of coupled chemical reactions. The Journal of Physical Chemistry 93555, 2340–2361 (1977)

    Article  Google Scholar 

  24. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512–535 (1994)

    Article  MATH  Google Scholar 

  25. Heiner, M., Rohr, C., Schwarick, M.: MARCIE – model checking and reachability analysis done efficiently. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 389–399. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  26. Jegourel, C., Legay, A., Sedwards, S.: Cross-entropy optimisation of importance sampling parameters for statistical model checking. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 327–342. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  27. Jegourel, C., Legay, A., Sedwards, S.: Importance splitting for statistical model checking rare properties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 576–591. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  28. Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 218–234. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  29. Jung, C., Ellington, A.D.: Diagnostic applications of nucleic acid circuits. Accounts of Chemical Research (2014, to appear)

    Google Scholar 

  30. Kartson, D., Balbo, G., Donatelli, S., Franceschinis, G., Conte, G.: Modelling with generalized stochastic Petri nets. Wiley (1994)

    Google Scholar 

  31. Kwiatkowska, M.: Quantitative verification: models, techniques and tools. In: Proc. 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), pp. 449–458. ACM Press (September 2007)

    Google Scholar 

  32. Kwiatkowska, M.: Challenges in automated verification and synthesis for molecular programming. In: Abadi, M., Gardner, P., Gordon, A.D., Mardare, R. (eds.) Essays for the Luca Cardelli Fest, Volume MSR-TR-2014-104 of Technical Report, pp. 155–170. Microsoft Research (2014)

    Google Scholar 

  33. Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  34. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  35. Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  36. Lakin, M., Parker, D., Cardelli, L., Kwiatkowska, M., Phillips, A.: Design and analysis of DNA strand displacement devices using probabilistic model checking. Journal of the Royal Society Interface 9, 1470–1485 (2012)

    Article  Google Scholar 

  37. Liu, F., Heiner, M.: Colored petri nets to model and simulate biological systems. In: Proceedings of the Workshops of the 31st International Conference on Application and Theory of Petri Nets and Other Models of Concurrency (PETRI NETS 2010) and of the 10th International Conference on Application of Concurrency to System Design (ACSD 2010), Braga, Portugal (June 2010) pages 71–85, 2010

    Google Scholar 

  38. Češka, M., Dannenberg, F., Kwiatkowska, M., Paoletti, N.: Precise parameter synthesis for stochastic biochemical systems. In: Mendes, P., Dada, J.O., Smallbone, K. (eds.) CMSB 2014. LNCS, vol. 8859, pp. 86–98. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  39. Mateescu, M.-E.-C.: Propagation Models for Biochemical Reaction Networks. PhD thesis (2011)

    Google Scholar 

  40. Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46–57. IEEE (1977)

    Google Scholar 

  41. Qian, L., Winfree, E.: Scaling up digital circuit computation with DNA strand displacement cascades. Science 332, 1196–1201 (2011)

    Article  Google Scholar 

  42. Reijsbergen, D., de Boer, P.-T., Scheinhardt, W., Haverkort, B.: Automated rare event simulation for stochastic petri nets. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 372–388. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  43. Rothemund, P.: Folding DNA to create nanoscale shapes and patterns. Nature 440, 297–302 (2006)

    Article  Google Scholar 

  44. Seelig, G., Soloveichik, D., Zhang, D., Winfree, E.: Enzyme-free nucleic acid logic circuits. Science 314, 1585–1588 (2006)

    Article  Google Scholar 

  45. Soloveichik, D., Seelig, G., Winfree, E.: DNA as a universal substrate for chemical kinetics. Proceedings of the National Academy of Science 107(12), 5393–5398 (2010)

    Article  Google Scholar 

  46. Wald, A.: Sequential tests of statistical hypotheses. The Annals of Mathematical Statistics 16(2), 117–186 (1945)

    Article  MATH  MathSciNet  Google Scholar 

  47. Wickham, S.F., Endo, M., Katsuda, Y., Hidaka, K., Bath, J., Sugiyama, H., Turberfield, A.J.: Direct observation of stepwise movement of a synthetic molecular transporter. Nature Nanotechnology 6(3), 166–169 (2011)

    Article  Google Scholar 

  48. Wickham, S.F.J., Bath, J., Katsuda, Y., Endo, M., Hidaka, K., Sugiyama, H., Turberfield, A.J.: A DNA-based molecular motor that can navigate a network of tracks. Nature Nanotechnology 7, 169–173 (2012)

    Article  Google Scholar 

  49. Wickham, S.F.J., Bath, J., Katsuda, Y., Endo, M., Hidaka, K., Sugiyama, H., Turberfield, A.J.: A dna-based molecular motor that can navigate a network of tracks. Nat Nano 7(3), 169–173 (2012)

    Article  Google Scholar 

  50. Wickham, S.F.J., Endo, M., Katsuda, Y., Hidaka, K., Bath, J., Sugiyama, H., Turberfield, A.J.: Direct observation of stepwise movement of a synthetic molecular transporter. Nature Nanotechnology 6, 166–169 (2011)

    Article  Google Scholar 

  51. Yin, P., Yan, H., Daniell, X.G., Turberfield, A.J., Reif, J.H.: A unidirectional DNA walker that moves autonomously along a track. Angewandte Chemie International Edition 43, 4906–4911 (2004)

    Article  Google Scholar 

  52. Yin, P., Yan, H., Daniell, X.G., Turberfield, A.J., Reif, J.H.: A unidirectional dna walker that moves autonomously along a track. Angewandte Chemie International Edition 43(37), 4906–4911 (2004)

    Article  Google Scholar 

  53. Younes, H., Simmons, R.: Statistical probabilistic model checking with a focus on time-bounded properties. Information and Computation 204(9), 1368–1409 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  54. Yurke, B., Turberfield, A., Mills, A., Simmel, F., Neumann, J.: A DNA-fuelled molecular machine made of DNA. Nature 406(6796), 605–8 (2000)

    Article  Google Scholar 

  55. Zhang, D., Seelig, G.: Dynamic DNA nanotechnology using strand displacement reactions. Nature Chemistry 3, 103–113 (2011)

    Article  Google Scholar 

  56. Zhang, D.Y., Turberfield, A.J., Yurke, B., Winfree, E.: Engineering entropy-driven reactions and networks catalyzed by DNA. Science 318(5853), 1121 (2007)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK

    Benoît Barbot & Marta Kwiatkowska

Authors
  1. Benoît Barbot
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marta Kwiatkowska
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Benoît Barbot or Marta Kwiatkowska .

Editor information

Editors and Affiliations

  1. Université Libre de Bruxelles, Brussels, Belgium

    Raymond Devillers

  2. Tampere University of Technology, Tampere, Finland

    Antti Valmari

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Barbot, B., Kwiatkowska, M. (2015). On Quantitative Modelling and Verification of DNA Walker Circuits Using Stochastic Petri Nets. In: Devillers, R., Valmari, A. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2015. Lecture Notes in Computer Science(), vol 9115. Springer, Cham. https://doi.org/10.1007/978-3-319-19488-2_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-19488-2_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-19487-5

  • Online ISBN: 978-3-319-19488-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation