News
26.04.2017

Theoretical Exercise 1Dear students, The results of the first theoretical assignment is online now. Thanks, Hahn & Hashemi 
24.04.2017

Theoretical Exercise 2Dear students, The theoretical Exercise 2 is online now. Please note that for both hard and soft copy submissions, the deadline is firm and before the next lecture on 8.05.2017. Thanks, Hahn &... Read more Dear students, The theoretical Exercise 2 is online now. Please note that for both hard and soft copy submissions, the deadline is firm and before the next lecture on 8.05.2017. Thanks, Hahn & Hashemi

24.04.2017

Room changesDear students, from now on, the lecture will take place Mondays 810 in E 1 3 room 528 and the tutorials will take place on Wednesdays 1416 in E 1 3 room 328. Note that this already affects the tutorial the day after tomorrow. Thanks, Hahn & Hashemi 
21.04.2017

QMC lecture: Mondays 810 amDear students, due to the result of Doodle, it seems that the only time slot which is possible for almost all of you is Monday 810 am. Therefore, we follow the current schedule for the lectures. Thanks, Hahn & Hashemi

19.04.2017

Theoretical Exercise 1Dear students, the first theoretical assignment is online now. The due date for the assignment is Monday 24th April before the lecture. You can submit your solutions electronically via dCMS or hand them in before the lecture. Best regards, Vahid ... Read more Dear students, the first theoretical assignment is online now. The due date for the assignment is Monday 24th April before the lecture. You can submit your solutions electronically via dCMS or hand them in before the lecture. Best regards, Vahid

19.04.2017

Alternative time slots for the QMC lectureDear students of QMC 2017, Due to some requests, we have provided some extra time slots for the QMC lecture. Unless you are fine with the current timing, i.e., Mondays 810, you can vote for the other time slot(s) which best suits you. In case of a consensus,... Read more Dear students of QMC 2017, Due to some requests, we have provided some extra time slots for the QMC lecture. Unless you are fine with the current timing, i.e., Mondays 810, you can vote for the other time slot(s) which best suits you. In case of a consensus, we will change the timing. You can participate in the Doodle at http://doodle.com/poll/r8em2tsec476b7qe. Thanks, Ernst Moritz Hahn and Vahid Hashemi

Quantitative Model Checking
Ernst Moritz Hahn (instructor)
Vahid Hashemi (assistant)
Audience
This advanced course addresses Bachelor and Master students in Computer Science, Bioinformatics, CuK or Computerlinguistics. Background in probability theory and the module Verification are of advantage but not mandatory.
Objectives
Quantitative model checking is concerned with quantities (mostly probabilities) within systems exhibiting random behaviour. Such systems include networked, embedded, or biological systems. Their underlying semantics are usually discretetime and/or continuoustime Markov chains, possibly extended with nondeterminism. On the respective models, quantitative properties of interest can be verified. The properties can be specified, e.g., by PCTL or LTL for discretetime models, and CSL for continuoustime models. This course aims to cover both the model construction and the verification techniques for these systems.
Credits: 6 ECTS points (2 hours of lecture, 2 hours of tutorials, and some exercises every week)
When and where?
Lectures: first lecture on Wednesday 14  16, April 19, 2017 in the seminar room U12 in E1 1,
afterwards every Monday 8  10 in the seminar room 528 in E1 3 (note the room change), starting on April 24, 2017,
Tutorials: every Wednesday 14  16 in the seminar room 328 in E1 3 (note the room change), starting on April 26, 2017
Grading
The dates for the exams will be announced.
Having at least 50% points for both theoretical and practical exercises is required for admission to the final exam. Your current point status will be made available in dCMS.
Syllabus (tentative)
 Model Checking
 Probability Theory
 Stochastic Processes
 DiscreteTime Markov Chains (DTMC)
 Probabilistic Computation Tree Logic (PCTL)
 Model Checking DTMC
 Probabilistic Bisimulation (DTMC)
 Continuoustime Markov Chains (CTMC)
 Continuous Stochastic Logic (CSL)
 Model Checking CTMC
 Probabilistic Bisimulation (CTMC)
 Logical Characterization
 NonDeterminism and Markov Decision Processes (MDP)
 Model Checking MDP
 Bisimulation and Logical Characterization (MDP)
Textbooks
 Principles of Model Checking. Christel Baier and JoostPieter Katoen, MIT Press, 2008 (also available from the library)
 First Look at Rigorous Probability Theory. Jeffrey S Rosenthal, World Scientific Publishing Company, 2006