Prism — An Overview

Abstract

• PRISM is a probabilistic model checker − automatic verification of systems with stochastic behaviour − e.g. due to unreliability, uncertainty, randomisation, … • Construction/analysis of probabilistic models… − discrete-and continuous-time Markov chains, Markov decision processes, probabilistic timed automata − modelling language, case study repository, benchmark suite • Verification of properties in probabilistic temporal logics… − PCTL, CSL, LTL, PCTL*, quantitative extensions, costs/rewards • Various model checking engines and techniques… − symbolic (multi-terminal BDDs), explicit-state data structures, symmetry reduction, quantitative abstraction refinement, simulation-based (approximate/statistical model checking), …