{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:36:03Z","timestamp":1725536163767},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540888680"},{"type":"electronic","value":"9783540888697"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-540-88869-7_20","type":"book-chapter","created":{"date-parts":[[2009,8,12]],"date-time":"2009-08-12T21:41:55Z","timestamp":1250113315000},"page":"391-409","source":"Crossref","is-referenced-by-count":8,"title":["Quantitative Verification Techniques for\u00a0Biological Processes"],"prefix":"10.1007","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,8,13]]},"reference":[{"issue":"1","key":"20_CR1","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A Aziz","year":"2000","unstructured":"Aziz A, Sanwal K, Singhal V, Brayton R (2000) Model checking continuous time Markov chains. ACM Trans Comput Log 1(1):162\u2013170","journal-title":"ACM Trans Comput Log"},{"issue":"6","key":"20_CR2","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, Hermanns H, Katoen J-P (2003) Model-checking algorithms for continuous-time Markov chains. IEEE Trans Softw Eng 29(6):524\u2013541","journal-title":"IEEE Trans Softw Eng"},{"key":"20_CR3","first-page":"1","volume":"7","author":"M Calder","year":"2006","unstructured":"Calder M, Gilmore S, Hillston J (2006) Modelling the influence of RKIP on the ERK signaling pathway using the stochastic process algebra PEPA. Trans Comput Syst Biol 7:1\u201323","journal-title":"Trans Comput Syst Biol"},{"key":"20_CR4","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/11880646_3","volume":"4","author":"M Calder","year":"2006","unstructured":"Calder M, Vyshemirsky V, Gilbert D, Orton R (2006) Analysis of signaling pathways using continuous time Markov chains. Trans Comput Syst Biol 4:44\u201367","journal-title":"Trans Comput Syst Biol"},{"issue":"2","key":"20_CR5","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E Clarke","year":"1986","unstructured":"Clarke E, Emerson E, Sistla A (1986) Automatic verification of finite-state concurrent systems using temporal logics. ACM Trans Program Lang Syst 8(2):244\u2013263","journal-title":"ACM Trans Program Lang Syst"},{"key":"20_CR6","first-page":"722","volume-title":"Proceedings of the international conference on dependable systems and networks (DSN\u201905)","author":"L Cloth","year":"2005","unstructured":"Cloth L, Katoen J-P, Khattri M, Pulungan R (2005) Model checking Markov reward models with impulse rewards. In: Proceedings of the international conference on dependable systems and networks (DSN\u201905). IEEE Computer Society, Los Alamitos, pp 722\u2013731"},{"key":"20_CR7","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1109\/QEST.2007.30","volume-title":"Proceedings of the 4th international conference on quantitative evaluation of systems (QEST\u201907)","author":"A Donaldson","year":"2007","unstructured":"Donaldson A, Miller A, Parker D (2007) GRIP: Generic representatives in PRISM. In: Proceedings of the 4th international conference on quantitative evaluation of systems (QEST\u201907). IEEE Computer Society, Los Alamitos, pp 115\u2013116"},{"key":"20_CR8","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/978-3-540-39724-3_20","volume-title":"Proceedings of the 12th conference on correct hardware design and verification methods (CHARME 2003)","author":"E Emerson","year":"2003","unstructured":"Emerson E, Wahl T (2003) On combining symmetry reduction and symbolic representation for efficient model checking. In: Geist D, Tronci E (eds) Proceedings of the 12th conference on correct hardware design and verification methods (CHARME 2003). Lecture notes in computer science, vol 2860. Springer, Berlin, pp 216\u2013230"},{"issue":"25","key":"20_CR9","doi-asserted-by":"publisher","first-page":"2340","DOI":"10.1021\/j100540a008","volume":"81","author":"D Gillespie","year":"1977","unstructured":"Gillespie D (1977) Exact stochastic simulation of coupled chemical reactions. J Phys Chem 81(25):2340\u20132361","journal-title":"J Phys Chem"},{"issue":"5","key":"20_CR10","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson H, Jonsson B (1994) A logic for reasoning about time and reliability. Form Asp Comput 6(5):512\u2013535","journal-title":"Form Asp Comput"},{"key":"20_CR11","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 (2008) Probabilistic model checking of complex biological pathways. Theor Comput Sci 319:239\u2013257","journal-title":"Theor Comput Sci"},{"issue":"2","key":"20_CR12","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/s100090100072","volume":"4","author":"H Hermanns","year":"2003","unstructured":"Hermanns H, Katoen J-P, Meyer-Kayser J, Siegle M (2003) A tool for model checking Markov chains. Softw Tools Technol Transf 4(2):153\u2013172","journal-title":"Softw Tools Technol Transf"},{"key":"20_CR13","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511569951","volume-title":"A compositional approach to performance modeling","author":"J Hillston","year":"1996","unstructured":"Hillston J (1996) A compositional approach to performance modeling. Cambridge University Press, Cambridge"},{"key":"20_CR14","series-title":"Lecture notes in computer science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Proceedings of the 12th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201906)","author":"A Hinton","year":"2006","unstructured":"Hinton A, Kwiatkowska M, Norman G, Parker D (2006) PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns H, Palsberg J (eds) Proceedings of the 12th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201906). Lecture notes in computer science, vol 3920. Springer, Berlin, pp 441\u2013444"},{"key":"20_CR15","doi-asserted-by":"publisher","first-page":"10078","DOI":"10.1073\/pnas.93.19.10078","volume":"93","author":"C Huang","year":"1996","unstructured":"Huang C, Ferrell J (1996) Ultrasensitivity in the mitogen-activated protein kinase cascade. Proc Natl Acad Sci 93:10078\u201310083","journal-title":"Proc Natl Acad Sci"},{"key":"20_CR16","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1109\/QEST.2005.2","volume-title":"Proceedings of the 2nd international conference on quantitative evaluation of systems (QEST\u201905)","author":"J-P Katoen","year":"2005","unstructured":"Katoen J-P, Khattri M, Zapreev I (2005) A Markov reward model checker. In: Proceedings of the 2nd international conference on quantitative evaluation of systems (QEST\u201905). IEEE Computer Society, Los Alamitos, pp 243\u2013244"},{"issue":"2","key":"20_CR17","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/s10009-004-0140-2","volume":"6","author":"M Kwiatkowska","year":"2004","unstructured":"Kwiatkowska M, Norman G, Parker D (2004) Probabilistic symbolic model checking with PRISM: a hybrid approach. Softw Tools Technol Transf 6(2):128\u2013142","journal-title":"Softw Tools Technol Transf"},{"issue":"4","key":"20_CR18","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1145\/1059816.1059820","volume":"32","author":"M Kwiatkowska","year":"2005","unstructured":"Kwiatkowska M, Norman G, Parker D (2005) Probabilistic model checking in practice: case studies with PRISM. ACM SIGMETRICS Perform Eval Rev 32(4):16\u201321","journal-title":"ACM SIGMETRICS Perform Eval Rev"},{"key":"20_CR19","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1007\/11817963_23","volume-title":"Proceedings of the 18th international conference on computer aided verification (CAV\u201906)","author":"M Kwiatkowska","year":"2006","unstructured":"Kwiatkowska M, Norman G, Parker D (2006) Symmetry reduction for probabilistic model checking. In: Ball T, Jones R (eds) Proceedings of the 18th international conference on computer aided verification (CAV\u201906). Lecture notes in computer science, vol 4114. Springer, Berlin, pp 234\u2013248"},{"key":"20_CR20","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 the design of computer, communication and software systems: performance evaluation (SFM\u201907)","author":"M Kwiatkowska","year":"2007","unstructured":"Kwiatkowska M, Norman G, Parker D (2007) Stochastic model checking. In: Bernardo M, Hillston J (eds) Formal methods for the design of computer, communication and software systems: performance evaluation (SFM\u201907). Lecture notes in computer science, vol 4486. Springer, Berlin, pp 220\u2013270"},{"key":"20_CR21","unstructured":"Lecca P, Priami C (2003) Cell cycle control in eukaryotes: a BioSpi model. In: Proceedings of the workshop concurrent models in molecular biology (BioConcur\u201903). Electronic notes in theoretical computer science"},{"key":"20_CR22","unstructured":"MAPLE. \n                    www.maplesoft.com\/products\/maple\/"},{"key":"20_CR23","unstructured":"MATLAB. \n                    http:\/\/www.mathworks.com\/products\/matlab\/"},{"key":"20_CR24","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1109\/QEST.2007.31","volume-title":"Proceedings of the 4th international conference on quantitative evaluation of systems (QEST\u201907)","author":"G Norman","year":"2007","unstructured":"Norman G, Palamidessi C, Parker D, Wu P (2007) Model checking the probabilistic \u03c0-calculus. In: Proceedings of the 4th international conference on quantitative evaluation of systems (QEST\u201907). IEEE Computer Society, Los Alamitos, pp 169\u2013178"},{"key":"20_CR25","unstructured":"Parker D (2002) Implementation of symbolic model checking for probabilistic systems. PhD thesis, University of Birmingham"},{"key":"20_CR26","series-title":"Lecture notes in bioinformatics","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/978-3-540-75140-3_13","volume-title":"Proceedings of the 5th international conference on computational methods in systems biology (CMSB\u201907)","author":"A Phillips","year":"2007","unstructured":"Phillips A, Cardelli L (2007) Efficient, correct simulation of biological processes in the stochastic \u03c0-calculus. In: Calder M, Gilmore S (eds) Proceedings of the 5th international conference on computational methods in systems biology (CMSB\u201907). Lecture notes in bioinformatics, vol 4695. Springer, Berlin, pp 184\u2013199"},{"key":"20_CR27","unstructured":"PRISM web site. \n                    http:\/\/www.prismmodelchecker.org\/"},{"issue":"7","key":"20_CR28","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1093\/comjnl\/38.7.578","volume":"38","author":"C Priami","year":"1995","unstructured":"Priami C (1995) Stochastic \u03c0-calculus. Comput J 38(7):578\u2013589","journal-title":"Comput J"},{"key":"20_CR29","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, Silverman W, Shapiro E (2001) Application of a stochastic name passing calculus to representation and simulation of molecular processes. Inf Process Lett 80:25\u201331","journal-title":"Inf Process Lett"},{"key":"20_CR30","volume-title":"Proceedings of the 3rd international workshop on methods and tools for coordinating concurrent, distributed and mobile systems (MTCoord 2007)","author":"T Pronk","year":"2007","unstructured":"Pronk T, de Vink E, Bosnacki D, Breit T (2007) Stochastic modeling of codon bias with PRISM. In: Linden I, Talcott C (eds) Proceedings of the 3rd international workshop on methods and tools for coordinating concurrent, distributed and mobile systems (MTCoord 2007). Computer Science Department, University of Cyprus, Nicosia"},{"key":"20_CR31","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1007\/11963516_30","volume-title":"Proceedings of the 7th international workshop on membrane computing (WMC06)","author":"F Romero-Campero","year":"2006","unstructured":"Romero-Campero F, Gheorghe M, Bianco L, Pescini D, P\u00e9rez-Jim\u00e9nez M, Ceterchi R (2006) Towards probabilistic model checking on P systems using PRISM. In: Hoogeboom H, P\u0103un G, Rozenberg G, Salomaa A (eds) Proceedings of the 7th international workshop on membrane computing (WMC06). Lecture notes in computer science, vol 4361. Springer, Berlin, pp 477\u2013495"},{"key":"20_CR32","series-title":"CRM monograph series","doi-asserted-by":"crossref","DOI":"10.1090\/crmm\/023","volume-title":"Mathematical techniques for analyzing concurrent and probabilistic systems","author":"J Rutten","year":"2004","unstructured":"Rutten J, Kwiatkowska M, Norman G, Parker D (2004) Mathematical techniques for analyzing concurrent and probabilistic systems. CRM monograph series, vol 23. AMS, Providence"},{"key":"20_CR33","unstructured":"SBML-to-PRISM translator. \n                    http:\/\/www.prismmodelchecker.org\/sbml\/"},{"key":"20_CR34","unstructured":"SBML web site. \n                    http:\/\/sbml.org\/"},{"key":"20_CR35","unstructured":"SBML-shorthand. \n                    http:\/\/www.staff.ncl.ac.uk\/d.j.wilkinson\/software\/sbml-sh\/"},{"key":"20_CR36","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1109\/TNB.2004.833694","volume":"3","author":"O Wolkenhauer","year":"2004","unstructured":"Wolkenhauer O, Ullah M, Kolch W, Cho K-H (2004) Modeling and simulation of intracellular dynamics: choosing an appropriate framework. IEEE Trans Nanobiosci 3:200\u2013207","journal-title":"IEEE Trans Nanobiosci"},{"key":"20_CR37","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1007\/11513988_43","volume-title":"Proceedings of the 17th international conference on computer aided verification (CAV\u201905)","author":"H Younes","year":"2005","unstructured":"Younes H (2005) Ymer: A statistical model checker. In: Etessami K, Rajamani S (eds) Proceedings of the 17th international conference on computer aided verification (CAV\u201905). Lecture notes in computer science, vol 3576. Springer, Berlin, pp 429\u2013433"},{"issue":"3","key":"20_CR38","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/s10009-005-0187-8","volume":"8","author":"H Younes","year":"2006","unstructured":"Younes H, Kwiatkowska M, Norman G, Parker D (2006) Numerical vs. statistical probabilistic model checking. Softw Tools Technol Transf 8(3):216\u2013228","journal-title":"Softw Tools Technol Transf"}],"container-title":["Natural Computing Series","Algorithmic Bioprocesses"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88869-7_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T12:11:56Z","timestamp":1619525516000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88869-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783540888680","9783540888697"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88869-7_20","relation":{},"ISSN":["1619-7127"],"issn-type":[{"type":"print","value":"1619-7127"}],"subject":[],"published":{"date-parts":[[2009]]}}}