News

  • (new) 13.05.2011 Fixed a typo on sheet 5, exercise 2.
  • 10.05.2011 Seven students participated in the poll. None of the offered 16 timeslots fits all. There is a tie between the current timeslot and an alternative. We therefore stick to the current time slot (Wed, 13:30) since it was announced early before the semester and a change would (according to the poll) not increase the number of participants.
  • 04.05.2011 Currently our exercise class overlaps with other classes. To find out if we can shift it, please  go to doodle.com/7p2ubv64q6dguir6 and indicate *ALL* time slots that suit your schedule.
  • 14.03.2011: The first lecture will take place on Monday 11th April.


Schedule

Type

Day

Time

Place

Start

Lecturer

V3

Mon

12:30-14:00

2350|314.1 (AH III)

April 11

Katoen

Tue

8:15-9:45

2350|111 (AH II)

Katoen

Ü2

Wed

13:30-15:00

2350|314.1 (AH III)

April 20

Sher, Gretz


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 "Performance Evaluation and Model Checking Join Forces" in the popular journal Communications of the ACM (2010).


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.


Contents

No.

Date

Topic

Handout

Exercises

1

11 April

Probability Theory Refresher

2

12 April

Discrete Time Markov Chains

until April 20

3

18 April

Reachability Probabilities


until April 27

4

26 April

Qualitative Properties


until May 4

5

2 May

Probabilistic Computation Tree Logic

6

3 May

PCTL Expressiveness


until May 11

7

9 May

Probabilistic Bisimulation

until May 18

8

16 May

Equivalence Proof

on the blackboard

9

17 May

Verifying Linear-Time Properties

until May 25

10

23 May

Markov Decision Processes

until June 1

11

30 May

(11+12) Reachability Probabilities in MDPs

12

31 May

continue....


 until June 8

13

6 June

Model Checking MDPs


until June 22

14

20 June

Continuous-Time Markov Chains

until June 29

15

27 June

Transient Analysis of CTMCs

16

28 June

Timed Reachability in CTMCs

until July 6

17

4 July

Continuous Stochastic Logic

until July 13

18

11 July

Probabilistic Automata (PA)

19

12 July

Interactive Markov Chains (IMC)


Prerequisites

Basic knowledge of the relevant undergraduate courses of the first two years (Vordiplom/Bachelor) is required:

  • Introduction to Model Checking
  • Automata Theory
  • Discrete Mathematics
  • Probability Theory


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.