Kies de Nederlandse taal
Course module: 202100113
Probabilistic Model Checking (Software Science)
Course info
Course module202100113
Credits (ECTS)5
Course typeCourse
Language of instructionEnglish
Contact persondr. A. Hartmanns
Lecturer E.M. Hahn
dr. A. Hartmanns
Contactperson for the course
dr. A. Hartmanns
Academic year2022
Starting block
Application procedureYou apply via OSIRIS Student
Registration using OSIRISYes
After successfully completing this course, the student:
  • is able to research, understand, and apply recent scientific results in software science
  • is able to answer software-related research questions on an appropriate level of abstraction
The student acquires: 
  • understanding of LTL and CTL model checking
  • understanding of Markov models and probabilistic model checking
  • practical experience of developing a probabilistic model checker
  • practice in independently studying, analysing, and explaining recent research in probabilistic verification

Software is everywhere, and our society is depending more and more on software working reliably and efficiently. To make it more reliable and efficient, we need to have a thorough understanding of the behavior of software systems, and how we can analyse and improve this behavior. This course gives insights in current research directions in the area of software systems, and how these new ideas can be used to improve software.
The goal of the course Software Science is to teach several topics related to active, on-going research in software engineering and formal methods. Each edition of the course consists of one topic of recent research, presented in lectures complemented with exercise or lab sessions to gain practical experiences with the material introduced during the lectures. Each topic comes with one or more individual homework/project assignments.
If one is interested in more than one topic, it is possible to follow the course a second time choosing a different topic. In this way, one can study 2 topics for 10 ECTS.

Model checking is a classic technique to verify that a system model satisfies a given set of formally stated requirements. Models can be represented as labelled transition systems (LTS); popular requirement languages are CTL and LTL. When systems are subject to stochastic effects, e.g. due to random faults or by using randomised algorithms, we need probabilistic modelling formalisms, probabilistic requirement languages, and probabilistic model checking algorithms. In this course, students learn the mathematical and computer science concepts behind classic and probabilistic model checking - LTS, CTL, LTL, Markov chains, Markov decision processes, probabilistic CTL, etc. - and apply them by implementing their own high-performance probabilistic model checker. Students conclude the course by studying and presenting recent scientific results in probabilistic verification.

Assumed previous knowledge
Knowledge of Markov decision processes and related algorithms such as value iteration or reinforcement learning, as taught in e.g. 191531920 Markov Decision Theory and Algorithmic Methods, 201200006 Quantitative Evaluation of Embedded Systems, 202100109 Reinforcement Learning, or 202001366 Stochastic Models.
Participating study
Master Computer Science
Required materials
Recommended materials
Course material
Papers will be provided via Canvas
Instructional modes

Project unsupervised


Project, Exam

Kies de Nederlandse taal