Instructors

Overview

Timeplan

  • 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

Papers

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

https://dl.acm.org/doi/10.1145/3373718.3394761

https://www.youtube.com/watch?v=my7tOrom1Fg

Download 1. Theory
2. Implementation
LTL-Constrained Steady-State Policy Synthesis Jan

https://www.ijcai.org/proceedings/2021/565

[Youtube-video to come]

[Slides to come] 1. Theory
2. Implementation
Reinforcement Learning with Decision Trees Steffi

https://www.cs.colostate.edu/pubserv/pubs/Pyeatt-TechReports-Reports-1998-tr98-112.pdf

https://arxiv.org/pdf/1907.01180

Download 1. Implementation
2. Evaluation
Correct Probabilistic Model Checking with Floating-Point Arithmetic Alex

https://link.springer.com/chapter/10.1007/978-3-030-99527-0_3

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.