Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Natural Computing

17-11-2021

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

Published in: Natural Computing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
Appendix
Available only for authorised users
Literature
Abdulla PA, Sistla AP, Talupur M (2018) Model checking parameterized systems. In: Clarke EM, Henzinger TA, Veith H, Bloem R (eds) Handbook of Model Checking. Springer, pp 685–725
Anderson DF, Kurtz TG (2011) Continuous time Markov chain models for chemical reaction networks. In: Heinz K, Gianluca S, Mario di B, Douglas D, (eds) Design and Analysis of Biomolecular Circuits. Springer, pp 3–42
Anderson DF, Kurtz TG (eds) (2015) Stochastic analysis of biochemical systems, volume 1.2. Springer International Publishing
Angluin D, Aspnes J, Eisenstat D (2008) A simple population protocol for fast robust approximate majority. Distrib Comput 21(2):87–102CrossRef
Angluin D, Aspnes J, Eisenstat D, Ruppert E (2007) The computational power of population protocols. Distrib Comput 20(4):279–304CrossRef
Badelt S, Shin SW, Johnson RF, Dong Q, Thachuk C, Winfree E (2017) 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, Lecture Notes in Computer Science, pp 232–248
Baier C, Katoen J-P (2008) Principles of model checking (Representation and mind series). The MIT Press, USAMATH
Bortolussi L, Cardelli L, Kwiatkowska M, Laurenti L (2019) Central limit model checking. ACM Trans Comput Log 20(4):19:1-19:35
Cannon S, Miracle S, Randall D (2018) Phase transitions in random dyadic tilings and rectangular dissections. SIAM J Discret Math 32(3):1966–1992MathSciNetCrossRef
Cardelli L, Csikász-Nagy A (2012) The cell cycle switch computes approximate majority. Scientific Reports, 2
Cardelli L, Kwiatkowska M, Whitby M (2016) Chemical reaction network designs for asynchronous logic circuits. In: International Conference on DNA-Based Computers. Springer, pp 67–81
Cardelli L, Kwiatkowska M, Whitby M (2018) Chemical reaction network designs for asynchronous logic circuits. Nat Comput 17(1):109–130MathSciNetCrossRef
Cauchi N, Laurenti L, Lahijanian M, Abate A, Kwiatkowska M, Cardelli L (2019) 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., pp 240–251
Ceska M, Jansen N, Junges S, Katoen JP (2019) 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
Chen Y-J, Dalchau N, Srinivas N, Phillips A, Cardelli L, Soloveichik D, Seelig G (2013) Programmable chemical controllers made from DNA. Nat Nanotechnol 8(10):755–762CrossRef
Chrszon P, Dubslaff C, Klüppelholz S, Baier C (2018) ProFeat: feature-oriented engineering for family-based probabilistic model checking. Formal Asp Comput 30(1):45–75MathSciNetCrossRef
Clarke EM, Allen Emerson E, Sifakis J (2009) Model checking: algorithmic verification and debugging. Commun ACM 52(11):74–84CrossRef
Condon A, Hajiaghayi M, Kirkpatrick DG, Manuch J (2017) Simplifying analyses of chemical reaction networks for approximate majority. In: Proceedings of the 23rd International Conference on DNA Computing and Molecular Programming, volume 10467 of Lecture Notes in Computer Science, pages 188–209. Springer
Cook M, Soloveichik D, Winfree E, Bruck J (2009) Programmability of chemical reaction networks. In: Condon A, Harel D, Kok JN, Salomaa A, Winfree E (eds) Algorithmic Bioprocesses. Springer, Natural Computing Series, pp 543–584CrossRef
Dietz H. Synthetic DNA machines to fight viruses and other troubles. Matter to Life Lecture Series, Technical University of Munich
Douglas SM, Bachelet I, Church GM (2012) A logic-gated nanorobot for targeted transport of molecular payloads. Science 335(6070):831–834CrossRef
Ellis SJ, Klinge TH, Lathrop JI, Lutz JH, Lutz RR, Miner AS, Potter HD (2019) Runtime fault detection in programmed molecular systems. ACM Trans Softw Eng Methodol 28(2):6:1-6:20
Fages F, Le Guludec G, Bournez O, Pouly A (2017) 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 International Publishing
Harel D (1986) Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness. J ACM 33(1):224–248MathSciNetCrossRef
Heath J, Kwiatkowska M, Norman G, Parker D, Tymchyshyn O (2006) Probabilistic model checking of complex biological pathways. In: Computational Methods in Systems Biology, pages 32–47, Berlin, Heidelberg. Springer Berlin Heidelberg
Jackson D (2019) Alloy: a language and tool for exploring software designs. Commun ACM 62(9):66–76CrossRef
Kovács L, Voronkov A (2013) First-order theorem proving and vampire. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 1–35. Springer
Kozen D (2006) Theory of computation. Texts in Computer Science. Springer
Kurtz TG (1972) The relationship between stochastic and deterministic models for chemical reactions. J Chem Phys 57(7):2976–2978CrossRef
Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: Verification of probabilistic real-time systems. In: Proceedings of the 23rd International Conference on Computer Aided Verification, volume 6806 of Lecture Notes in Computer Science, pages 585–591. Springer
Kwiatkowska M, Thachuk C (2014) Probabilistic model checking for biology. Softw Syst Safety 36:165–189
Kwiatkowska MZ (1989) Survey of fairness notions. Inf Softw Technol 31(7):371–386CrossRef
Lakin MR, Parker D, Cardelli L, Kwiatkowska M, Phillips A (2012) Design and analysis of DNA strand displacement devices using probabilistic model checking. J R Soc Interface 9(72):1470–1485CrossRef
Lathrop JI, Lutz JH, Lutz RR, Potter HD, Riley MR (2020) Population-induced phase transitions and the verification of chemical reaction networks. In: 26th International Conference on DNA Computing and Molecular Programming, LIPIcs, pages 5:1–5:17. Schloss Dagstuhl
Li S, Jiang Q, Liu S, Zhang Y, Tian Y, Song C, Wang J, Zou Y, Anderson GJ, Han J-Y, Chang Y, Liu Y, Zhang C, Chen L, Zhou G, Nie G, Yan H, Ding B, Zhao Y (2018) A DNA nanorobot functions as a cancer therapeutic in response to a molecular trigger in vivo. Nat Biotechnol 36:258CrossRef
Liu X, Liu Y, Yan H (2013) Functionalized DNA nanostructures for nanomedicine. Isr J Chem 53(8):555–566CrossRef
Lomuscio A, Pirovano E (2019) 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
MATLAB (2019) version 9.7.0 (R2019b, Update 4). The MathWorks Inc., Natick, Massachusetts
Miller B, Bassler L (2001) Quorum sensing in bacteria. Annu Rev Microbiol 55(1):165–199 (PMID: 11544353)CrossRef
Nemouchi Y, Foster S, Gleirscher M, Kelly T (2019) Isabelle/SACM: Computer-assisted assurance cases with integrated formal methods. In: Proceedings of the 15th International Conference on Integrated Formal MethodsIFM 2019, volume 11918 of Lecture Notes in Computer Science, pages 379–398. Springer
Nipkow T, Klein G (2014) Concrete semantics-With Isabelle/HOL. Springer, BerlinMATH
Nipkow T, Paulson LC, Wenzel M (2002) Isabelle/HOL, volume 2283 of Lecture Notes in Computer Science. Springer-Verlag Berlin Heidelberg, 1 edition
Pavese E, Braberman V, Uchitel S (2016) Less is more: Estimating probabilistic rewards over partial system explorations. ACM Trans Softw Eng Methodol 25(2):16:1-16:47
Dana R (2010) Phase transitions in sampling algorithms and the underlying random structures. In: Kaplan H (ed) Proceedings Scandinavian Symposium and Workshops on Algorithm Theory SWAT, vol 6139. Lecture Notes in Computer Science, page 309. Springer
Randall D (2017) Phase Transitions and Emergent Phenomena in Random Structures and Algorithms (Keynote Talk). In: 31st International Symposium on Distributed Computing (DISC 2017), volume 91 of Leibniz International Proceedings in Informatics (LIPIcs), pages 3:1–3:2. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik,
Rice HG (1951) Classes of recursively enumerable sets and their decision problems. Ph.D thesis, Syracuse University
Apoorva S, Akshaya A, Junling G, Samir M (2020) Layered self-assemblies for controlled drug delivery: A translational overview. Biomaterials 242:119929CrossRef
Soloveichik D, Cook M, Winfree E, Bruck J (2008) Computation with finite stochastic chemical reaction networks. Nat Comput 7(4):615–633MathSciNetCrossRef
Soloveichik D, Seelig G, Winfree E (2009) DNA as a universal substrate for chemical kinetics. In: Proceedings of the 14th International Meeting on DNA Computing, volume 5347 of Lecture Notes in Computer Science, pages 57–69. Springer
Thubagere AJ, Thachuk C, Berleant J, Johnson RF, Ardelean DA, Cherry KM, Qian L (2017) Compiler-aided systematic construction of large-scale DNA strand displacement circuits using unpurified components. Nature Communications, 8
Wooley John C, Lin Herbert S (2005) Catalyzing inquiry at the interface of computing and biology. National Academies Press, USA
Zhang DY, Seelig G (2011) Dynamic DNA nanotechnology using strand-displacement reactions. Nat Chem 3(2):103–113CrossRef
Metadata
Title
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
Publication date
17-11-2021
Publisher
Springer Netherlands
Published in
Natural Computing
Print ISSN: 1567-7818
Electronic ISSN: 1572-9796
DOI
https://doi.org/10.1007/s11047-021-09877-9

Premium Partner

    Image Credits