Affordable Access

Stochastic model checking

Authors
Publisher
Springer
Publication Date
Keywords
  • Qa75 Electronic Computers. Computer Science
Disciplines
  • Biology
  • Computer Science
  • Mathematics

Abstract

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.