Advertisement

Functional Analysis of Large-Scale DNA Strand Displacement Circuits

Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8141)

Abstract

We present a method for the analysis of functional properties of large-scale DNA strand displacement (DSD) circuits based on Satisfiability Modulo Theories that enables us to prove the functional correctness of DNA circuit designs for arbitrary inputs, and provides significantly improved scalability and expressivity over existing methods. We implement this method as an extension to the Visual DSD tool, and use it to formalize the behavior of a 4-bit square root circuit, together with the components used for its construction. We show that our method successfully verifies that certain designs function as required and identifies erroneous computations in others, even when millions of copies of a circuit are interacting with each other in parallel. Our method is also applicable in the verification of properties for more general chemical reaction networks.

Keywords

Model Check Terminal State Transition Relation Reachable State Logical Block 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in to check access.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  2. 2.
    Chandran, H., Gopalkrishnan, N., Phillips, A., Reif, J.: Localized hybridization circuits. In: Cardelli, L., Shih, W. (eds.) DNA 17. LNCS, vol. 6937, pp. 64–83. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  3. 3.
    Chen, H.-L., Doty, D., Soloveichik, D.: Deterministic Function Computation with Chemical Reaction Networks. In: Stefanovic, D., Turberfield, A. (eds.) DNA 18. LNCS, vol. 7433, pp. 25–42. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  4. 4.
    Condon, A., Kirkpatrick, B., Maňuch, J.: Reachability Bounds for Chemical Reaction Networks and Strand Displacement Systems. In: Stefanovic, D., Turberfield, A. (eds.) DNA 2012. LNCS, vol. 7433, pp. 43–57. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  5. 5.
    Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252. ACM (1977)Google Scholar
  6. 6.
    de Moura, L.M., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  7. 7.
    Dong, Q.: A bisimulation approach to verification of molecular implementations of formal chemical reaction networks. Master’s thesis, Stony Brook University (2012)Google Scholar
  8. 8.
    Doty, D., Hajiaghayi, M.: Leaderless deterministic chemical reaction networks. arXiv:1304.4519 (2013)Google Scholar
  9. 9.
    Famili, I., Palsson, B.O.: The convex basis of the left null space of the stoichiometric matrix leads to the definition of metabolically meaningful pools. Biophysical Journal 85(1), 16–26 (2003)CrossRefGoogle Scholar
  10. 10.
    Fränzle, M., Hermanns, H., Teige, T.: Stochastic satisfiability modulo theory: A novel technique for the analysis of probabilistic hybrid systems. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 172–186. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  11. 11.
    Heiner, M., Gilbert, D., Donaldson, R.: Petri Nets for Systems and Synthetic Biology. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol. 5016, pp. 215–264. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  12. 12.
    Kaivola, R., Ghughal, R., Narasimhan, N., Telfer, A., Whittemore, J., Pandav, S., Slobodová, A., Taylor, C., Frolov, V., Reeber, E., Naik, A.: Replacing Testing with Formal Verification in Intel® CoreTM i7 Processor Execution Engine Validation. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 414–429. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  13. 13.
    Lakin, M.R., 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(72), 1470–1485 (2012)CrossRefGoogle Scholar
  14. 14.
    Lakin, M.R., Youssef, S., Polo, F., Emmott, S., Phillips, A.: Visual DSD: A design and analysis tool for DNA strand displacement systems. Bioinformatics 27(22), 3211–3213 (2011)CrossRefGoogle Scholar
  15. 15.
    Lakin, M.R., Phillips, A.: Modelling, simulating and verifying turing-powerful strand displacement systems. In: Cardelli, L., Shih, W. (eds.) DNA 17. LNCS, vol. 6937, pp. 130–144. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  16. 16.
    Manna, Z., Pnueli, A.: Temporal verification of reactive systems: safety, vol. 2. Springer (1995)Google Scholar
  17. 17.
    Qian, L., Winfree, E.: Scaling up digital circuit computation with DNA strand displacement cascades. Science 332(6034), 1196–1201 (2011)CrossRefGoogle Scholar
  18. 18.
    Shin, S.W.: Compiling and verifying DNA-based chemical reaction network implementations. Master’s thesis, California Institute of Technology (2012)Google Scholar
  19. 19.
    Thachuk, C., Condon, A.: Space and Energy Efficient Computation with DNA Strand Displacement Systems. In: Stefanovic, D., Turberfield, A. (eds.) DNA 18. LNCS, vol. 7433, pp. 135–149. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  20. 20.
    Wintersteiger, C.M., Hamadi, Y., de Moura, L.: Efficiently solving quantified bit-vector formulas. Formal Methods in System Design 42(1), 3–23 (2013)CrossRefzbMATHGoogle Scholar
  21. 21.
    Yordanov, B., Wintersteiger, C.M., Hamadi, Y., Kugler, H.: SMT-based analysis of biological computation. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 78–92. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  22. 22.
    Z34Bio at rise4fun Software Engineering Tools from Microsoft Research (2013), http://rise4fun.com/z34biology
  23. 23.
    Zavattaro, G., Cardelli, L.: Termination problems in chemical kinetics. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 477–491. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  24. 24.
    Zhang, D.Y., Seelig, G.: Dynamic DNA nanotechnology using strand-displacement reactions. Nat. Chem. 3(2), 103–113 (2011)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  1. 1.Microsoft ResearchCambridgeUK

Personalised recommendations

Cite paper

Buy options