{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:04:11Z","timestamp":1776373451305,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540435396","type":"print"},{"value":"9783540460299","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46029-2_13","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T01:26:30Z","timestamp":1180661190000},"page":"200-204","source":"Crossref","is-referenced-by-count":305,"title":["PRISM: Probabilistic Symbolic Model Checker"],"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":[[2002,4,10]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur and T. Henzinger. Reactive modules. In Proc. LICS\u201996, 1996.","DOI":"10.1109\/LICS.1996.561320"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"J. Aspnes and M. Herlihy. Fast Randomized Consensus using Shared Memory. Journal of Algorithms, 15(1), 1990.","DOI":"10.1016\/0196-6774(90)90021-6"},{"key":"13_CR3","unstructured":"C. Baier. On algorithmic verification methods for probabilistic systems. Universit\u00e4t Mannheim, 1998."},{"key":"13_CR4","series-title":"Lect Notes Comput Sci","volume-title":"CAV 2000","author":"C. Baier","year":"2000","unstructured":"C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model checking continuous-time Markov chains by transient analysis. In CAV 2000, volume 1855 of LNCS, 2000."},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"C. Baier and M. Kwiatkowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11(3), 1998.","DOI":"10.1007\/s004460050046"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Proc. FST & TCS, 1995.","DOI":"10.21236\/ADA461346"},{"key":"13_CR7","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. LICS\u201990, 1990."},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"C. Cachin, K. Kursawe, and V. Shoup. Random oracles in Constantinople: Practical asynchronous Byzantine agreement using cryptography (extended abstract). In Proc. PODC\u201900, 2000.","DOI":"10.1145\/343477.343531"},{"key":"13_CR9","unstructured":"G. Ciardo and M. Tilgner. On the use of Kronecker operators for the solution of generalized stocastic Petri nets. ICASE Report 96-35, Institute for Computer Applications in Science and Engineering, 1996."},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"E. Clarke, M. Fujita, P. McGeer, J. Yang, and X. Zhao. Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. In Proc. IWLS\u201993, 1993.","DOI":"10.1007\/978-1-4613-1385-4_4"},{"key":"13_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Proc. TACAS 2000","author":"L. Alfaro de","year":"2000","unstructured":"L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, and R. Segala. Symbolic model checking of concurrent probabilistic processes using MTBDDs and the Kronecker representation. In Proc. TACAS 2000, volume 1785 of LNCS, 2000."},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"H. Hansson and B. Jonsson. A logic for reasoning about time and probability. Formal Aspects of Computing, 6, 1994.","DOI":"10.1007\/BF01211866"},{"key":"13_CR13","series-title":"Lect Notes Comput Sci","volume-title":"Proc. TACAS 2000","author":"H. Hermanns","year":"2000","unstructured":"H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. A Markov Chain Model Checker. In Proc. TACAS 2000, volume 1785 of LNCS, 2000."},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"O. Ibe and K. Trivedi. Stochastic Petri net models of polling systems. IEEE Journal on Selected Areas in Communications, 8(9), 1990.","DOI":"10.1109\/49.62852"},{"key":"13_CR15","series-title":"Lect Notes Comput Sci","volume-title":"PAPM\/PROBMIV\u201901","author":"J.-P. Katoen","year":"2001","unstructured":"J.-P. Katoen, M. Kwiatkowska, G. Norman, and D. Parker. Faster and symbolic ctmc model checking. In PAPM\/PROBMIV\u201901, volume 2165 of LNCS, 2001."},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic symbolic model checking with PRISM: A hybrid approach. In Proc. TACAS 2002, 2002. To appear.","DOI":"10.1007\/3-540-46002-0_5"},{"key":"13_CR17","series-title":"Lect Notes Comput Sci","volume-title":"Proc. CAV\u201901","author":"M. Kwiatkowska","year":"2001","unstructured":"M. Kwiatkowska, G. Norman, and R. Segala. Automated verification of a randomized distributed consensus protocol using Cadence SMV and PRISM. In Proc. CAV\u201901, volume 2102 of LNCS, 2001."},{"key":"13_CR18","unstructured":"PRISM web page. http:\/\/www.cs.bham.ac.uk\/~dxp\/prism\/ ."},{"key":"13_CR19","volume-title":"CUDD: CU Decision Diagram package","author":"F. Somenzi","year":"1997","unstructured":"F. Somenzi. CUDD: CU Decision Diagram package. Public software, Colorado University, Boulder, 1997."},{"key":"13_CR20","unstructured":"W. Stewart. MARCA: Marcov chain analyzer. a software package for Markov modelling. In Proc. NSMC\u201991, 1991."}],"container-title":["Lecture Notes in Computer Science","Computer Performance Evaluation: Modelling Techniques and Tools"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46029-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T11:25:02Z","timestamp":1556450702000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46029-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540435396","9783540460299"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-46029-2_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}