Switch to English
Cursus: 202100113
Probabilistic Model Checking (Software Science)
Cursus informatie
Studiepunten (ECTS)5
Contactpersoondr. A. Hartmanns
Docent E.M. Hahn
dr. A. Hartmanns
Contactpersoon van de cursus
dr. A. Hartmanns
AanmeldingsprocedureZelf aanmelden via OSIRIS Student
Inschrijven via OSIRISJa
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.

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
Verplicht materiaal
Aanbevolen materiaal
Course material
Papers will be provided via Canvas

Project onbegeleid


Project, Exam

Switch to English