Instructors
- Lecturer: Prof. Jan Kretinsky
- Supervisors:
Alexandros Evangelidis, Stefanie Mohr, Maximilian Weininger,
Overview
- Module IN0012, IN2106
- Language: English
- See the description in TUMonline for information on content and prerequisites.
- See the Slides of the pre-meeting for information on course structure and expectations.
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 | 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.