{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,10]],"date-time":"2025-04-10T04:21:56Z","timestamp":1744258916617,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642336355"},{"type":"electronic","value":"9783642336362"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33636-2_4","type":"book-chapter","created":{"date-parts":[[2012,9,27]],"date-time":"2012-09-27T23:25:48Z","timestamp":1348788348000},"page":"29-48","source":"Crossref","is-referenced-by-count":3,"title":["Expressive Statistical Model Checking of Genetic Networks with Delayed Stochastic Dynamics"],"prefix":"10.1007","author":[{"given":"Paolo","family":"Ballarini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jarno","family":"M\u00e4kel\u00e4","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andre S.","family":"Ribeiro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"Cosmos home page, http:\/\/www.lsv.ens-cachan.fr\/software\/cosmos\/"},{"key":"4_CR2","unstructured":"Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. John Wiley & Sons (1995)"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems","author":"R. Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol.\u00a0736, pp. 209\u2013229. Springer, Heidelberg (1993)"},{"issue":"4","key":"4_CR4","doi-asserted-by":"crossref","first-page":"1633","DOI":"10.1093\/genetics\/149.4.1633","volume":"149","author":"A.P. Arkin","year":"1998","unstructured":"Arkin, A.P., Ross, J., McAdams, H.H.: Stochastic Kinetic Analysis of a Developmental Pathway Bifurcation in Phage-l Escherichia coli. Genetics\u00a0149(4), 1633\u20131648 (1998)","journal-title":"Genetics"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Baier, C., Cloth, L., Haverkort, B., Kuntz, M., Siegle, M.: Model checking action- and state-labelled Markov chains. IEEE Trans. on Software Eng.\u00a033(4) (2007)","DOI":"10.1109\/TSE.2007.36"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for CTMCs. IEEE Trans. on Software Eng.\u00a029(6) (2003)","DOI":"10.1109\/TSE.2003.1205180"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: COSMOS: a\u00a0statistical model checker for the hybrid automata stochastic logic. In: Proceedings of the 8th International Conference on Quantitative Evaluation of Systems (QEST 2011), pp. 143\u2013144. IEEE Computer Society Press (September 2011)","DOI":"10.1109\/QEST.2011.24"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: HASL: an expressive language for statistical verification of stochastic models. In: Proc. Valuetools (2011)","DOI":"10.4108\/icst.valuetools.2011.245710"},{"issue":"20","key":"4_CR9","doi-asserted-by":"publisher","first-page":"2019","DOI":"10.1016\/j.tcs.2010.02.010","volume":"411","author":"P. Ballarini","year":"2010","unstructured":"Ballarini, P., Guerriero, M.L.: Query-based verification of qualitative trends and oscillations in biochemical systems. Theoretical Computer Science\u00a0411(20), 2019\u20132036 (2010)","journal-title":"Theoretical Computer Science"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Cern\u00e1, I., Drazan, S., Fabrikov\u00e1, J., L\u00e1n\u00edk, J., Safr\u00e1nek, D., Ma, H.: Biodivine: A framework for parallel analysis of biological models. In: COMPMOD. EPTCS, vol.\u00a06, pp. 31\u201345 (2009)","DOI":"10.4204\/EPTCS.6.3"},{"issue":"9","key":"4_CR11","doi-asserted-by":"publisher","first-page":"1017","DOI":"10.1371\/journal.pcbi.0020117","volume":"2","author":"M. Barrio","year":"2006","unstructured":"Barrio, M., Burrage, K., Leier, A., Tian, T.: Oscillatory regulation of hes1: Discrete stochastic delay modelling and simulation. PLoS Computational Biology\u00a02(9), 1017\u20131030 (2006)","journal-title":"PLoS Computational Biology"},{"issue":"3","key":"4_CR12","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1016\/j.jtbi.2004.04.003","volume":"229","author":"G. Bernot","year":"2004","unstructured":"Bernot, G., Comet, J.-P., Richard, A., Guespin, J.: Application of formal methods to biological regulatory networks: extending Thomas\u2019 asynchronous logical approach with temporal logic. Journal of Theoretical Biology\u00a0229(3), 339\u2013347 (2004)","journal-title":"Journal of Theoretical Biology"},{"issue":"41","key":"4_CR13","doi-asserted-by":"publisher","first-page":"14593","DOI":"10.1073\/pnas.0503858102","volume":"102","author":"D. Bratsun","year":"2005","unstructured":"Bratsun, D., Volfson, D., Tsimring, L.S., Hasty, J.: Delay-induced stochastic oscillations in gene regulation. Proc. Natl. Acad. Sci. USA.\u00a0102(41), 14593\u201314598 (2005)","journal-title":"Proc. Natl. Acad. Sci. USA."},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Quantitative model checking of CTMC against timed automata specifications. In: Proc. LICS 2009 (2009)","DOI":"10.1109\/LICS.2009.21"},{"issue":"3","key":"4_CR15","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1093\/bioinformatics\/btf851","volume":"19","author":"H. Jong De","year":"2003","unstructured":"De Jong, H., Geiselmann, J., Hernandez, C., Page, M.: Genetic network analyzer: qualitative simulation of genetic regulatory networks. Bioinformatics\u00a019(3), 244\u2013336 (2003)","journal-title":"Bioinformatics"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with CSL TA . IEEE Trans. on Software Eng.\u00a035 (2009)","DOI":"10.1109\/TSE.2008.108"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-10003-2_69","volume-title":"Automata, Languages and Programming","author":"E.A. Emerson","year":"1980","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing Correctness Properties of Parallel Programs Using Fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol.\u00a085, pp. 169\u2013181. Springer, Heidelberg (1980)"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-540-68894-5_3","volume-title":"Formal Methods for Computational Systems Biology","author":"F. Fages","year":"2008","unstructured":"Fages, F., Soliman, S.: Formal Cell Biology in Biocham. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol.\u00a05016, pp. 54\u201380. Springer, Heidelberg (2008)"},{"issue":"2","key":"4_CR19","doi-asserted-by":"publisher","first-page":"64","DOI":"10.4024\/2040402.jbpc.04.02","volume":"4","author":"F. Fages","year":"2004","unstructured":"Fages, F., Soliman, S., Rivier, C.N.: Modelling and querying interaction networks in the biochemical abstract machine BIOCHAM. Journal of Biological Physics and Chemistry\u00a04(2), 64\u201373 (2004)","journal-title":"Journal of Biological Physics and Chemistry"},{"issue":"25","key":"4_CR20","doi-asserted-by":"publisher","first-page":"2340","DOI":"10.1021\/j100540a008","volume":"81","author":"D.T. Gillespie","year":"1977","unstructured":"Gillespie, D.T.: Exact stochastic simulation of coupled chemical reactions. Journal of Physical Chemistry\u00a081(25), 2340\u20132361 (1977)","journal-title":"Journal of Physical Chemistry"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Hansson, H.A., Jonsson, B.: A framework for reasoning about time and reliability. In: Proc. 10th IEEE Real -Time Systems Symposium, Santa Monica, Ca, pp. 102\u2013111. IEEE Computer Society Press (1989)","DOI":"10.1109\/REAL.1989.63561"},{"key":"4_CR22","unstructured":"Haverkort, B.R., Cloth, L., Hermanns, H., Katoen, J.-P., Baier, C.: Model checking performability properties. In: Proc. DSN 2002 (2002)"},{"issue":"3","key":"4_CR23","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/j.tcs.2007.11.013","volume":"319","author":"J. Heath","year":"2008","unstructured":"Heath, J., Kwiatkowska, M., Norman, G., Parker, D., Tymchyshyn, O.: Probabilistic model checking of complex biological pathways. Theoretical Computer Science\u00a0319(3), 239\u2013257 (2008)","journal-title":"Theoretical Computer Science"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-642-03845-7_15","volume-title":"Computational Methods in Systems Biology","author":"S.K. Jha","year":"2009","unstructured":"Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A Bayesian Approach to Model Checking Biological Systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol.\u00a05688, pp. 218\u2013234. Springer, Heidelberg (2009)"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Kandhavelu, M., Hakkinen, A., Yli-Harja, O., Ribeiro, A.S.: Single-molecule dynamics of transcription of the lar promoter. Phys. Biol.\u00a09(2) (2012)","DOI":"10.1088\/1478-3975\/9\/2\/026004"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Kitano, H.: Foundations of Systems Biology. MIT Press (2002)","DOI":"10.7551\/mitpress\/3087.001.0001"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-72522-0_6","volume-title":"Formal Methods for Performance Evaluation","author":"M. Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic Model Checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol.\u00a04486, pp. 220\u2013270. Springer, Heidelberg (2007)"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Lakin, M., Parker, D., Cardelli, L., Kwiatkowska, M., Phillips, A.: Design and analysis of DNA strand displacement devices using probabilistic model checking. Journal of the Royal Society Interface (to appear, 2011)","DOI":"10.1098\/rsif.2011.0800"},{"issue":"1","key":"4_CR29","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1186\/1471-2105-12-121","volume":"12","author":"J. Makela","year":"2011","unstructured":"Makela, J., Lloyd-Price, J., Yli-Harja, O., Ribeiro, A.S.: Stochastic sequence-level model of coupled transcription and translation in prokaryotes. BMC Bioinformatics\u00a012(1), 121 (2011)","journal-title":"BMC Bioinformatics"},{"key":"4_CR30","doi-asserted-by":"publisher","first-page":"2103","DOI":"10.1529\/biophysj.107.127191","volume":"95","author":"J.A. Megerle","year":"2008","unstructured":"Megerle, J.A., Fritz, G., Gerland, U., Jung, K., R\u00e4dler, J.O.: Timing and Dynamics of Single Cell Gene Expression in the Arabinose Utilization System. Biophysical Journal\u00a095, 2103\u20132115 (2008)","journal-title":"Biophysical Journal"},{"key":"4_CR31","unstructured":"Prism home page, http:\/\/www.prismmodelchecker.org"},{"issue":"9","key":"4_CR32","doi-asserted-by":"publisher","first-page":"1630","DOI":"10.1089\/cmb.2006.13.1630","volume":"13","author":"A. Ribeiro","year":"2006","unstructured":"Ribeiro, A., Zhu, R., Kauffman, S.A.: A general modeling strategy for gene regulatory networks with stochastic dynamics. Journal of Computational Biology: a Journal of Computational Molecular Cell Biology\u00a013(9), 1630\u20131639 (2006)","journal-title":"Journal of Computational Biology: a Journal of Computational Molecular Cell Biology"},{"issue":"6","key":"4_CR33","doi-asserted-by":"publisher","first-page":"777","DOI":"10.1093\/bioinformatics\/btm004","volume":"23","author":"A.S. Ribeiro","year":"2007","unstructured":"Ribeiro, A.S., Lloyd-Price, J.: SGN Sim, a stochastic genetic networks simulator. Bioinformatics\u00a023(6), 777\u2013779 (2007)","journal-title":"Bioinformatics"},{"issue":"4","key":"4_CR34","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1088\/1478-3975\/3\/4\/005","volume":"3","author":"M.R. Roussel","year":"2006","unstructured":"Roussel, M.R., Zhu, R.: Validation of an algorithm for delay stochastic simulation of transcription and translation in prokaryotic gene expression. Physical Biology\u00a03(4), 274\u2013284 (2006)","journal-title":"Physical Biology"},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"Schwarick, M., Rohr, C., Heiner, M.: Marcie - model checking and reachability analysis done efficiently. In: Proc. 8th International Conference on Quantitative Evaluation of SysTems (QEST 2011), pp. 91\u2013100. IEEE CS Press (2011)","DOI":"10.1109\/QEST.2011.19"},{"key":"4_CR36","unstructured":"Spieler, D.: Model checking of oscillatory and noisy periodic behavior in markovian population models. Master\u2019s thesis, Saarland University (2009)"},{"issue":"5991","key":"4_CR37","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1126\/science.1188308","volume":"329","author":"Y. Taniguchi","year":"2010","unstructured":"Taniguchi, Y., Choi, P.J., Li, G.-W., Chen, H., Babu, M., Hearn, J., Emili, A., Xie, X.S.: Quantifying E. coli Proteome and Transcriptome with Single-Molecule Sensitivity in Single Cells. Science\u00a0329(5991), 533\u2013538 (2010)","journal-title":"Science"},{"issue":"4","key":"4_CR38","doi-asserted-by":"publisher","first-page":"725","DOI":"10.1016\/j.jtbi.2007.01.021","volume":"246","author":"R. Zhu","year":"2007","unstructured":"Zhu, R., Ribeiro, A.S., Salahub, D., Kauffman, S.A.: Studying genetic regulatory networks at the molecular level: Delayed reaction stochastic models. Journal of Theoretical Biology\u00a0246(4), 725\u2013745 (2007)","journal-title":"Journal of Theoretical Biology"}],"container-title":["Lecture Notes in Computer Science","Computational Methods in Systems Biology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33636-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T17:20:42Z","timestamp":1744219242000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33636-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642336355","9783642336362"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33636-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}