{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T21:02:13Z","timestamp":1757451733760,"version":"3.41.0"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2014,12,30]],"date-time":"2014-12-30T00:00:00Z","timestamp":1419897600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Science Foundation","award":["CCF-0916105 and CCF-0916042"],"award-info":[{"award-number":["CCF-0916105 and CCF-0916042"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. Emerg. Technol. Comput. Syst."],"published-print":{"date-parts":[[2014,12,30]]},"abstract":"<jats:p>\n            Synthetic genetic circuits have a number of exciting potential applications such as cleaning up toxic waste, hunting and killing tumor cells, and producing drugs and bio-fuels more efficiently. When designing and analyzing genetic circuits, researchers are often interested in the probability of observing certain behaviors. Discerning these probabilities typically involves simulating the circuit to produce some time series data and computing statistics over the resulting data. However, for very rare behaviors of complex genetic circuits, it becomes computationally intractable to obtain good results as the number of required simulation runs grows exponentially. It is, therefore, necessary to apply numerical methods to determine these probabilities directly. This article describes how\n            <jats:italic>stochastic model checking<\/jats:italic>\n            , a method for determining the likelihood that certain events occur in a system, can by applied to models of genetic circuits by translating them into\n            <jats:italic>continuous-time Markov chains<\/jats:italic>\n            (CTMCs) and analyzing them using\n            <jats:italic>Markov chain analysis<\/jats:italic>\n            to check\n            <jats:italic>continuous stochastic logic<\/jats:italic>\n            (CSL) properties. The utility of this approach is demonstrated with several case studies illustrating how this method can be used to perform design space exploration of two genetic oscillators and two genetic state-holding elements. Our results show that this method results in a substantial speedup as compared with conventional simulation-based approaches.\n          <\/jats:p>","DOI":"10.1145\/2644817","type":"journal-article","created":{"date-parts":[[2015,1,5]],"date-time":"2015-01-05T13:27:09Z","timestamp":1420464429000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Stochastic Model Checking of Genetic Circuits"],"prefix":"10.1145","volume":"11","author":[{"given":"Curtis","family":"Madsen","sequence":"first","affiliation":[{"name":"Newcastle University, United Kingdom"}]},{"given":"Zhen","family":"Zhang","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, UT"}]},{"given":"Nicholas","family":"Roehner","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, UT"}]},{"given":"Chris","family":"Winstead","sequence":"additional","affiliation":[{"name":"Utah State University, Logon, UT"}]},{"given":"Chris","family":"Myers","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, UT"}]}],"member":"320","published-online":{"date-parts":[[2014,12,30]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jmb.2005.10.076"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1038\/nbt0708-771"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.copbio.2008.08.008"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343402"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/SASOW.2008.14"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1021\/sb400024s"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1371\/journal.pone.0018882"},{"key":"e_1_2_1_8_1","unstructured":"K. Burrage M. Hegland S. Macnamara and R. Sidje. 2006. A Krylov-based finite state projection algorithm for solving the chemical master equation arising in the discrete modelling of biological systems. In Mam 2006: Markov Anniversary Meeting: An International Conference to Celebrate the 150th Anniversary of the birth of A.A. Markov A. N. Langville and W. J. Stewart Eds. Boston Books Charleston SC 21--38.  K. Burrage M. Hegland S. Macnamara and R. Sidje. 2006. A Krylov-based finite state projection algorithm for solving the chemical master equation arising in the discrete modelling of biological systems. In Mam 2006: Markov Anniversary Meeting: An International Conference to Celebrate the 150th Anniversary of the birth of A.A. Markov A. N. Langville and W. J. Stewart Eds. Boston Books Charleston SC 21--38."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1093\/nar\/gkq086"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.2159468"},{"key":"e_1_2_1_11_1","first-page":"213","article-title":"Genetically modified organisms for the environment: Stories of success and failure and what we have learned from them","volume":"8","author":"Cases I.","year":"2005","unstructured":"I. Cases and V. de Lorenzo . 2005 . Genetically modified organisms for the environment: Stories of success and failure and what we have learned from them . Int. Microbiol. 8 , 213 -- 222 . I. Cases and V. de Lorenzo. 2005. Genetically modified organisms for the environment: Stories of success and failure and what we have learned from them. Int. Microbiol. 8, 213--222.","journal-title":"Int. Microbiol."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1186\/1754-1611-3-19"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.02.010"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"M. Elowitz and S. Leibler. 2000. A synthetic oscillatory network of transcriptional regulators. Nature 403 6767 335--338.  M. Elowitz and S. Leibler. 2000. A synthetic oscillatory network of transcriptional regulators. Nature 403 6767 335--338.","DOI":"10.1038\/35002125"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1038\/nature04342"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1038\/35002131"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1021\/jp993732q"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1021\/j100540a008"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.1613254"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.3116791"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1662583.1662590"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_27"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_29"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.03.007"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"H. Kuwahara C. Madsen I. Mura C. Myers A. Tejada and C. Winstead. 2010. Efficient stochastic simulation to analyze targeted properties of biological systems. In Stochastic Control C. Myers Ed. Sciyo 505--532.  H. Kuwahara C. Madsen I. Mura C. Myers A. Tejada and C. Winstead. 2010. Efficient stochastic simulation to analyze targeted properties of biological systems. In Stochastic Control C. Myers Ed. Sciyo 505--532.","DOI":"10.5772\/46977"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.2987701"},{"key":"e_1_2_1_28_1","first-page":"150","article-title":"Automated abstraction methodology for genetic regulatory networks","author":"Kuwahara H.","year":"2006","unstructured":"H. Kuwahara , C. Myers , N. Barker , M. Samoilov , and A. Arkin . 2006 . Automated abstraction methodology for genetic regulatory networks . Trans. Comp. Syst. Biol. VI , 150 -- 175 . H. Kuwahara, C. Myers, N. Barker, M. Samoilov, and A. Arkin. 2006. Automated abstraction methodology for genetic regulatory networks. Trans. Comp. Syst. Biol. VI, 150--175.","journal-title":"Trans. Comp. Syst. Biol."},{"volume-title":"Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07)","author":"Kwiatkowska M.","key":"e_1_2_1_29_1","unstructured":"M. Kwiatkowska , G. Norman , and D. Parker 2007. Stochastic model checking . In Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07) , M. Bernardo and J. Hillston, Eds., Lecture Notes in Computer Science (Tutorial Volume), vol. 4486 , Springer , 220--270. M. Kwiatkowska, G. Norman, and D. Parker 2007. Stochastic model checking. In Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07), M. Bernardo and J. Hillston, Eds., Lecture Notes in Computer Science (Tutorial Volume), vol. 4486, Springer, 220--270."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1093\/bioinformatics\/btn330"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1371\/journal.pcbi.1001083"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-9525(98)01659-X"},{"volume-title":"Proceedings of the International Symposium on the Theory of Switching","author":"Muller D. E.","key":"e_1_2_1_34_1","unstructured":"D. E. Muller and W. S. Bartky . 1959. A theory of asynchronous circuits . In Proceedings of the International Symposium on the Theory of Switching . Harvard University Press, Cambridge, MA, 204--243. D. E. Muller and W. S. Bartky. 1959. A theory of asynchronous circuits. In Proceedings of the International Symposium on the Theory of Switching. Harvard University Press, Cambridge, MA, 204--243."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.2145882"},{"volume-title":"Engineering Genetic Circuits","author":"Myers C. J.","key":"e_1_2_1_36_1","unstructured":"C. J. Myers . 2009. Engineering Genetic Circuits . Chapman and Hall\/CRC. C. J. Myers. 2009. Engineering Genetic Circuits. Chapman and Hall\/CRC."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1093\/bioinformatics\/btp457"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jtbi.2009.10.026"},{"key":"e_1_2_1_39_1","doi-asserted-by":"crossref","first-page":"S437","DOI":"10.1098\/rsif.2008.0516.focus","article-title":"Towards programming languages for genetic engineering of living cells","volume":"6","author":"Pedersen M.","year":"2009","unstructured":"M. Pedersen and A. Phillips . 2009 . Towards programming languages for genetic engineering of living cells . J. Roy. Soc. Interface 6, (Suppl. 4 ), S437 -- S450 . M. Pedersen and A. Phillips. 2009. Towards programming languages for genetic engineering of living cells. J. Roy. Soc. Interface 6, (Suppl. 4), S437--S450.","journal-title":"J. Roy. Soc. Interface"},{"key":"e_1_2_1_40_1","volume-title":"C: The Art of Scientific Computing","author":"Press W. H.","year":"1992","unstructured":"W. H. Press , B. P. Flannery , S. A. Teukolsky , and W. T. Vetterling . 1992 . Numerical Recipes in C: The Art of Scientific Computing , 2 nd ed. Cambridge University Press . W. H. Press, B. P. Flannery, S. A. Teukolsky, and W. T. Vetterling. 1992. Numerical Recipes in C: The Art of Scientific Computing, 2nd ed. Cambridge University Press.","edition":"2"},{"issue":"0","key":"e_1_2_1_41_1","first-page":"0","article-title":"Synthetic biology open language visual (SBOL Visual)","volume":"1","author":"Quinn J.","year":"2013","unstructured":"J. Quinn , J. Beal , S. Bhatia , P. Cai , J. Chen , K. Clancy , N. J. Hillson , M. Galdzicki , A. Maheshwari , P. Umesh , M. Pocock , C. Rodriguez , G.-B. Stan , and D. Endy . 2013 . Synthetic biology open language visual (SBOL Visual) , Version 1 . 0 . 0 . BBF RFC 93. J. Quinn, J. Beal, S. Bhatia, P. Cai, J. Chen, K. Clancy, N. J. Hillson, M. Galdzicki, A. Maheshwari, P. Umesh, M. Pocock, C. Rodriguez, G.-B. Stan, and D. Endy. 2013. Synthetic biology open language visual (SBOL Visual), Version 1.0.0. BBF RFC 93.","journal-title":"Version"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.1545446"},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"D.-K. Ro E. M. Paradise M. Ouellet K. J. Fisher K. L. Newman J. M. Ndungu K. A. Ho R. A. Eachus T. S. Ham J. Kirby M. C. Y. Chang S. T. Withers Y. Shiba R. Sarpong and J. D. Keasling. 2006. Production of the antimalarial drug percursor artemisinic acid in engineered yeast. Nature 440.  D.-K. Ro E. M. Paradise M. Ouellet K. J. Fisher K. L. Newman J. M. Ndungu K. A. Ho R. A. Eachus T. S. Ham J. Kirby M. C. Y. Chang S. T. Withers Y. Shiba R. Sarpong and J. D. Keasling. 2006. Production of the antimalarial drug percursor artemisinic acid in engineered yeast. Nature 440.","DOI":"10.1038\/nature04640"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.2919546"},{"volume-title":"Introduction to the Numerical Solution of Markov Chains","author":"Stewart W. J.","key":"e_1_2_1_45_1","unstructured":"W. J. Stewart . 1994. Introduction to the Numerical Solution of Markov Chains . Priceton University Press , Princeton, NJ . W. J. Stewart. 1994. Introduction to the Numerical Solution of Markov Chains. Priceton University Press, Princeton, NJ."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1038\/nature07389"},{"volume-title":"Biology, Chemistry and Engineering","author":"Strogatz S. H.","key":"e_1_2_1_47_1","unstructured":"S. H. Strogatz . 1994. Nonlinear Dynamics and Chaos: With Applications to Physics , Biology, Chemistry and Engineering . Westview Press . S. H. Strogatz. 1994. Nonlinear Dynamics and Chaos: With Applications to Physics, Biology, Chemistry and Engineering. Westview Press."},{"key":"e_1_2_1_48_1","first-page":"277","article-title":"Dynamical behaviour of biological networks: Immunity control in bacteriophage lamabda","volume":"57","author":"Thieffry D.","year":"1995","unstructured":"D. Thieffry and R. Thomas . 1995 . Dynamical behaviour of biological networks: Immunity control in bacteriophage lamabda . Bull. Math. Biol. 57 , 2, 277 -- 297 . D. Thieffry and R. Thomas. 1995. Dynamical behaviour of biological networks: Immunity control in bacteriophage lamabda. Bull. Math. Biol. 57, 2, 277--297.","journal-title":"Bull. Math. Biol."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-5193(05)80350-9"},{"key":"e_1_2_1_50_1","first-page":"1","article-title":"The dynamics of feedback control circuits in biochemical pathways","volume":"5","author":"Tyson J.","year":"1978","unstructured":"J. Tyson and H. Othmer . 1978 . The dynamics of feedback control circuits in biochemical pathways . Prog. Theoret. Biol. 5 , 1 -- 62 . J. Tyson and H. Othmer. 1978. The dynamics of feedback control circuits in biochemical pathways. Prog. Theoret. Biol. 5, 1--62.","journal-title":"Prog. Theoret. Biol."},{"key":"e_1_2_1_51_1","volume-title":"Forhandlinger: Videnskabs - Selskabet i Christinia 35.","author":"Waage P.","year":"1864","unstructured":"P. Waage and C. M. Guldberg . 1864 . Studies concerning affinity. Forhandlinger: Videnskabs - Selskabet i Christinia 35. P. Waage and C. M. Guldberg. 1864. Studies concerning affinity. Forhandlinger: Videnskabs - Selskabet i Christinia 35."},{"volume-title":"Proceedings of the International Symposium on Circuits and Systems (ISCAS). IEEE, 553--556","author":"Winstead C.","key":"e_1_2_1_52_1","unstructured":"C. Winstead , C. Madsen , and C. J. Myers . 2010. iSSA: An incremental stochastic simulation algorithm for genetic circuits . In Proceedings of the International Symposium on Circuits and Systems (ISCAS). IEEE, 553--556 . C. Winstead, C. Madsen, and C. J. Myers. 2010. iSSA: An incremental stochastic simulation algorithm for genetic circuits. In Proceedings of the International Symposium on Circuits and Systems (ISCAS). IEEE, 553--556."},{"volume-title":"Proceedings of the 49th IEEE Conference on Decision and Control (CDC). 5899--5904","author":"Yordanov B.","key":"e_1_2_1_53_1","unstructured":"B. Yordanov , J. Tumova , C. Belta , I. Cerna , and J. Barnat . 2010. Formal analysis of piecewise affine systems through formula-guided refinement . In Proceedings of the 49th IEEE Conference on Decision and Control (CDC). 5899--5904 . B. Yordanov, J. Tumova, C. Belta, I. Cerna, and J. Barnat. 2010. Formal analysis of piecewise affine systems through formula-guided refinement. In Proceedings of the 49th IEEE Conference on Decision and Control (CDC). 5899--5904."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-005-0187-8"}],"container-title":["ACM Journal on Emerging Technologies in Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2644817","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2644817","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:13:12Z","timestamp":1750227192000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2644817"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12,30]]},"references-count":52,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,12,30]]}},"alternative-id":["10.1145\/2644817"],"URL":"https:\/\/doi.org\/10.1145\/2644817","relation":{},"ISSN":["1550-4832","1550-4840"],"issn-type":[{"type":"print","value":"1550-4832"},{"type":"electronic","value":"1550-4840"}],"subject":[],"published":{"date-parts":[[2014,12,30]]},"assertion":[{"value":"2014-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-12-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}