• 03.05.: First lecture: Basics of model checking (Slides)
  • 10.05.: Second lecture: Presenting the papers
  • 17.05.: Third lecture: Detailed theoretical background and selection of papers
  • 24.05.: No lecture (FVV). Time to read your papers.
  • 31.05.: Final lecture: Technical introduction to the codebase and time for questions
  • Roughly 01.06.-01.08.: Group work
  • 05.07. at 10:00: Midterm presentations (different room: 03.09.012)
  • Beginning of August: Endterm presentations


Title Supervisor Links Slides Focus
Approximating Values of Generalized-Reachability Stochastic Games Maxi

Download 1. Theory
2. Implementation
LTL-Constrained Steady-State Policy Synthesis Jan
[Youtube-video to come]
[Slides to come] 1. Theory
2. Implementation
Reinforcement Learning with Decision Trees Steffi
Download 1. Implementation
2. Evaluation
Correct Probabilistic Model Checking with Floating-Point Arithmetic Alex Download 1. Evaluation
2. Implementation

Model checkers

The first two papers use PRISM; the first one the specific branch PRISM-Games.
The latter two papers extend Storm.