Probabilistic Model Checking

Model checking is a formal method for deciding whether or not a finite-state model of a system meets a given specification, where the latter includes for example liveness and safety requirements. Hence, in contrast to testing and simulation, model checking yields a method that provides absolute guarantees of correctness with respect to the given specification. In this purely qualitative setting the result of model checking is either YES or NO (probably enriched with a counterexample). In practice such rigid notions are hard, or even impossible, to guarantee for many relevant properties, as e.g., when hardware failures or message losses can happen with certain (low) probabilities. Other reasons for observing stochastic behavior can be located within the system design itself, as, e.g., in case of randomized algorithms. But stochastic distributions and rates play also an important role when used as abstraction of runtime phenomena, e.g. when characterizing the workload put onto a system by external user(s).

The focus of this lecture will be on probabilistic model checking (PMC) that enables a quantitative analysis of systems that exhibit stochastic behavior. On the basis of stochastic operational models, such as Markov chains and Markov decision processes that extend transition systems with probabilities and rates, we will study the theory and application of PMC for computing various quantitative measures. The latter include probabilities for temporal events, expectations of random variables (modeling, e.g., costs or utility) and other, more complex multi-objective measures. The practical part of the lecture consists of exercises related to the theory as well as basic modeling and analysis tasks to be solved using a probabilistic model checker such as PRISM or Storm