News
- 01.04.2021: The timeslots for lecture and exercise as well as the exam dates are indicated below. If you want to take this course please register for the Moodle room. Further organisational info will be published there.
- 15.02.2021: We are online.
Schedule
| Type | Day | Time | Room | (Start) date | Lecturer |
|---|---|---|---|---|---|
| Lecture | Tue | 8:30-10:00 | online | 13.04. | Katoen |
| Fr | 8:30-10:00 | online | 16.04. | Katoen | |
| Exercise | Tue | 12:30-14:00 | online | 27.04. | Winkler, Bork |
| Exam 1 | Wed | 12:00-14:00 | TBA | 25.08. | |
| Exam 2 | Thu | 14:00-16:00 | TBA | 16.09. |
Overview
The aim of this course is to address the compositional modeling and the automated verification (i.e., model checking) of probabilistic models. These models are important for addressing performance aspects, they are the key to randomised distributed algorithms, and have applications in systems biology as well as security, to mention a few. This course is about:
- How to obtain models for complex systems that involve random aspects?
- How to verify in a fully algorithmic manner, whether such models satisfy basic properties, such as reachability probabilities?
- Can we make these models smaller to enable or simplify their verification?
- What kind of practical problems can be treated in this manner?
If you’d like to have an introductory read on this lecture, then you might consider to read the paper “Model Checking Meets Probability: A Gentle Introduction” by Joost-Pieter Katoen. Moreover, the paper “Performance Evaluation and Model Checking Join Forces” published in Communications of the ACM (2010) might be of interest.
Topics
Markov chains, Markov decision processes, probabilistic automata, Markov automata (aka: continuous-time MDPs), model checking, probabilistic temporal logic (probabilistic CTL and LTL), bisimulation, compositional modeling, concurrency, compositional minimisation.
Organization
This course is organized via Moodle. Please register in RWTH Online to get access. Further organisational information can be found in the Moodle room.
Additional background literature
- C. Baier and J.-P. Katoen. Principles of Model Checking, MIT Press, 2008 [Chapter 10].
- H.C. Tijms: A First Course in Stochastic Models. Wiley, 2003.
- J.-P. Katoen. The Probabilistic Model Checking Landscape. LICS 2016.
- H. Hermanns: Interactive Markov Chains: The Quest for Quantified Quality. LNCS 2428, Springer 2002.
- E. Brinksma, H. Hermanns, J.-P. Katoen: Lectures on Formal Methods and Performance Analysis. LNCS 2090, Springer 2001.
- M. Stoelinga: Introduction to Probabilistic Automata. Bulletin of the EATCS 78. 2002
- M. Timmer: Efficient Modelling, Generation and Analysis of Markov Automata. Chapter 3. 2013