Affordable Access

Stochastic model checking

Publication Date
  • Qa75 Electronic Computers. Computer Science
  • Biology
  • Computer Science
  • Mathematics


This tutorial presents an overview of model checking for both discrete and continuous-time Markov chains (DTMCs and CTMCs). Model checking algorithms are given for verifying DTMCs and CTMCs against specifications written in probabilistic extensions of temporal logic, including quantitative properties with rewards. Example properties include the probability that a fault occurs and the expected number of faults in a given time period. We also describe the practical application of stochastic model checking with the probabilistic model checker PRISM by outlining the main features supported by PRISM and three real-world case studies: a probabilistic security protocol, dynamic power management and a biological pathway.

There are no comments yet on this publication. Be the first to share your thoughts.