Document Open Access Logo

Population-Induced Phase Transitions and the Verification of Chemical Reaction Networks

Authors James I. Lathrop, Jack H. Lutz, Robyn R. Lutz, Hugh D. Potter, Matthew R. Riley

PDF
Thumbnail PDF

File

LIPIcs.DNA.2020.5.pdf
  • Filesize: 0.6 MB
  • 17 pages

Document Identifiers

Author Details

James I. Lathrop
  • Iowa State University, Ames, IA, USA
Jack H. Lutz
  • Iowa State University, Ames, IA, USA
Robyn R. Lutz
  • Iowa State University, Ames, IA, USA
Hugh D. Potter
  • Iowa State University, Ames, IA, USA
Matthew R. Riley
  • Iowa State University, Ames, IA, USA

Funding

This research was supported in part by National Science Foundation grants 1545028, 1900716, and 1909688.

Acknowledgements

The second and third authors thank Erik Winfree for his hospitality while they did part of this work during a 2020 sabbatical visit at Caltech. We thank Neil Lutz for technical assistance. We thank the reviewers for detailed suggestions that have improved our exposition, both here and in an expansion of this paper in preparation.

Cite AsGet BibTex

James I. Lathrop, Jack H. Lutz, Robyn R. Lutz, Hugh D. Potter, and Matthew R. Riley. Population-Induced Phase Transitions and the Verification 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. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.DNA.2020.5

Abstract

We show that very simple molecular systems, modeled as chemical reaction networks, can have behaviors that exhibit dramatic phase transitions at certain population thresholds. Moreover, the magnitudes of these thresholds can thwart attempts to use simulation, model checking, or approximation by differential equations to formally verify the behaviors of such systems at realistic populations. We show how formal theorem provers can successfully verify some such systems at populations where other verification methods fail.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
Keywords
  • chemical reaction networks
  • molecular programming
  • phase transitions
  • population protocols
  • verification

Metrics

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

References

  1. Parosh Aziz Abdulla, A. Prasad Sistla, and Muralidhar Talupur. Model checking parameterized systems. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 685-725. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_21.
  2. David F. Anderson and Thomas G. Kurtz. Continuous time Markov chain models for chemical reaction networks. In Heinz Koeppl, Gianluca Setti, Mario di Bernardo, and Douglas Densmore, editors, Design and Analysis of Biomolecular Circuits, pages 3-42. Springer, 2011. Google Scholar
  3. David F. Anderson and Thomas G. Kurtz. Stochastic Analysis of Biochemical Systems. Springer, 2015. Google Scholar
  4. 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
  5. Dana Angluin, James Aspnes, David Eisenstat, and Eric Ruppert. The computational power of population protocols. Distributed Computing, 20(4):279-304, 2007. Google Scholar
  6. Stefan Badelt, Seung Woo Shin, Robert F. Johnson, Qing Dong, Chris Thachuk, and Erik Winfree. A general-purpose CRN-to-DSD compiler with formal verification, optimization, and simulation capabilities. In Proceedings of the 23rd International Conference on DNA Computing and Molecular Programming, Springer, pages 232-248, 2017. Google Scholar
  7. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking (Representation and Mind Series). The MIT Press, 2008. Google Scholar
  8. Luca Bortolussi, Luca Cardelli, Marta Kwiatkowska, and Luca Laurenti. Central limit model checking. ACM Trans. Comput. Log., 20(4):19:1-19:35, 2019. URL: https://doi.org/10.1145/3331452.
  9. Sarah Cannon, Sarah Miracle, and Dana Randall. Phase transitions in random dyadic tilings and rectangular dissections. SIAM J. Discret. Math., 32(3):1966-1992, 2018. URL: https://doi.org/10.1137/17M1157118.
  10. Luca Cardelli and Attila Csikász-Nagy. The cell cycle switch computes approximate majority. Scientific Reports, 2, 2012. Google Scholar
  11. Luca Cardelli, Marta Kwiatkowska, and Max Whitby. Chemical reaction network designs for asynchronous logic circuits. Natural Computing, 17(1):109-130, 2018. URL: https://doi.org/10.1007/s11047-017-9665-7.
  12. Nathalie Cauchi, Luca Laurenti, Morteza Lahijanian, Alessandro Abate, Marta Kwiatkowska, and Luca Cardelli. Efficiency through uncertainty: scalable formal synthesis for stochastic hybrid systems. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, April 16-18, 2019., pages 240-251, 2019. URL: https://doi.org/10.1145/3302504.3311805.
  13. Milan Ceska, Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen. Shepherding hordes of Markov chains. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 172-190. Springer, 2019. Google Scholar
  14. 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-762, 2013. Google Scholar
  15. Philipp Chrszon, Clemens Dubslaff, Sascha Klüppelholz, and Christel Baier. ProFeat: feature-oriented engineering for family-based probabilistic model checking. Formal Asp. Comput., 30(1):45-75, 2018. URL: https://doi.org/10.1007/s00165-017-0432-4.
  16. Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis. Model checking: algorithmic verification and debugging. Commun. ACM, 52(11):74-84, 2009. URL: https://doi.org/10.1145/1592761.1592781.
  17. Anne Condon, Monir Hajiaghayi, David G. Kirkpatrick, and Ján Manuch. Simplifying analyses of chemical reaction networks for approximate majority. In Proceedings of the 23rd International Conference on DNA Computing and Molecular Programming, pages 188-209. Springer, 2017. Google Scholar
  18. Matthew Cook, David Soloveichik, Erik Winfree, and Jehoshua Bruck. Programmability of chemical reaction networks. In Anne Condon, David Harel, Joost N. Kok, Arto Salomaa, and Erik Winfree, editors, Algorithmic Bioprocesses, Natural Computing Series, pages 543-584. Springer, 2009. Google Scholar
  19. Shawn M. Douglas, Ido Bachelet, and George M. Church. A logic-gated nanorobot for targeted transport of molecular payloads. Science, 335(6070):831-834, 2012. Google Scholar
  20. Samuel J. Ellis, Titus H. Klinge, James I. Lathrop, Jack H. Lutz, Robyn R. Lutz, Andrew S. Miner, and Hugh D. Potter. Runtime fault detection in programmed molecular systems. ACM Trans. Softw. Eng. Methodol., 28(2):6:1-6:20, 2019. URL: https://doi.org/10.1145/3295740.
  21. François Fages, Guillaume Le Guludec, Olivier Bournez, and Amaury Pouly. Strong Turing completeness of continuous chemical reaction networks and compilation of mixed analog-digital programs. In Proceedings of the 15th International Conference on Computational Methods in Systems Biology, pages 108-127. Springer, 2017. Google Scholar
  22. David Harel. Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness. J. ACM, 33(1):224-248, 1986. URL: https://doi.org/10.1145/4904.4993.
  23. J. Heath, M. Kwiatkowska, G. Norman, D. Parker, and O. Tymchyshyn. Probabilistic model checking of complex biological pathways. In Computational Methods in Systems Biology, pages 32-47, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  24. Daniel Jackson. Alloy: a language and tool for exploring software designs. Commun. ACM, 62(9):66-76, 2019. URL: https://doi.org/10.1145/3338843.
  25. Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, pages 1-35. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_1.
  26. Dexter Kozen. Theory of Computation. Texts in Computer Science. Springer, 2006. URL: https://doi.org/10.1007/1-84628-477-5.
  27. Thomas G. Kurtz. The relationship between stochastic and deterministic models for chemical reactions. The Journal of Chemical Physics, 57(7):2976-2978, 1972. Google Scholar
  28. Marta Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In Proceedings of the 23rd International Conference on Computer Aided Verification, pages 585-591. Springer, 2011. Google Scholar
  29. Marta Kwiatkowska and Chris Thachuk. Probabilistic model checking for biology. Software Systems Safety, 36:165-189, 2014. Google Scholar
  30. Marta Z. Kwiatkowska. Survey of fairness notions. Information and Software Technology, 31(7):371-386, 1989. URL: https://doi.org/10.1016/0950-5849(89)90159-6.
  31. 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. Google Scholar
  32. Suping Li, Qiao Jiang, Shaoli Liu, Yinlong Zhang, Yanhua Tian, Chen Song, Jing Wang, Yiguo Zou, Gregory J Anderson, Jing-Yan Han, Yung Chang, Yan Liu, Chen Zhang, Liang Chen, Guangbiao Zhou, Guangjun Nie, Hao Yan, Baoquan Ding, and Yuliang Zhao. A DNA nanorobot functions as a cancer therapeutic in response to a molecular trigger in vivo. Nature Biotechnology, 36:258, 2018. Google Scholar
  33. Xiaowei Liu, Yan Liu, and Hao Yan. Functionalized DNA nanostructures for nanomedicine. Israel Journal of Chemistry, 53(8):555-566, 2013. Google Scholar
  34. Alessio Lomuscio and Edoardo Pirovano. A counter abstraction technique for the verification of probabilistic swarm systems. In Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS'19, pages 161-169, 2019. URL: http://dl.acm.org/citation.cfm?id=3331689.
  35. MATLAB. version 9.7.0 (R2019b, Update 4). The MathWorks Inc., Natick, Massachusetts, 2019. Google Scholar
  36. Melissa B. Miller and Bonnie L. Bassler. Quorum sensing in bacteria. Annual Review of Microbiology, 55(1):165-199, 2001. PMID: 11544353. URL: https://doi.org/10.1146/annurev.micro.55.1.165.
  37. Cristopher Moore and Stephan Mertens. The Nature of Computation. Oxford University Press, 2011. Google Scholar
  38. Yakoub Nemouchi, Simon Foster, Mario Gleirscher, and Tim Kelly. Isabelle/SACM: Computer-assisted assurance cases with integrated formal methods. In Proceedings of the 15th International Conference on Integrated Formal MethodsIFM 2019, pages 379-398. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-34968-4_21.
  39. Tobias Nipkow and Gerwin Klein. Concrete Semantics-With Isabelle/HOL. Springer, 2014. Google Scholar
  40. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL, volume 2283 of Lecture Notes in Computer Science. Springer-Verlag Berlin Heidelberg, 1 edition, 2002. Google Scholar
  41. Lawrence C. Paulson, Tobias Nipkow, and Makarius Wenzel. From LCF to Isabelle/HOL. Formal Asp. Comput., 31(6):675-698, 2019. URL: https://doi.org/10.1007/s00165-019-00492-1.
  42. Esteban Pavese, Víctor Braberman, and Sebastián Uchitel. Less is more: Estimating probabilistic rewards over partial system explorations. ACM Transactions on Software Engineering and Methodology, 25(2):16:1-16:47, 2016. Google Scholar
  43. Gerald Pollack and Wei-Chun Chin, editors. Phase Transitions in Cell Biology. Springer, 2008. Google Scholar
  44. Hamid Ramezani and Hendrik Dietz. Building machines with DNA molecules. Nature Reviews Genetics, 21(1):5-26, 2020. Google Scholar
  45. Dana Randall. Phase transitions in sampling algorithms and the underlying random structures. In Haim Kaplan, editor, Proceedings Scandinavian Symposium and Workshops on Algorithm Theory SWAT, page 309. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-13731-0_29.
  46. Dana Randall. Phase Transitions and Emergent Phenomena in Random Structures and Algorithms (Keynote Talk). In 31st International Symposium on Distributed Computing (DISC 2017), pages 3:1-3:2. Schloss Dagstuhl LZI, 2017. URL: https://doi.org/10.4230/LIPIcs.DISC.2017.3.
  47. Dana Randall. Statistical Physics and Algorithms (Invited Talk). In Christophe Paul and Markus Bläser, editors, 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020), pages 1:1-1:6. Schloss Dagstuhl LZI, 2020. Google Scholar
  48. H. G. Rice. Classes of Recursively Enumerable Sets and Their Decision Problems. PhD thesis, Syracuse University, 1951. Google Scholar
  49. H. G. Rice. Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society, 74:358-366, 1953. URL: https://doi.org/10.1090/s0002-9947-1953-0053041-6.
  50. Apoorva Sarode, Akshaya Annapragada, Junling Guo, and Samir Mitragotri. Layered self-assemblies for controlled drug delivery: A translational overview. Biomaterials, 242:119929, 2020. URL: https://doi.org/10.1016/j.biomaterials.2020.119929.
  51. David Soloveichik, Matthew Cook, Erik Winfree, and Jehoshua Bruck. Computation with finite stochastic chemical reaction networks. Natural Computing, 7(4):615-633, 2008. Google Scholar
  52. David Soloveichik, Georg Seelig, and Erik Winfree. DNA as a universal substrate for chemical kinetics. In Proceedings of the 14th International Meeting on DNA Computing, pages 57-69. Springer, 2009. Google Scholar
  53. Anupama J. Thubagere, Chris Thachuk, Joseph Berleant, Robert F. Johnson, Diana A. Ardelean, Kevin M. Cherry, and Lulu Qian. Compiler-aided systematic construction of large-scale DNA strand displacement circuits using unpurified components. Nature Communications, 8, 2017. Google Scholar
  54. John C. Wooley and Herbert S. Lin. Catalyzing Inquiry at the Interface of Computing and Biology. National Academies Press, 2005. Google Scholar
  55. David Yu Zhang and Georg Seelig. Dynamic DNA nanotechnology using strand-displacement reactions. Nature Chemistry, 3(2):103-113, 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