{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,21]],"date-time":"2026-04-21T14:55:38Z","timestamp":1776783338716,"version":"3.51.2"},"reference-count":16,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2009,3,25]],"date-time":"2009-03-25T00:00:00Z","timestamp":1237939200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGMETRICS Perform. Eval. Rev."],"published-print":{"date-parts":[[2009,3,25]]},"abstract":"<jats:p>Probabilistic model checking is a formal verification technique for the modelling and analysis of stochastic systems. It has proved to be useful for studying a wide range of quantitative properties of models taken from many diffierent application domains. This includes, for example, performance and reliability properties of computer and communication systems. In this paper, we give an overview of the probabilistic model checking tool PRISM, focusing in particular on its support for continuous-time Markov chains and Markov reward models, and how these can be used to analyse performability properties.<\/jats:p>","DOI":"10.1145\/1530873.1530882","type":"journal-article","created":{"date-parts":[[2009,4,21]],"date-time":"2009-04-21T14:14:44Z","timestamp":1240323284000},"page":"40-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":198,"title":["PRISM"],"prefix":"10.1145","volume":"36","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[{"name":"Oxford University Computing Laboratory, Oxford"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[{"name":"Oxford University Computing Laboratory, Oxford"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[{"name":"Oxford University Computing Laboratory, Oxford"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2009,3,25]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008739929481"},{"key":"e_1_2_1_2_1","series-title":"LNCS","first-page":"269","volume-title":"Proc. CAV'96","author":"Aziz A.","year":"1996","unstructured":"A. Aziz , K. Sanwal , V. Singhal , and R. Brayton . Verifying continuous time Markov chains . In Proc. CAV'96 , volume 1102 of LNCS , pages 269 -- 276 . Springer , 1996 . A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Verifying continuous time Markov chains. In Proc. CAV'96, volume 1102 of LNCS, pages 269--276. Springer, 1996."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008699807402"},{"key":"e_1_2_1_4_1","series-title":"LNCS","first-page":"780","volume-title":"Proc. ICALP'00","author":"Baier C.","year":"2000","unstructured":"C. Baier , B. Haverkort , H. Hermanns , and J.-P. Katoen . On the logical characterisation of performability properties . In Proc. ICALP'00 , volume 1853 of LNCS , pages 780 -- 792 . Springer , 2000 . C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. On the logical characterisation of performability properties. In Proc. ICALP'00, volume 1853 of LNCS, pages 780--792. Springer, 2000."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"e_1_2_1_6_1","series-title":"LNCS","first-page":"146","volume-title":"Proc. CONCUR'99","author":"Baier C.","year":"1999","unstructured":"C. Baier , J.-P. Katoen , and H. Hermanns . Approximate symbolic model checking of continuous-time Markov chains . In J. Baeten and S. Mauw, editors, Proc. CONCUR'99 , volume 1664 of LNCS , pages 146 -- 161 . Springer , 1999 . C. Baier, J.-P. Katoen, and H. Hermanns. Approximate symbolic model checking of continuous-time Markov chains. In J. Baeten and S. Mauw, editors, Proc. CONCUR'99, volume 1664 of LNCS, pages 146--161. Springer, 1999."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008647823331"},{"key":"e_1_2_1_8_1","volume-title":"Model Checking","author":"Clarke E.","year":"1999","unstructured":"E. Clarke , O. Grumberg , and D. Peled . Model Checking . The MIT Press , 1999 . E. Clarke, O. Grumberg, and D. Peled. Model Checking. The MIT Press, 1999."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_10_1","volume-title":"Chapman & Hall","author":"Kulkarni V.","year":"1995","unstructured":"V. Kulkarni . Modeling and Analysis of Stochastic Systems . Chapman & Hall , 1995 . V. Kulkarni. Modeling and Analysis of Stochastic Systems. Chapman & Hall, 1995."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0140-2"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.conengprac.2006.07.003"},{"key":"e_1_2_1_13_1","series-title":"LNCS","first-page":"220","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 LNCS , 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 LNCS, pages 220--270. Springer, 2007."},{"issue":"2","key":"e_1_2_1_14_1","first-page":"9","article-title":"Stochastic reward nets for reliability prediction. Communications in Reliability","volume":"1","author":"Muppala J.","year":"1994","unstructured":"J. Muppala , G. Ciardo , and K. Trivedi . Stochastic reward nets for reliability prediction. Communications in Reliability , Maintainability and Serviceability , 1 ( 2 ): 9 -- 20 , 1994 . J. Muppala, G. Ciardo, and K. Trivedi. Stochastic reward nets for reliability prediction. Communications in Reliability, Maintainability and Serviceability, 1(2):9--20, 1994.","journal-title":"Maintainability and Serviceability"},{"key":"e_1_2_1_16_1","unstructured":"PRISM web site. www.prismmodelchecker.org.  PRISM web site. www.prismmodelchecker.org."},{"key":"e_1_2_1_17_1","volume-title":"Introduction to the Numerical Solution of Markov Chains","author":"Stewart W.J.","year":"1994","unstructured":"W.J. Stewart . Introduction to the Numerical Solution of Markov Chains . Princeton , 1994 . W.J. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton, 1994."}],"container-title":["ACM SIGMETRICS Performance Evaluation Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1530873.1530882","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1530873.1530882","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:23Z","timestamp":1750253423000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1530873.1530882"}},"subtitle":["probabilistic model checking for performance and reliability analysis"],"short-title":[],"issued":{"date-parts":[[2009,3,25]]},"references-count":16,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,3,25]]}},"alternative-id":["10.1145\/1530873.1530882"],"URL":"https:\/\/doi.org\/10.1145\/1530873.1530882","relation":{},"ISSN":["0163-5999"],"issn-type":[{"value":"0163-5999","type":"print"}],"subject":[],"published":{"date-parts":[[2009,3,25]]},"assertion":[{"value":"2009-03-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}