{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T18:39:57Z","timestamp":1773945597460,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":47,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642038440","type":"print"},{"value":"9783642038457","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03845-7_15","type":"book-chapter","created":{"date-parts":[[2009,8,26]],"date-time":"2009-08-26T02:41:17Z","timestamp":1251254477000},"page":"218-234","source":"Crossref","is-referenced-by-count":137,"title":["A Bayesian Approach to Model Checking Biological Systems"],"prefix":"10.1007","author":[{"given":"Sumit K.","family":"Jha","sequence":"first","affiliation":[]},{"given":"Edmund M.","family":"Clarke","sequence":"additional","affiliation":[]},{"given":"Christopher J.","family":"Langmead","sequence":"additional","affiliation":[]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[]},{"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[]},{"given":"Paolo","family":"Zuliani","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"15_CR1","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1385\/CBB:38:3:271","volume":"38","author":"M. Antoniotti","year":"2003","unstructured":"Antoniotti, M., Policriti, A., Ugel, N., Mishra, B.: Model building and model checking for biochemical processes. Cell Biochem. Biophys.\u00a038(3), 271\u2013286 (2003)","journal-title":"Cell Biochem. Biophys."},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/3-540-63165-8_199","volume-title":"Automata, Languages and Programming","author":"C. Baier","year":"1997","unstructured":"Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M.Z., Ryan, M.: Symbolic model checking for probabilistic processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol.\u00a01256, pp. 430\u2013440. Springer, Heidelberg (1997)"},{"issue":"6","key":"15_CR3","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time markov chains. IEEE Trans. Software Eng.\u00a029(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Software Eng."},{"key":"15_CR4","unstructured":"Bailey, N.: The Elements of Stochastic Processes with Applications to the Natural Sciences. Wiley-IEEE (1990)"},{"key":"15_CR5","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1038\/35002258","volume":"403","author":"N. Barkai","year":"2000","unstructured":"Barkai, N., Leibler, S.: Biological rhythms: Circadian clocks limited by noise. Nature\u00a0403, 267\u2013268 (2000)","journal-title":"Nature"},{"issue":"1","key":"15_CR6","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1093\/bioinformatics\/bti1048","volume":"25","author":"G. Batt","year":"2005","unstructured":"Batt, G., Ropers, D., de Jong, H., Geiselmann, J., Mateescu, R., Page, M., Schneider, D.: Validation of qualitative models of genetic regulatory networks by model checking: analysis of the nutritional stress response in Escherichia coli. Bioinformatics\u00a025(1), i19\u2013i28 (2005)","journal-title":"Bioinformatics"},{"key":"15_CR7","doi-asserted-by":"publisher","first-page":"660","DOI":"10.1080\/01621459.1960.10483366","volume":"55","author":"R. Bechhofer","year":"1960","unstructured":"Bechhofer, R.: A note on the limiting relative efficiency of the Wald sequential probability ratio test. J. Amer. Statist. Assoc.\u00a055, 660\u2013663 (1960)","journal-title":"J. Amer. Statist. Assoc."},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Calder, M., Gilmore, S., Hillston, J.: Modelling the influence of RKIP on the ERK signalling pathway using the stochastic process algebra PEPA. Transactions on Computational Systems Biology (2006) (in press)","DOI":"10.1007\/11905455_1"},{"key":"15_CR9","unstructured":"Calder, M., Vyshemirsky, V., Gilbert, D., Orton, R.: Analysis of signalling pathways using the PRISM model checker. In: Proc. Computational Methods in Systems Biology (CMSB 2005), pp. 179\u2013190 (2005)"},{"key":"15_CR10","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/11599128_10","volume-title":"Transactions on Computational Systems Biology III","author":"L. Cardelli","year":"2005","unstructured":"Cardelli, L.: Abstract machines of systems biology. In: Priami, C., Merelli, E., Gonzalez, P., Omicini, A. (eds.) Transactions on Computational Systems Biology III. LNCS (LNBI), vol.\u00a03737, pp. 145\u2013168. Springer, Heidelberg (2005)"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-36481-1_13","volume-title":"Computational Methods in Systems Biology","author":"N. Chabrier","year":"2003","unstructured":"Chabrier, N., Fages, F.: Symbolic Model Checking of Biochemical Networks. In: Priami, C. (ed.) CMSB 2003. LNCS, vol.\u00a02602, pp. 149\u2013162. Springer, Heidelberg (2003)"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-540-24611-4_5","volume-title":"Validation of Stochastic Systems","author":"F. Ciesinski","year":"2004","unstructured":"Ciesinski, F., Gr\u00f6\u00dfer, M.: On probabilistic computation tree logic. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol.\u00a02925, pp. 147\u2013188. Springer, Heidelberg (2004)"},{"key":"15_CR13","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logic of Programs, Workshop","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, Workshop, London, UK, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"15_CR14","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-540-88562-7_18","volume-title":"Computational Methods in Systems Biology","author":"E.M. Clarke","year":"2008","unstructured":"Clarke, E.M., Faeder, J.R., Langmead, C.J., Harris, L.A., Jha, S.K., Legay, A.: Statistical model checking in biolab: Applications to the automated analysis of t-cell receptor signaling pathway. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol.\u00a05307, pp. 231\u2013250. Springer, Heidelberg (2008)"},{"key":"15_CR15","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"4","key":"15_CR16","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM\u00a042(4), 857\u2013907 (1995)","journal-title":"Journal of the ACM"},{"key":"15_CR17","volume-title":"Bayesian Statistics 2: Proceedings of the 2nd Valencia International Meeting","author":"P. Diaconis","year":"1985","unstructured":"Diaconis, P., Ylvisaker, D.: Quantifying prior opinion. In: Bernardo, J.M., De Groot, M.H., Lindley, D.B., Smith, A.F.M. (eds.) Bayesian Statistics 2: Proceedings of the 2nd Valencia International Meeting. Elsevier Science Publisher, Amsterdam (1985)"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11680093_1","volume-title":"Logic Based Program Synthesis and Transformation","author":"F. Fages","year":"2006","unstructured":"Fages, F.: Temporal logic constraints in the biochemical abstract machine biocham. In: Hill, P.M. (ed.) LOPSTR 2005. LNCS, vol.\u00a03901, pp. 1\u20135. Springer, Heidelberg (2006)"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Sipma, H.: Checking finite traces using alternating automata. In: Proceedings of Runtime Verification (RV 2001), pp. 44\u201360 (2001)","DOI":"10.1016\/S1571-0661(04)00250-6"},{"issue":"6","key":"15_CR20","doi-asserted-by":"publisher","first-page":"1951","DOI":"10.1073\/pnas.0409433102","volume":"102","author":"J. Fisher","year":"2005","unstructured":"Fisher, J., Piterman, N., Hubbard, E.J., Stern, M.J., Harel, D.: Computational insights into caenorhabditis elegans vulval development. Proc. Natl. Acad. Sci. U S A\u00a0102(6), 1951\u20131956 (2005)","journal-title":"Proc. Natl. Acad. Sci. U S A"},{"key":"15_CR21","volume-title":"Handbook of sequential analysis","year":"1991","unstructured":"Ghosh, B., Sen, P. (eds.): Handbook of sequential analysis. Dekker, New York (1991)"},{"issue":"25","key":"15_CR22","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. The Journal of Physical Chemistry\u00a081(25), 2340\u20132361 (1977)","journal-title":"The Journal of Physical Chemistry"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Grosu, R., Smolka, S.: Monte Carlo Model Checking. In: CAV, pp. 271\u2013286 (2005)","DOI":"10.1007\/978-3-540-31980-1_18"},{"key":"15_CR24","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/11885191_3","volume-title":"Computational Methods in Systems Biology","author":"J. Heath","year":"2006","unstructured":"Heath, J., Kwiatkowska, M., Norman, G., Parker, D., Tymchyshyn, O.: Probabilistic model checking of complex biological pathways. In: Priami, C. (ed.) CMSB 2006. LNCS (LNBI), vol.\u00a04210, pp. 32\u201347. Springer, Heidelberg (2006)"},{"issue":"3","key":"15_CR25","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":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-540-24622-0_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. H\u00e9rault","year":"2004","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 73\u201384. Springer, Heidelberg (2004)"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"15_CR28","volume-title":"Theory of Probability","author":"H. Jeffreys","year":"1961","unstructured":"Jeffreys, H.: Theory of Probability. Clarendon Press, Oxford (1961)"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A bayesian approach to model checking biological systems. Technical Report CMU-CS-09-110, Computer Science Department, Carnegie Mellon University (2009)","DOI":"10.1007\/978-3-642-03845-7_15"},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"Kam, N., Harel, D., Cohen, I.R.: Modeling biological reactivity: Statecharts vs. boolean logic. In: Proceedings of the Second International Conference on Systems Biology (2001)","DOI":"10.1145\/1556262.1556318"},{"key":"15_CR31","first-page":"322","volume-title":"QEST","author":"M.Z. Kwiatkowska","year":"2004","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Prism 2.0: A tool for probabilistic model checking. In: QEST, pp. 322\u2013323. IEEE, Los Alamitos (2004)"},{"key":"15_CR32","unstructured":"Langmead, C.J.: Generalized Queries and Bayesian Statistical Model Checking in Dynamic Bayesian Networks: Application to Personalized Medicine. In: Proc. 8th Ann. Intnl Conf. on Comput. Sys. Bioinf. (CSB), pp. 201\u2013212 (2009)"},{"key":"15_CR33","unstructured":"Lecca, P., Priami, C.: Cell cycle control in eukaryotes: A BioSpi model. In: Proc. Workshop on Concurrent Models in Molecular Biology (BioConcur 2003). ENTCS (2003)"},{"key":"15_CR34","doi-asserted-by":"publisher","first-page":"650","DOI":"10.1126\/science.7624793","volume":"269","author":"H. McAdams","year":"1995","unstructured":"McAdams, H., Shapiro, L.: Circuit simulation of genetic networks. Science\u00a0269, 650\u2013656 (1995)","journal-title":"Science"},{"issue":"3","key":"15_CR35","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S.S. Owicki","year":"1982","unstructured":"Owicki, S.S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst.\u00a04(3), 455\u2013495 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"15_CR36","first-page":"46","volume-title":"FOCS","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE, Los Alamitos (1977)"},{"issue":"1","key":"15_CR37","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/S0020-0190(01)00214-9","volume":"80","author":"C. Priami","year":"2001","unstructured":"Priami, C., Regev, A., Shapiro, E., Silverman, W.: Application of a stochastic name-passing calculus to representation and simulation of molecular processes. Inf. Process. Lett.\u00a080(1), 25\u201331 (2001)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"15_CR38","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1109\/TCBB.2007.1076","volume":"5","author":"A. Sadot","year":"2008","unstructured":"Sadot, A., Fisher, J., Barak, D., Admanit, Y., Stern, M.J., Hubbard, E.J.A., Harel, D.: Toward verified biological models. IEEE\/ACM Transactions on Computational Biology and Bioinformatics\u00a05(2), 223\u2013234 (2008)","journal-title":"IEEE\/ACM Transactions on Computational Biology and Bioinformatics"},{"key":"15_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-27813-9_16","volume-title":"Computer Aided Verification","author":"K. Sen","year":"2004","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 202\u2013215. Springer, Heidelberg (2004)"},{"key":"15_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/11513988_26","volume-title":"Computer Aided Verification","author":"K. Sen","year":"2005","unstructured":"Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 266\u2013280. Springer, Heidelberg (2005)"},{"issue":"9","key":"15_CR41","doi-asserted-by":"publisher","first-page":"5988","DOI":"10.1073\/pnas.092133899","volume":"99","author":"J. Vilar","year":"2002","unstructured":"Vilar, J., Kueh, H.-Y., Barkai, N., Leibler, S.: Mechanisms of noise-resistance in genetic oscillators. Proc. Nat. Acad. Sci. USA\u00a099(9), 5988\u20135992 (2002)","journal-title":"Proc. Nat. Acad. Sci. USA"},{"issue":"2","key":"15_CR42","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1214\/aoms\/1177731118","volume":"16","author":"A. Wald","year":"1945","unstructured":"Wald, A.: Sequential tests of statistical hypotheses. Annals of Mathematical Statistics\u00a016(2), 117\u2013186 (1945)","journal-title":"Annals of Mathematical Statistics"},{"key":"15_CR43","unstructured":"Wald, A.: Sequential Analysis. Dover Publications (June 2004)"},{"issue":"19","key":"15_CR44","doi-asserted-by":"publisher","first-page":"10764","DOI":"10.1073\/pnas.1834247100","volume":"100","author":"T.M. Yi","year":"2003","unstructured":"Yi, T.M., Kitano, H., Simon, M.I.: A quantitative characterization of the yeast heterotrimeric g protein cycle. Proc. Natl. Acad. Sci. USA\u00a0100(19), 10764\u201310769 (2003)","journal-title":"Proc. Natl. Acad. Sci. USA"},{"issue":"3","key":"15_CR45","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/s10009-005-0187-8","volume":"8","author":"H.L.S. Younes","year":"2006","unstructured":"Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. STTT\u00a08(3), 216\u2013228 (2006)","journal-title":"STTT"},{"key":"15_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer Aided Verification","author":"H.L.S. Younes","year":"2002","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 223\u2013235. Springer, Heidelberg (2002)"},{"issue":"9","key":"15_CR47","doi-asserted-by":"publisher","first-page":"1368","DOI":"10.1016\/j.ic.2006.05.002","volume":"204","author":"H.L.S. Younes","year":"2006","unstructured":"Younes, H.L.S., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Information and Computation\u00a0204(9), 1368\u20131409 (2006)","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Computational Methods in Systems Biology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03845-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T01:11:59Z","timestamp":1558487519000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03845-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642038440","9783642038457"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03845-7_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}