%0 Conference Paper %1 10.1007/3-540-46029-2_13 %A Kwiatkowska, Marta %A Norman, Gethin %A Parker, David %B Computer Performance Evaluation: Modelling Techniques and Tools %C Berlin, Heidelberg %D 2002 %E Field, Tony %E Harrison, Peter G. %E Bradley, Jeremy %E Harder, Uli %I Springer Berlin Heidelberg %K markov model-checking probabilistic %P 200--204 %T PRISM: Probabilistic Symbolic Model Checker %X In this paper we describe PRISM, a tool being developed at the University of Birmingham for the analysis of probabilistic systems. PRISM supports three probabilistic models: discrete-time Markov chains, Markov decision processes and continuous-time Markov chains. Analysis is performed through model checking such systems against specifications written in the probabilistic temporal logics PCTL and CSL. The tool features three model checking engines: one symbolic, using BDDs (binary decision diagrams) and MTBDDs (multi-terminal BDDs); one based on sparse matrices; and one which combines both symbolic and sparse matrix methods. PRISM has been successfully used to analyse probabilistic termination, performance, and quality of service properties for a range of systems, including randomized distributed algorithms, manufacturing systems and workstation clusters. %@ 978-3-540-46029-9

@inproceedings{10.1007/3-540-46029-2_13, abstract = {In this paper we describe PRISM, a tool being developed at the University of Birmingham for the analysis of probabilistic systems. PRISM supports three probabilistic models: discrete-time Markov chains, Markov decision processes and continuous-time Markov chains. Analysis is performed through model checking such systems against specifications written in the probabilistic temporal logics PCTL and CSL. The tool features three model checking engines: one symbolic, using BDDs (binary decision diagrams) and MTBDDs (multi-terminal BDDs); one based on sparse matrices; and one which combines both symbolic and sparse matrix methods. PRISM has been successfully used to analyse probabilistic termination, performance, and quality of service properties for a range of systems, including randomized distributed algorithms, manufacturing systems and workstation clusters.}, added-at = {2020-03-20T14:38:35.000+0100}, address = {Berlin, Heidelberg}, author = {Kwiatkowska, Marta and Norman, Gethin and Parker, David}, biburl = {https://www.bibsonomy.org/bibtex/2d7d5944225468d80c1cb06eee4e23ad1/maximeb}, booktitle = {Computer Performance Evaluation: Modelling Techniques and Tools}, editor = {Field, Tony and Harrison, Peter G. and Bradley, Jeremy and Harder, Uli}, interhash = {251bcd0231e96c8e18e50b3c7cf1a8e3}, intrahash = {d7d5944225468d80c1cb06eee4e23ad1}, isbn = {978-3-540-46029-9}, keywords = {markov model-checking probabilistic}, pages = {200--204}, publisher = {Springer Berlin Heidelberg}, timestamp = {2020-03-20T14:38:35.000+0100}, title = {PRISM: Probabilistic Symbolic Model Checker}, year = 2002 }