Modeling and Verification of Probabilistic Systems

News

  • 13.11.2015: We fixed a mistake in the exercise. When listing probabilities for the given properties, one should use a maximizing scheduler.
  • 26.11.2015: Due to technical problems, we uploaded the files slightly later. [now fixed]
  • 26.10.2015: Please note that task 1c) of sheet 1 has slightly changed.
  • 21.10.2015: The exercise class will be taking place on Wednesdays in the seminar room of i2, that is room 4201b in E1.
  • 19.10.2015: [Important] Due to collisions with other courses, the time and place of Tuesday’s lectures has permanently shifted to 14.15 at 9U10 (in the basement of building E3).
  • 08.09.2015: We are online.

Schedule

Type Day Time Room Start Lecturer
Lecture Tue 14:15 – 15:45h 9U10 (E3) Oct 27 Katoen
Wed 10:15 – 11:45h 5052 Oct 21 Katoen
Exercise Wed 14:15 – 15:45h Seminar Room i2 (4201b) Oct 28 Dehnert  / Junges

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 algorithmical manner, whether such models satisfy basic properties, such as reachability probabilities?
  3. Can we make these models smaller to enable or simplify 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 recent paper called “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, interactive Markov chains, model checking, probabilistic temporal logic (CTL and LTL), bisimulation, compositional modeling, concurrency, compositional minimisation.

Slides

No. Date Subject Slides
1 Oct 21  Probability Theory Refresher  slides_mvps2015_lecture1.pdf
2 Oct 27  Markov Chains  slides_mvps2015_lecture2.pdf
3 Oct 28  Reachability Probabilities  slides_mvps2015_lecture3.pdf
4 Nov 3  Almost-Sure Properties  slides_mvps2015_lecture4.pdf
5 Nov 4  Verifying Probabilistic LTL  slides_mvps2015_lecture5.pdf
6 Nov 10  PCTL Model Checking  slides_mvps2015_lecture6.pdf
7 Nov 11  Qualitative PCTL  slides_mvps2015_lecture7.pdf
8+9 Nov 17+18  Probabilistic Bisimulation  slides_mvps2015_lecture8.pdf
10 Nov 24  Markov Decision Processes  slides_mvps2015_lecture10.pdf
11 Nov 25  Reachability Probabilities in MDPs  slides_mvps2015_lecture11.pdf
12 Dec 2  PCTL Model Checking on MDPs  slides_mvps2015_lecture12.pdf
13 Dec 8  Continuous-Time Markov Chains  slides_mvps2015_lecture13.pdf
14 Dec 9  Transient Analysis in CTMCs  slides_mvps2015_lecture14.pdf
15 Dec 15  Timed Reachability Probabilities  slides_mvps2015_lecture15.pdf
16 Dec 16  Timed PCTL Model Checking  slides_mvps2015_lecture16.pdf
17 Jan 13  Probabilistic Automata
18 Jan 19  Probabilistic Automata (continued)
19 Jan 26  Markov Automata
20 Jan 27  Markov Automata (continued)
21 Feb 9  Applications

Exercises

No. Due Exercise Solution
 1  Oct 28  ex01  sol01
 2  Nov 4  ex02  sol02
 3  Nov 11  ex03  sol03
 4  Nov 18  ex04  sol04
 5  Nov 25  ex05  sol05
 6  Dec 02  ex06  sol06
 7  Dec 09  ex07  sol07
 8  Dec 16  ex08  sol08
 9  Jan 13  ex09  sol09
10 Jan 27  ex10  sol10
11 Feb 4

Exam

The exam will be in the form of an oral exam. For the oral exam, you will be given one hour of silent work to prepare solutions for two tasks. Afterwards you are to present your solutions and you will be asked a few additional questions. The dates for the exams will be announced in time on this website.

Further information

  • The course will be entirely given in English.
  • There are no lecture notes (yet); the course material will consist of slides.
  • The exam will be awarded with 6 ECTS credits. Details will follow later.

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.
  • 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