{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T01:47:38Z","timestamp":1768096058379,"version":"3.49.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2008,3,1]],"date-time":"2008-03-01T00:00:00Z","timestamp":1204329600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/D07956XEP\/D076625"],"award-info":[{"award-number":["EP\/D07956XEP\/D076625"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGMETRICS Perform. Eval. Rev."],"published-print":{"date-parts":[[2008,3]]},"abstract":"<jats:p>Probabilistic model checking is a formal verification framework for systems which exhibit stochastic behaviour. It has been successfully applied to a wide range of domains, including security and communication protocols, distributed algorithms and power management. In this paper we demonstrate its applicability to the analysis of biological pathways and show how it can yield a better understanding of the dynamics of these systems. Through a case study of the MAP (Mitogen-Activated Protein) Kinase cascade, we explain how biological pathways can be modelled in the probabilistic model checker PRISM and how this enables the analysis of a rich selection of quantitative properties.<\/jats:p>","DOI":"10.1145\/1364644.1364651","type":"journal-article","created":{"date-parts":[[2008,4,29]],"date-time":"2008-04-29T13:01:12Z","timestamp":1209474072000},"page":"14-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":65,"title":["Using probabilistic model checking in systems biology"],"prefix":"10.1145","volume":"35","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[{"name":"Oxford University, Oxford"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[{"name":"Oxford University, Oxford"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[{"name":"Oxford University, Oxford"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,3]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343402"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"e_1_2_1_3_1","first-page":"1","article-title":"Modelling the influence of RKIP on the ERK signalling pathway using the stochastic process algebra PEPA","volume":"7","author":"Calder M.","year":"2006","unstructured":"M. Calder , S. Gilmore , and J. Hillston . Modelling the influence of RKIP on the ERK signalling pathway using the stochastic process algebra PEPA . Trans. Computational Systems Biology , 7 : 1 -- 23 , 2006 . M. Calder, S. Gilmore, and J. Hillston. Modelling the influence of RKIP on the ERK signalling pathway using the stochastic process algebra PEPA. Trans. Computational Systems Biology, 7:1--23, 2006.","journal-title":"Trans. Computational Systems Biology"},{"key":"e_1_2_1_4_1","first-page":"44","article-title":"Analysis of signalling pathways using continuous time Markov chains","volume":"4","author":"Calder M.","year":"2006","unstructured":"M. Calder , V. Vyshemirsky , D. Gilbert , and R. Orton . Analysis of signalling pathways using continuous time Markov chains . Trans. Computational Systems Biology , 4 : 44 -- 67 , 2006 . M. Calder, V. Vyshemirsky, D. Gilbert, and R. Orton. Analysis of signalling pathways using continuous time Markov chains. Trans. Computational Systems Biology, 4:44--67, 2006.","journal-title":"Trans. Computational Systems Biology"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2005.64"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2007.23"},{"key":"e_1_2_1_8_1","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":"Proc. 12th Conf. Correct Hardware Design and Verification Methods (CHARME","author":"Emerson E.","year":"2003","unstructured":"E. Emerson and T. Wahl . On combining symmetry reduction and symbolic representation for efficientc model checking . In D. Geist and E. Tronci, editors, Proc. 12th Conf. Correct Hardware Design and Verification Methods (CHARME 2003 ), volume 2860 of Lecture Notes in Computer Science , pages 216 -- 230 . Springer , 2003. E. Emerson and T. Wahl. On combining symmetry reduction and symbolic representation for efficientc model checking. In D. Geist and E. Tronci, editors, Proc. 12th Conf. Correct Hardware Design and Verification Methods (CHARME 2003), volume 2860 of Lecture Notes in Computer Science, pages 216--230. Springer, 2003."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1021\/j100540a008"},{"key":"e_1_2_1_10_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/3-540-58021-2_20","volume-title":"Proc. 7th Int. Conf. Modelling Techniques and Tools for Computer Performance Evaluation","author":"Gilmore S.","year":"1994","unstructured":"S. Gilmore and J. Hillston . The PEPA workbench: A tool to support a process algebra-based approach to performance modelling . In G. Haring and G. Kotsis, editors, Proc. 7th Int. Conf. Modelling Techniques and Tools for Computer Performance Evaluation , volume 794 of LNCS , pages 353 -- 368 . Springer , 1994 . S. Gilmore and J. Hillston. The PEPA workbench: A tool to support a process algebra-based approach to performance modelling. In G. Haring and G. Kotsis, editors, Proc. 7th Int. Conf. Modelling Techniques and Tools for Computer Performance Evaluation, volume 794 of LNCS, pages 353--368. Springer, 1994."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.11.013"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100072"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/236373"},{"key":"e_1_2_1_15_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Proc. 12th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06)","author":"Hinton A.","year":"2006","unstructured":"A. Hinton , M. Kwiatkowska , G. Norman , and D. Parker . PRISM: A tool for automatic verification of probabilistic systems . In H. Hermanns and J. Palsberg, editors, Proc. 12th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06) , volume 3920 of Lecture Notes in Computer Science , pages 441 -- 444 . Springer , 2006 . 10.1007\/11691372_29 A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker. PRISM: A tool for automatic verification of probabilistic systems. In H. Hermanns and J. Palsberg, editors, Proc. 12th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), volume 3920 of Lecture Notes in Computer Science, pages 441--444. Springer, 2006. 10.1007\/11691372_29"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.93.19.10078"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2005.2"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0140-2"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1059816.1059820"},{"key":"e_1_2_1_20_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1007\/11817963_23","volume-title":"Proc. 18th Int. Conf. Computer Aided Verification (CAV'06)","author":"Kwiatkowska M.","year":"2006","unstructured":"M. Kwiatkowska , G. Norman , and D. Parker . Symmetry reduction for probabilistic model checking . In T. Ball and R. Jones, editors, Proc. 18th Int. Conf. Computer Aided Verification (CAV'06) , volume 4114 of Lecture Notes in Computer Science , pages 234 -- 248 . Springer , 2006 . 10.1007\/11817963_23 M. Kwiatkowska, G. Norman, and D. Parker. Symmetry reduction for probabilistic model checking. In T. Ball and R. Jones, editors, Proc. 18th Int. Conf. Computer Aided Verification (CAV'06), volume 4114 of Lecture Notes in Computer Science, pages 234--248. Springer, 2006. 10.1007\/11817963_23"},{"key":"e_1_2_1_21_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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'07)","author":"Kwiatkowska M.","year":"2007","unstructured":"M. Kwiatkowska , G. Norman , and D. Parker . Stochastic model checking . In M. Bernardo and J. Hillston, editors, Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07) , volume 4486 of Lecture Notes in Computer Science , pages 220 -- 270 . Springer , 2007 . M. Kwiatkowska, G. Norman, and D. Parker. Stochastic model checking. In M. Bernardo and J. Hillston, editors, Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07), volume 4486 of Lecture Notes in Computer Science, pages 220--270. Springer, 2007."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.08.072"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2007.27"},{"key":"e_1_2_1_25_1","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/978-3-540-75140-3_13","volume-title":"Proc. 5th Int. Conf. Computational Methods in Systems Biology (CMSB'07)","author":"Phillips A.","year":"2007","unstructured":"A. Phillips and L. Cardelli . Efficient, correct simulation of biological processes in the stochastic &pi;-calculus . In M. Calder and S. Gilmore, editors, Proc. 5th Int. Conf. Computational Methods in Systems Biology (CMSB'07) , volume 4695 of Lecture Notes in Bioinformatics , pages 184 -- 199 . Springer Verlag , 2007 . A. Phillips and L. Cardelli. Efficient, correct simulation of biological processes in the stochastic &pi;-calculus. In M. Calder and S. Gilmore, editors, Proc. 5th Int. Conf. Computational Methods in Systems Biology (CMSB'07), volume 4695 of Lecture Notes in Bioinformatics, pages 184--199. Springer Verlag, 2007."},{"key":"e_1_2_1_26_1","unstructured":"PRISM web site. http:\/\/www.prismmodelchecker.org\/.  PRISM web site. http:\/\/www.prismmodelchecker.org\/."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/38.7.578"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(01)00214-9"},{"key":"e_1_2_1_29_1","volume-title":"Proc. 3rd Int. Workshop Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems (MTCoord 2007","author":"Pronk T.","year":"2007","unstructured":"T. Pronk , E. de Vink , D. Bosnacki , and T. Breit . Stochastic modeling of Codon bias with PRISM. In I. Linden and C. Talcott, editors , Proc. 3rd Int. Workshop Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems (MTCoord 2007 ). Computer Science Department, University of Cyprus, Nicosia , 2007 . T. Pronk, E. de Vink, D. Bosnacki, and T. Breit. Stochastic modeling of Codon bias with PRISM. In I. Linden and C. Talcott, editors, Proc. 3rd Int. Workshop Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems (MTCoord 2007). Computer Science Department, University of Cyprus, Nicosia, 2007."},{"key":"e_1_2_1_30_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1007\/11963516_30","volume-title":"Proc. 7th Int. Workshop Membrane Computing (WMC06)","author":"Romero-Campero F.","year":"2006","unstructured":"F. Romero-Campero , M. Gheorghe , L. Bianco , D. Pescini , M. Prez-Jimnez , and R. Ceterchi . Towards probabilistic model checking on P Systems using PRISM . In H. Hoogeboom, G. Paun, G. Rozenberg, and A. Salomaa, editors, Proc. 7th Int. Workshop Membrane Computing (WMC06) , volume 4361 of Lecture Notes in Computer Science , pages 477 -- 495 . Springer , 2006 . 10.1007\/11963516_30 F. Romero-Campero, M. Gheorghe, L. Bianco, D. Pescini, M. Prez-Jimnez, and R. Ceterchi. Towards probabilistic model checking on P Systems using PRISM. In H. Hoogeboom, G. Paun, G. Rozenberg, and A. Salomaa, editors, Proc. 7th Int. Workshop Membrane Computing (WMC06), volume 4361 of Lecture Notes in Computer Science, pages 477--495. Springer, 2006. 10.1007\/11963516_30"},{"key":"e_1_2_1_31_1","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":"Rutten J.","year":"2004","unstructured":"J. Rutten , M. Kwiatkowska , G. Norman , and D. Parker . Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems , volume 23 of CRM Monograph Series . AMS , 2004 . J. Rutten, M. Kwiatkowska, G. Norman, and D. Parker. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, volume 23 of CRM Monograph Series. AMS, 2004."},{"key":"e_1_2_1_32_1","unstructured":"SBML-to-PRISM translator. http:\/\/www.prismmodelchecker.org\/sbml\/.  SBML-to-PRISM translator. http:\/\/www.prismmodelchecker.org\/sbml\/."},{"key":"e_1_2_1_33_1","unstructured":"SBML web site. http:\/\/sbml.org\/.  SBML web site. http:\/\/sbml.org\/."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNB.2004.833694"},{"key":"e_1_2_1_35_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1007\/11513988_43","volume-title":"Proc. 17th Int. Conf. Computer Aided Verification (CAV'05)","author":"Younes H.","year":"2005","unstructured":"H. Younes . Ymer: A statistical model checker . In K. Etessami and S. Rajamani, editors, Proc. 17th Int. Conf. Computer Aided Verification (CAV'05) , volume 3576 of Lecture Notes in Computer Science , pages 429 -- 433 . Springer , 2005 . 10.1007\/11513988_43 H. Younes. Ymer: A statistical model checker. In K. Etessami and S. Rajamani, editors, Proc. 17th Int. Conf. Computer Aided Verification (CAV'05), volume 3576 of Lecture Notes in Computer Science, pages 429--433. Springer, 2005. 10.1007\/11513988_43"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-005-0187-8"}],"container-title":["ACM SIGMETRICS Performance Evaluation Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1364644.1364651","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1364644.1364651","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:56:11Z","timestamp":1750254971000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1364644.1364651"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,3]]},"references-count":35,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2008,3]]}},"alternative-id":["10.1145\/1364644.1364651"],"URL":"https:\/\/doi.org\/10.1145\/1364644.1364651","relation":{},"ISSN":["0163-5999"],"issn-type":[{"value":"0163-5999","type":"print"}],"subject":[],"published":{"date-parts":[[2008,3]]},"assertion":[{"value":"2008-03-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}