Probabilistic Model Checking

Dr. Sascha Klüppelholz
SWS: (1/1/0), in English

Changed proceedings due to COVID-19 outbreak

Due to the recent outbreak of the COVID-19 virus, the university has decided not to carry out any events with mandatory attendance at least until 4^th May 2020 (as of 19^th March). Lectures and exercises from the start of the Semester (in the week from 6th April) up until the start of teaching events with mandatory attendance are instead provided with online alternatives via OPAL.

Please inform yourself about current developments and decisions of the university at https://tu-dresden.de/corona and https://tu-dresden.de/studium/im-studium/coronavirus/

Please revisit this site and https://tu-dresden.de/corona from time to time to stay up to date.

Description

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.

Dates

Within this time slot, either there will be a lecture or tutorial session.

Registration

Please enroll via OPAL.

Prerequisites

Knowledge from the lecture on Model Checking is benefitial, but not a formal requirement or prerequisite.

Creditability

Bachelor Informatik

• INF-B-510: Vertiefung
• INF-B-520: Vertiefung zur Bachelor-Arbeit

Master Informatik

• INF-BAS6: Basismodul Theoretische Informatik
• INF-VERT6: Vertiefungsmodul Theoretische Informatik

Master Computational Logic

• MCL-TCSL: Theoretical Computer Science and Logic

Diplom Informatik

• INF-BAS6: Basismodul Theoretische Informatik
• INF-VERT6: Vertiefungsmodul Theoretische Informatik

Course Material

The course mainly follows material from Chapter 10 of "Principles of Model Checking" by Christel Baier and Joost-Pieter Katoen (MIT Press). The relevant parts will be made available via OPAL.

Exercises

Here and/or in OPAL, you will find the sheets for the upcoming exercise in PDF format.

Contact