Modeling and Verification of Probabilistic Systems

News

  • 11.09.2018: We are online.

Schedule

Type Day Time Room Start Lecturer
Lecture Mon 10:30 – 12:00h 5056 8. 10. Katoen
  Tue 08:30 – 10:00h 5056 9.10. Katoen
Exercise Wed 14:30 – 16:00h AH VI 24.10. Spel, Quatmann

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:

  1. How to obtain models for complex systems that involve random aspects?
  2. How to verify in a fully algorithmic manner, whether such models satisfy basic properties, such as reachability probabilities?
  3. Can we make these models smaller to enable or simplify their verification?
  4. 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.

Slides

No. Date Subject Slides Notes
1  8.10  Introduction/Probability Refresher  mvps2018_lec01  
2  9.10  Discrete-Time Markov Chains  mvps2018_lec02  notes02
3  15.10  Reachability Probabilities  mvps2018_lec03  notes03
4  22.10  Qualitative Properties  mvps2018_lec04  notes04
5  23.10  Verifying Linear-Time Properties (1)  mvps2018_lec05  notes05-6
6  29.10  Verifying Linear-Time Properties (2)    
7  30.10  Probabilistic CTL  mvps2018_lec07  notes07
8  5.11  Qualitative PCTL versus CTL  mvps2018_lec08  notes08
9  6.11  Probabilistic Bisimulation (1)  mvps2018_lec09  notes09+10
10  12.11  Probabilistic Bisimulation (2)    
11  13.11  Markov Decision Processes  mvps2018_lec11  notes11
12  19.11  Reachability Probabilities in MDPs (1)  mvps2018_lec12  notes12
13  20.11  Reachability Probabilities in MDPs (2)    
14  26.11  MDP Model Checking  mvps2018_lec14  notes14
15  27.11  Continuous-Time Markov Chains  mvps2018_lec15  notes15
16  4.12  Transient Analysis in CTMCs  mvps2018_lec16  notes16
17  10.12  Timed Reachability in CTMCs  mvps2018_lec17  
18  11.12      
19  17.12      
20  18.12      
21  07.01      
22  08.01      
23  14.01      
24  15.01      

Exercises

No. Due Exercise
 1 24.10. ex01
2 31.10. ex02
3 07.11. ex03
4 14.11. ex04
5 21.11. ex05
6 28.11. ex06
7 05.12. ex07
8 12.12 ex08
9  19.12 ex09

Further information

  • The course will be entirely given in English.
  • There are no lecture notes (yet); the course material will consist of slides.
  • The written exam will be awarded with 6 ECTS credits.
  • The exam dates are: February 18, 2019 (10:00-12:00) and March 13, 2019 (10:00-12:00)

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