Document Open Access Logo

CRNs Exposed: A Method for the Systematic Exploration of Chemical Reaction Networks

Authors Marko Vasic, David Soloveichik, Sarfraz Khurshid

PDF
Thumbnail PDF

File

LIPIcs.DNA.2020.4.pdf
  • Filesize: 0.6 MB
  • 25 pages

Document Identifiers

Author Details

Marko Vasic
  • The University of Texas at Austin, TX, USA
David Soloveichik
  • The University of Texas at Austin, TX, USA
Sarfraz Khurshid
  • The University of Texas at Austin, TX, USA

Acknowledgements

This work was supported in part by NSF grants CCF-1901025 to DS and CCF-1718903 to SK.

Cite AsGet BibTex

Marko Vasic, David Soloveichik, and Sarfraz Khurshid. CRNs Exposed: A Method for the Systematic Exploration of Chemical Reaction Networks. In 26th International Conference on DNA Computing and Molecular Programming (DNA 26). Leibniz International Proceedings in Informatics (LIPIcs), Volume 174, pp. 4:1-4:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.DNA.2020.4

Abstract

Formal methods have enabled breakthroughs in many fields, such as in hardware verification, machine learning and biological systems. The key object of interest in systems biology, synthetic biology, and molecular programming is chemical reaction networks (CRNs) which formalizes coupled chemical reactions in a well-mixed solution. CRNs are pivotal for our understanding of biological regulatory and metabolic networks, as well as for programming engineered molecular behavior. Although it is clear that small CRNs are capable of complex dynamics and computational behavior, it remains difficult to explore the space of CRNs in search for desired functionality. We use Alloy, a tool for expressing structural constraints and behavior in software systems, to enumerate CRNs with declaratively specified properties. We show how this framework can enumerate CRNs with a variety of structural constraints including biologically motivated catalytic networks and metabolic networks, and seesaw networks motivated by DNA nanotechnology. We also use the framework to explore analog function computation in rate-independent CRNs. By computing the desired output value with stoichiometry rather than with reaction rates (in the sense that X → Y+Y computes multiplication by 2), such CRNs are completely robust to the choice of reaction rates or rate law. We find the smallest CRNs computing the max, minmax, abs and ReLU (rectified linear unit) functions in a natural subclass of rate-independent CRNs where rate-independence follows from structural network properties.

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • molecular programming
  • formal methods

Metrics

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

Supplementary Materials

References

  1. Dana Angluin, James Aspnes, and David Eisenstat. A simple population protocol for fast robust approximate majority. Distributed Computing, 21(2):87-102, 2008. Google Scholar
  2. Dana Angluin, James Aspnes, David Eisenstat, and Eric Ruppert. The computational power of population protocols. Distributed Computing, 20(4):279-304, 2007. Google Scholar
  3. Murad Banaji. Counting chemical reaction networks with NAUTY. arXiv preprint arXiv:1705.10820, 2017. Google Scholar
  4. Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In CAV, 2011. Google Scholar
  5. Gilles Bernot, Jean-Paul Comet, Adrien Richard, and Janine Guespin. Application of formal methods to biological regulatory networks: extending thomas’ asynchronous logical approach with temporal logic. Journal of theoretical biology, 2004. Google Scholar
  6. Luca Cardelli. Strand algebras for DNA computing. Natural Computing, 10(1):407-428, 2011. Google Scholar
  7. Luca Cardelli. Morphisms of reaction networks that couple structure to function. BMC systems biology, 8(1):84, 2014. Google Scholar
  8. Luca Cardelli, Milan Češka, Martin Fränzle, Marta Kwiatkowska, Luca Laurenti, Nicola Paoletti, and Max Whitby. Syntax-guided optimal synthesis for chemical reaction networks. In CAV, 2017. Google Scholar
  9. Cameron Chalk, Niels Kornerup, Wyatt Reeves, and David Soloveichik. Composable rate-independent computation in continuous chemical reaction networks. In CMSB, pages 256-273. Springer, 2018. Google Scholar
  10. Ho-Lin Chen, David Doty, and David Soloveichik. Deterministic function computation with chemical reaction networks. Natural computing, 13(4):517-534, 2014. Google Scholar
  11. Ho-Lin Chen, David Doty, and David Soloveichik. Rate-independent computation in continuous chemical reaction networks. In Proceedings of the 5th conference on Innovations in theoretical computer science, pages 313-326. ACM, 2014. Google Scholar
  12. 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(10):755, 2013. Google Scholar
  13. Kevin M Cherry and Lulu Qian. Scaling up molecular pattern recognition with DNA-based winner-take-all neural networks. Nature, 559(7714):370, 2018. Google Scholar
  14. Ben Chugg, Anne Condon, and Hooman Hashemi. Output-oblivious stochastic chemical reaction networks. arXiv preprint arXiv:1812.04401, 2018. Google Scholar
  15. Edmund M. Clarke, Orna Grumberg, Daniel Kroening, Doron Peled, and Helmut Veith. Model Checking. MIT Press, 2018. Google Scholar
  16. CRNs Exposed Github Page. URL: https://github.com/marko-vasic/crnsExposed.
  17. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008. Google Scholar
  18. Anastasia C Deckard, Frank T Bergmann, and Herbert M Sauro. Enumeration and online library of mass-action reaction networks. arXiv preprint arXiv:0901.3067, 2009. Google Scholar
  19. Greg Dennis, Felix Sheng-Ho Chang, and Daniel Jackson. Modular verification of code with SAT. In ISSTA, 2006. Google Scholar
  20. Niklas Een and Niklas Sorensson. An extensible SAT-solver. In SAT03, Santa Margherita Ligure, Italy, 2003. Google Scholar
  21. Marcelo F. Frias, Juan P. Galeotti, Carlos G. López Pombo, and Nazareno M. Aguirre. DynAlloy: Upgrading Alloy with actions. In ICSE, 2005. Google Scholar
  22. Juan P. Galeotti, Nicolás Rosner, Carlos G. López Pombo, and Marcelo F. Frias. TACO: efficient SAT-based bounded verification using symmetry breaking and tight bounds. TSE, 2013. Google Scholar
  23. Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposium on Security and Privacy (SP), 2018. Google Scholar
  24. Mirco Giacobbe, Călin C Guet, Ashutosh Gupta, Thomas A Henzinger, Tiago Paixão, and Tatjana Petrov. Model checking gene regulatory networks. In TACAS, 2015. Google Scholar
  25. Xavier Glorot, Antoine Bordes, and Yoshua Bengio. Deep sparse rectifier neural networks. In Proceedings of the fourteenth international conference on artificial intelligence and statistics, 2011. Google Scholar
  26. Patrice Godefroid. VeriSoft: A tool for the automatic analysis of concurrent reactive software. In CAV, pages 476-479. Springer, 1997. Google Scholar
  27. Richard HR Hahnloser, Rahul Sarpeshkar, Misha A Mahowald, Rodney J Douglas, and H Sebastian Seung. Digital selection and analogue amplification coexist in a cortex-inspired silicon circuit. Nature, 2000. Google Scholar
  28. Klaus Havelund and Thomas Pressburger. Model checking Java programs using Java pathfinder. International Journal on Software Tools for Technology Transfer, 2(4):366-381, 2000. Google Scholar
  29. John Heath, Marta Kwiatkowska, Gethin Norman, David Parker, and Oksana Tymchyshyn. Probabilistic model checking of complex biological pathways. Theoretical Computer Science, 2008. Google Scholar
  30. Gerard J Holzmann. The SPIN model checker: Primer and reference manual, volume 1003. Addison-Wesley Reading, 2004. Google Scholar
  31. De-An Huang, Jie-Hong R. Jiang, Ruei-Yang Huang, and Chi-Yun Cheng. Compiling program control flows into biochemical reactions. In Proceedings of the International Conference on Computer-Aided Design, pages 361-368, 2012. Google Scholar
  32. Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety verification of deep neural networks. In CAV, 2017. Google Scholar
  33. Daniel Jackson. Alloy: A lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology (TOSEM), 11(2):256-290, 2002. Google Scholar
  34. Daniel Jackson and Alan Fekete. Lightweight analysis of object interactions. In TACS, 2001. Google Scholar
  35. Daniel Jackson, Ian Schechter, and Ilya Shlyakhter. ALCOA: The Alloy constraint analyzer. In International Conference on Software Engineering, Limerick, Ireland, June 2000. Google Scholar
  36. Daniel Jackson and Mandana Vaziri. Finding bugs with a constraint solver. In ISSTA, 2000. Google Scholar
  37. Eunsuk Kang, Aleksandar Milicevic, and Daniel Jackson. Multi-representational security analysis. In FSE, 2016. Google Scholar
  38. Sarfraz Khurshid, Darko Marinov, and Daniel Jackson. An analyzable annotation language. In ACM SIGPLAN Notices, volume 37, pages 231-245. ACM, 2002. Google Scholar
  39. Sarfraz Khurshid, Darko Marinov, Ilya Shlyakhter, and Daniel Jackson. A case for efficient solution enumeration. In Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT), Santa Margherita Ligure, Italy, May 2003. Google Scholar
  40. 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, 2012. Google Scholar
  41. Yann LeCun, Yoshua Bengio, and Geoffrey Hinton. Deep learning. Nature, 2015. Google Scholar
  42. Tong Ihn Lee, Nicola J Rinaldi, François Robert, Duncan T Odom, Ziv Bar-Joseph, Georg K Gerber, Nancy M Hannett, Christopher T Harbison, Craig M Thompson, Itamar Simon, et al. Transcriptional regulatory networks in saccharomyces cerevisiae. Science, 298(5594):799-804, 2002. Google Scholar
  43. Marcelo O Magnasco. Chemical kinetics is Turing universal. Physical Review Letters, 78(6):1190, 1997. Google Scholar
  44. Darko Marinov and Sarfraz Khurshid. TestEra: A novel framework for automated testing of Java programs. In ASE, pages 22-31, 2001. Google Scholar
  45. Brendan D. McKay and Adolfo Piperno. Practical graph isomorphism, II. Journal of Symbolic Computation, 2014. Google Scholar
  46. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In 39th Design Automation Conference (DAC), 2001. Google Scholar
  47. Niall Murphy, Rasmus Petersen, Andrew Phillips, Boyan Yordanov, and Neil Dalchau. Synthesizing and tuning stochastic chemical reaction networks with specified behaviours. Journal of The Royal Society Interface, 15(145):20180283, 2018. Google Scholar
  48. Jason Ptacek, Geeta Devgan, Gregory Michaud, Heng Zhu, Xiaowei Zhu, Joseph Fasolo, Hong Guo, Ghil Jona, Ashton Breitkreutz, Richelle Sopko, et al. Global analysis of protein phosphorylation in yeast. Nature, 438(7068):679, 2005. Google Scholar
  49. Lulu Qian and Erik Winfree. Scaling up digital circuit computation with DNA strand displacement cascades. Science, 332(6034):1196-1201, 2011. Google Scholar
  50. Lulu Qian and Erik Winfree. A simple DNA gate motif for synthesizing large-scale circuits. Journal of the Royal Society Interface, 8(62):1281-1297, 2011. Google Scholar
  51. Sayed Ahmad Salehi, Keshab K. Parhi, and Marc D. Riedel. Chemical reaction networks for computing polynomials. ACS Synthetic Biology, 6(1):76-83, 2017. Google Scholar
  52. Eric E Severson, David Haley, and David Doty. Composable computation in discrete chemical reaction networks. In Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, pages 14-23, 2019. Google Scholar
  53. Shalin Shah, Jasmine Wee, Tianqi Song, Luis Ceze, Karin Strauss, Yuan-Jyue Chen, and John Reif. Using strand displacing polymerase to program chemical reaction networks. Journal of the American Chemical Society, 2020. Google Scholar
  54. Ilya Shlyakhter. Generating effective symmetry-breaking predicates for search problems. In Proc. Workshop on Theory and Applications of Satisfiability Testing, June 2001. Google Scholar
  55. David Soloveichik, Georg Seelig, and Erik Winfree. DNA as a universal substrate for chemical kinetics. Proceedings of the National Academy of Sciences, 107(12):5393-5398, 2010. Google Scholar
  56. Carlo Spaccasassi, Boyan Yordanov, Andrew Phillips, and Neil Dalchau. Fast enumeration of non-isomorphic chemical reaction networks. In CMSB, pages 224-247. Springer, 2019. Google Scholar
  57. Niranjan Srinivas, James Parkin, Georg Seelig, Erik Winfree, and David Soloveichik. Enzyme-free nucleic acid dynamical systems. Science, 358(6369):eaal2052, 2017. Google Scholar
  58. Marko Vasic, Cameron Chalk, Sarfraz Khurshid, and David Soloveichik. Deep Molecular Programming: A Natural Implementation of Binary-Weight ReLU Neural Networks. In International Conference on Machine Learning, 2020. Google Scholar
  59. Marko Vasic, David Soloveichik, and Sarfraz Khurshid. CRN++: molecular programming language. In International Conference on DNA Computing and Molecular Programming, pages 1-18. Springer, 2018. Google Scholar
  60. Vito Volterra. Variazioni e fluttuazioni del numero d'individui in specie animali conviventi. C. Ferrari, 1927. Google Scholar
  61. Qinsi Wang, Paolo Zuliani, Soonho Kong, Sicun Gao, and Edmund M Clarke. Sreach: A probabilistic bounded delta-reachability analyzer for stochastic hybrid systems. In CMSB, 2015. Google Scholar
  62. Thomas Wilhelm. The smallest chemical reaction system with bistability. BMC systems biology, 3(1):90, 2009. Google Scholar
  63. Thomas Wilhelm and Reinhart Heinrich. Smallest chemical reaction system with hopf bifurcation. Journal of mathematical chemistry, 17(1):1-14, 1995. Google Scholar
  64. David Yu Zhang and Georg Seelig. Dynamic DNA nanotechnology using strand-displacement reactions. Nature chemistry, 3(2):103, 2011. Google Scholar
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact