- Angeles Carrara
- Julieta Paola Storino
- Mateo Carranza Velez
This report presents an overview and analysis of PRISM, an open-source tool for modeling and formally verifying systems with random or probabilistic behaviors. After introducing the theoretical foundations—such as discrete-time and continuous-time Markov chains, Markov decision processes, and relevant temporal logics (PCTL, CSL)—the document explains the creation and evolution of PRISM, highlighting its active development and widespread use in academia and industry.
PRISM offers both a command-line and graphical interface, enabling users to specify models, properties to verify, and run simulations. The tool’s technical backbone relies on decision diagrams and incorporates optimization techniques for efficient analysis. PRISM provides exact results for qualitative properties and highly accurate numerical results for quantitative analyses.
The report describes several case studies, including protocols and algorithms, and compares PRISM to other tools, showing its strong balance between usability, features, and performance. A detailed, illustrative case study is presented: modeling a probabilistic version of the well-known “river crossing” puzzle, demonstrating PRISM’s capabilities for modeling, property verification, and expected value calculations.
In conclusion, PRISM is highlighted as an easy-to-use, powerful, and versatile tool for probabilistic model checking, with extensive documentation and potential for future applications to classic logic problems.