{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T16:29:50Z","timestamp":1746289790096,"version":"3.37.3"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2021,11,17]],"date-time":"2021-11-17T00:00:00Z","timestamp":1637107200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2021,11,17]],"date-time":"2021-11-17T00:00:00Z","timestamp":1637107200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1545028","1900716"],"award-info":[{"award-number":["1545028","1900716"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1909688"],"award-info":[{"award-number":["1909688"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Nat Comput"],"published-print":{"date-parts":[[2024,6]]},"DOI":"10.1007\/s11047-021-09877-9","type":"journal-article","created":{"date-parts":[[2021,11,17]],"date-time":"2021-11-17T06:03:41Z","timestamp":1637129021000},"page":"347-363","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Population-induced phase transitions and the verification of chemical reaction networks"],"prefix":"10.1007","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5467-5818","authenticated-orcid":false,"given":"James I.","family":"Lathrop","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1004-3891","authenticated-orcid":false,"given":"Jack H.","family":"Lutz","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5390-7982","authenticated-orcid":false,"given":"Robyn R.","family":"Lutz","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4437-674X","authenticated-orcid":false,"given":"Hugh D.","family":"Potter","sequence":"additional","affiliation":[]},{"given":"Matthew R.","family":"Riley","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,11,17]]},"reference":[{"key":"9877_CR1","doi-asserted-by":"crossref","unstructured":"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\u2013725","DOI":"10.1007\/978-3-319-10575-8_21"},{"key":"9877_CR2","doi-asserted-by":"crossref","unstructured":"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\u201342","DOI":"10.1007\/978-1-4419-6766-4_1"},{"key":"9877_CR3","doi-asserted-by":"crossref","unstructured":"Anderson DF, Kurtz TG (eds) (2015) Stochastic analysis of biochemical systems, volume 1.2. Springer International Publishing","DOI":"10.1007\/978-3-319-16895-1"},{"issue":"2","key":"9877_CR4","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/s00446-008-0059-z","volume":"21","author":"D Angluin","year":"2008","unstructured":"Angluin D, Aspnes J, Eisenstat D (2008) A simple population protocol for fast robust approximate majority. Distrib Comput 21(2):87\u2013102","journal-title":"Distrib Comput"},{"issue":"4","key":"9877_CR5","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s00446-007-0040-2","volume":"20","author":"D Angluin","year":"2007","unstructured":"Angluin D, Aspnes J, Eisenstat D, Ruppert E (2007) The computational power of population protocols. Distrib Comput 20(4):279\u2013304","journal-title":"Distrib Comput"},{"key":"9877_CR6","doi-asserted-by":"crossref","unstructured":"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\u2013248","DOI":"10.1007\/978-3-319-66799-7_15"},{"key":"9877_CR7","volume-title":"Principles of model checking (Representation and mind series)","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J-P (2008) Principles of model checking (Representation and mind series). The MIT Press, USA"},{"key":"9877_CR8","doi-asserted-by":"crossref","unstructured":"Bortolussi L, Cardelli L, Kwiatkowska M, Laurenti L (2019) Central limit model checking. ACM Trans Comput Log 20(4):19:1-19:35","DOI":"10.1145\/3331452"},{"issue":"3","key":"9877_CR9","doi-asserted-by":"publisher","first-page":"1966","DOI":"10.1137\/17M1157118","volume":"32","author":"S Cannon","year":"2018","unstructured":"Cannon S, Miracle S, Randall D (2018) Phase transitions in random dyadic tilings and rectangular dissections. SIAM J Discret Math 32(3):1966\u20131992","journal-title":"SIAM J Discret Math"},{"key":"9877_CR10","doi-asserted-by":"crossref","unstructured":"Cardelli L, Csik\u00e1sz-Nagy A (2012) The cell cycle switch computes approximate majority. Scientific Reports, 2","DOI":"10.1038\/srep00656"},{"key":"9877_CR11","doi-asserted-by":"crossref","unstructured":"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\u201381","DOI":"10.1007\/978-3-319-43994-5_5"},{"issue":"1","key":"9877_CR12","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s11047-017-9665-7","volume":"17","author":"L Cardelli","year":"2018","unstructured":"Cardelli L, Kwiatkowska M, Whitby M (2018) Chemical reaction network designs for asynchronous logic circuits. Nat Comput 17(1):109\u2013130","journal-title":"Nat Comput"},{"key":"9877_CR13","doi-asserted-by":"crossref","unstructured":"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\u2013251","DOI":"10.1145\/3302504.3311805"},{"key":"9877_CR14","doi-asserted-by":"crossref","unstructured":"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\u2013190. Springer","DOI":"10.1007\/978-3-030-17465-1_10"},{"issue":"10","key":"9877_CR15","doi-asserted-by":"publisher","first-page":"755","DOI":"10.1038\/nnano.2013.189","volume":"8","author":"Y-J Chen","year":"2013","unstructured":"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\u2013762","journal-title":"Nat Nanotechnol"},{"issue":"1","key":"9877_CR16","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s00165-017-0432-4","volume":"30","author":"P Chrszon","year":"2018","unstructured":"Chrszon P, Dubslaff C, Kl\u00fcppelholz S, Baier C (2018) ProFeat: feature-oriented engineering for family-based probabilistic model checking. Formal Asp Comput 30(1):45\u201375","journal-title":"Formal Asp Comput"},{"issue":"11","key":"9877_CR17","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/1592761.1592781","volume":"52","author":"EM Clarke","year":"2009","unstructured":"Clarke EM, Allen Emerson E, Sifakis J (2009) Model checking: algorithmic verification and debugging. Commun ACM 52(11):74\u201384","journal-title":"Commun ACM"},{"key":"9877_CR18","doi-asserted-by":"crossref","unstructured":"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\u2013209. Springer","DOI":"10.1007\/978-3-319-66799-7_13"},{"key":"9877_CR19","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-540-88869-7_27","volume-title":"Algorithmic Bioprocesses","author":"M Cook","year":"2009","unstructured":"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\u2013584"},{"key":"9877_CR20","unstructured":"Dietz H. Synthetic DNA machines to fight viruses and other troubles. Matter to Life Lecture Series, Technical University of Munich"},{"issue":"6070","key":"9877_CR21","doi-asserted-by":"publisher","first-page":"831","DOI":"10.1126\/science.1214081","volume":"335","author":"SM Douglas","year":"2012","unstructured":"Douglas SM, Bachelet I, Church GM (2012) A logic-gated nanorobot for targeted transport of molecular payloads. Science 335(6070):831\u2013834","journal-title":"Science"},{"key":"9877_CR22","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1145\/3295740"},{"key":"9877_CR23","doi-asserted-by":"crossref","unstructured":"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\u2013127. Springer International Publishing","DOI":"10.1007\/978-3-319-67471-1_7"},{"issue":"1","key":"9877_CR24","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1145\/4904.4993","volume":"33","author":"D Harel","year":"1986","unstructured":"Harel D (1986) Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness. J ACM 33(1):224\u2013248","journal-title":"J ACM"},{"key":"9877_CR25","doi-asserted-by":"crossref","unstructured":"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\u201347, Berlin, Heidelberg. Springer Berlin Heidelberg","DOI":"10.1007\/11885191_3"},{"issue":"9","key":"9877_CR26","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/3338843","volume":"62","author":"D Jackson","year":"2019","unstructured":"Jackson D (2019) Alloy: a language and tool for exploring software designs. Commun ACM 62(9):66\u201376","journal-title":"Commun ACM"},{"key":"9877_CR27","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs 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\u201335. Springer","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"9877_CR28","unstructured":"Kozen D (2006) Theory of computation. Texts in Computer Science. Springer"},{"issue":"7","key":"9877_CR29","doi-asserted-by":"publisher","first-page":"2976","DOI":"10.1063\/1.1678692","volume":"57","author":"TG Kurtz","year":"1972","unstructured":"Kurtz TG (1972) The relationship between stochastic and deterministic models for chemical reactions. J Chem Phys 57(7):2976\u20132978","journal-title":"J Chem Phys"},{"key":"9877_CR30","doi-asserted-by":"crossref","unstructured":"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\u2013591. Springer","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"9877_CR31","first-page":"165","volume":"36","author":"M Kwiatkowska","year":"2014","unstructured":"Kwiatkowska M, Thachuk C (2014) Probabilistic model checking for biology. Softw Syst Safety 36:165\u2013189","journal-title":"Softw Syst Safety"},{"issue":"7","key":"9877_CR32","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/0950-5849(89)90159-6","volume":"31","author":"MZ Kwiatkowska","year":"1989","unstructured":"Kwiatkowska MZ (1989) Survey of fairness notions. Inf Softw Technol 31(7):371\u2013386","journal-title":"Inf Softw Technol"},{"issue":"72","key":"9877_CR33","doi-asserted-by":"publisher","first-page":"1470","DOI":"10.1098\/rsif.2011.0800","volume":"9","author":"MR Lakin","year":"2012","unstructured":"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\u20131485","journal-title":"J R Soc Interface"},{"key":"9877_CR34","unstructured":"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\u20135:17. Schloss Dagstuhl"},{"key":"9877_CR35","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1038\/nbt.4071","volume":"36","author":"S Li","year":"2018","unstructured":"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:258","journal-title":"Nat Biotechnol"},{"issue":"8","key":"9877_CR36","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1002\/ijch.201300002","volume":"53","author":"X Liu","year":"2013","unstructured":"Liu X, Liu Y, Yan H (2013) Functionalized DNA nanostructures for nanomedicine. Isr J Chem 53(8):555\u2013566","journal-title":"Isr J Chem"},{"key":"9877_CR37","unstructured":"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\u201919, pages 161\u2013169"},{"key":"9877_CR38","unstructured":"MATLAB (2019) version 9.7.0 (R2019b, Update 4). The MathWorks Inc., Natick, Massachusetts"},{"issue":"1","key":"9877_CR39","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1146\/annurev.micro.55.1.165","volume":"55","author":"B Miller","year":"2001","unstructured":"Miller B, Bassler L (2001) Quorum sensing in bacteria. Annu Rev Microbiol 55(1):165\u2013199 (PMID: 11544353)","journal-title":"Annu Rev Microbiol"},{"key":"9877_CR40","doi-asserted-by":"crossref","unstructured":"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\u2013398. Springer","DOI":"10.1007\/978-3-030-34968-4_21"},{"key":"9877_CR41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete semantics-With Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow T, Klein G (2014) Concrete semantics-With Isabelle\/HOL. Springer, Berlin"},{"key":"9877_CR42","doi-asserted-by":"crossref","unstructured":"Nipkow T, Paulson LC, Wenzel M (2002) Isabelle\/HOL, volume 2283 of Lecture Notes in Computer Science. Springer-Verlag Berlin Heidelberg, 1 edition","DOI":"10.1007\/3-540-45949-9"},{"issue":"6","key":"9877_CR43","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/s00165-019-00492-1","volume":"31","author":"LC Paulson","year":"2019","unstructured":"Paulson LC, Nipkow T, Wenzel M (2019) From LCF to Isabelle\/HOL. Formal Asp Comput 31(6):675\u2013698","journal-title":"Formal Asp Comput"},{"key":"9877_CR44","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1145\/2890494"},{"key":"9877_CR45","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/978-3-642-13731-0_29"},{"key":"9877_CR46","unstructured":"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\u20133:2. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik,"},{"key":"9877_CR47","unstructured":"Rice HG (1951) Classes of recursively enumerable sets and their decision problems. Ph.D thesis, Syracuse University"},{"key":"9877_CR48","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1090\/S0002-9947-1953-0053041-6","volume":"74","author":"HG Rice","year":"1953","unstructured":"Rice HG (1953) Classes of recursively enumerable sets and their decision problems. Trans Am Math Soc 74:358\u2013366","journal-title":"Trans Am Math Soc"},{"key":"9877_CR49","doi-asserted-by":"publisher","first-page":"119929","DOI":"10.1016\/j.biomaterials.2020.119929","volume":"242","author":"S Apoorva","year":"2020","unstructured":"Apoorva S, Akshaya A, Junling G, Samir M (2020) Layered self-assemblies for controlled drug delivery: A translational overview. Biomaterials 242:119929","journal-title":"Biomaterials"},{"issue":"4","key":"9877_CR50","doi-asserted-by":"publisher","first-page":"615","DOI":"10.1007\/s11047-008-9067-y","volume":"7","author":"D Soloveichik","year":"2008","unstructured":"Soloveichik D, Cook M, Winfree E, Bruck J (2008) Computation with finite stochastic chemical reaction networks. Nat Comput 7(4):615\u2013633","journal-title":"Nat Comput"},{"key":"9877_CR51","doi-asserted-by":"crossref","unstructured":"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\u201369. Springer","DOI":"10.1007\/978-3-642-03076-5_6"},{"key":"9877_CR52","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1038\/ncomms14373"},{"key":"9877_CR53","unstructured":"Erik Winfree (2020) personal communication"},{"key":"9877_CR54","volume-title":"Catalyzing inquiry at the interface of computing and biology","author":"C Wooley John","year":"2005","unstructured":"Wooley John C, Lin Herbert S (2005) Catalyzing inquiry at the interface of computing and biology. National Academies Press, USA"},{"issue":"2","key":"9877_CR55","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1038\/nchem.957","volume":"3","author":"DY Zhang","year":"2011","unstructured":"Zhang DY, Seelig G (2011) Dynamic DNA nanotechnology using strand-displacement reactions. Nat Chem 3(2):103\u2013113","journal-title":"Nat Chem"}],"container-title":["Natural Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11047-021-09877-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11047-021-09877-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11047-021-09877-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,2]],"date-time":"2024-08-02T19:06:57Z","timestamp":1722625617000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11047-021-09877-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,17]]},"references-count":55,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["9877"],"URL":"https:\/\/doi.org\/10.1007\/s11047-021-09877-9","relation":{},"ISSN":["1567-7818","1572-9796"],"issn-type":[{"type":"print","value":"1567-7818"},{"type":"electronic","value":"1572-9796"}],"subject":[],"published":{"date-parts":[[2021,11,17]]},"assertion":[{"value":"16 October 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 November 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}