{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:56Z","timestamp":1761611216158},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540434191"},{"type":"electronic","value":"9783540460022"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46002-0_5","type":"book-chapter","created":{"date-parts":[[2007,10,28]],"date-time":"2007-10-28T02:29:59Z","timestamp":1193538599000},"page":"52-66","source":"Crossref","is-referenced-by-count":75,"title":["Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach"],"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,3,14]]},"reference":[{"key":"5_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":"5_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":"5_CR3","doi-asserted-by":"crossref","unstructured":"I. Bahar, E. Frohm, C. Gaona, G. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic decision diagrams and their applications. In Proc. ICCAD\u201993, 1993.","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"5_CR4","unstructured":"C. Baier. On algorithmic verification methods for probabilistic systems. Habilitation thesis, Universit\u00e4t Mannheim, 1998."},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"C. Baier, E. Clarke, V. Hartonas-Garmhausen, M. Kwiatkowska, and M. Ryan. Symbolic model checking for probabilistic processes. In Proc. ICALP\u201997, 1997.","DOI":"10.1007\/3-540-63165-8_199"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model checking continuous-time Markov chains by transient analysis. In Proc. CAV\u201900, 2000.","DOI":"10.1007\/10722167_28"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"C. Baier, J.-P. Katoen, and H. Hermanns. Approximative symbolic model checking of continuous-time Markov chains. In Proc. CONCUR\u201999, 1999.","DOI":"10.1007\/3-540-48320-9_12"},{"key":"5_CR8","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":"5_CR9","doi-asserted-by":"crossref","unstructured":"F. Bause, P. Buchholz, and P. Kemper. A toolbox for functional and quantitative analysis of DEDS. In Computer Performance Evaluation (Tools), 1998.","DOI":"10.1007\/3-540-68061-6_32"},{"key":"5_CR10","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":"5_CR11","doi-asserted-by":"crossref","unstructured":"R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"P. Buchholz and P. Kemper. Compact representations of probability distributions in the analysis of superposed GSPNs. In Proc. PNPM\u201901, 2001.","DOI":"10.1109\/PNPM.2001.953358"},{"key":"5_CR13","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":"5_CR14","unstructured":"G. Ciardo and A. Miner. SMART: Simulation and Markovian analyser for reliability and timing. In Tool Descriptions from PNPM\u201997, 1997."},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"G. Ciardo and A. Miner. A data structure for the efficient Kronecker solution of GSPNs. In Proc. PNPM\u201999, 1999.","DOI":"10.1109\/PNPM.1999.796529"},{"key":"5_CR16","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":"5_CR17","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":"5_CR18","doi-asserted-by":"crossref","unstructured":"P. D'Argenio, B. Jeannet, H. Jensen, and K. Larsen. Reachability analysis of probabilistic systems by successive refinements. In Proc. PAPM\/PROBMIV\u201901, 2001.","DOI":"10.1007\/3-540-44804-7_3"},{"key":"5_CR19","doi-asserted-by":"crossref","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\u201900, 2000.","DOI":"10.1007\/3-540-46419-0_27"},{"key":"5_CR20","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":"5_CR21","doi-asserted-by":"crossref","unstructured":"V. Hartonas-Garmhausen, S. Campos, and E. Clarke. ProbVerus: Probabilistic symbolic model checking. In Proc. ARTS\u201999, 1999.","DOI":"10.1007\/3-540-48778-6_6"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. A Markov chain model checker. In Proc. TACAS\u201900, 2000.","DOI":"10.1007\/3-540-46419-0_24"},{"key":"5_CR23","unstructured":"H. Hermanns, J. Meyer-Kayser, and M. Siegle. Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In Proc. NSMC\u201999, 1999."},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"A. Itai and M. Rodeh. Symmetry breaking in distributed networks. Information and Computation, 88(1), 1990.","DOI":"10.1016\/0890-5401(90)90004-2"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"J.-P. Katoen, M. Kwiatkowska, G. Norman, and D. Parker. Faster and symbolic CTMC model checking. In Proc. PAPM-PROBMIV\u201901, 2001.","DOI":"10.1007\/3-540-44804-7_2"},{"key":"5_CR26","unstructured":"M. Kwiatkowska, G. Norman, D. Parker, and R. Segala. Symbolic model checking of concurrent probabilistic systems using MTBDDs and Simplex. Technical Report CSR-99-1, School of Computer Science, University of Birmingham, 1999."},{"key":"5_CR27","doi-asserted-by":"crossref","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, 2001.","DOI":"10.1007\/3-540-44585-4_17"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"5_CR29","unstructured":"D. Parker. Implementation of symbolic model checking for probabilistic systems. PhD thesis, University of Birmingham, 2002. To appear."},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"B. Plateau. On the stochastic structure of parallelism and synchronisation models for distributed algorithms. In Proc. 1985 ACM SIGMETRICS Conference on Measurement and Modeling of Computer Systems, 1985.","DOI":"10.1145\/317795.317819"},{"key":"5_CR31","unstructured":"PRISM web page. http:\/\/www.cs.bham.ac.uk\/~dxp\/prism\/ ."},{"key":"5_CR32","volume-title":"Public software","author":"F. Somenzi","year":"1997","unstructured":"F. Somenzi. CUDD: Colorado University decision diagram package. Public software, Colorado Univeristy, Boulder, 1997."},{"key":"5_CR33","unstructured":"W. Stewart. MARCA: Markov chain analyser, a software package for Markov modelling. In Proc. NSMC\u201991, 1991."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46002-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T22:29:13Z","timestamp":1556922553000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46002-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540434191","9783540460022"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-46002-0_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}