News
21.06.2017

Clarification Practical Exercise Sheet 2Dear all, in the second practical exercise sheet, you are asked to compute the probabilities that the blue player wins. In one exercise, you are asked to compute this reachability probability within a given step bound, in the other exercise without a step bound.... Read more Dear all, in the second practical exercise sheet, you are asked to compute the probabilities that the blue player wins. In one exercise, you are asked to compute this reachability probability within a given step bound, in the other exercise without a step bound. Now, for the unbounded case, there are two possible interpretations: either "(F bluewins)" or "((not redwins) U bluewins)", and accordingly with a step bounds. For both the bounded and unbounded case, please use the second interpretation. That is, only paths in which the blue player wins before the red player wins should be taken into account. Hahn and Hashemi 
21.06.2017

Theoretical Exercise 5Dear all, results of the 5th theoretical assignment is online now. Thanks, Hahn and Hashemi 
19.06.2017

Practical Exercise Sheet 2Dear students, for the second practical exercise sheet, there is the issue that the size of the state space is too large to be explicitly generated in reasonable time and space. Therefore, you are allowed to use a configuration with the same number of places... Read more Dear students, for the second practical exercise sheet, there is the issue that the size of the state space is too large to be explicitly generated in reasonable time and space. Therefore, you are allowed to use a configuration with the same number of places and pieces as in the first practical exercise. Hahn and Hashemi 
02.05.2017

Final written exam scheduleDear students of QMC 2017, Your final exam is scheduled on Friday, August 4 (14:0016:00). If this timing does not work out for you, please send us an email not later than 8:30 am Monday, 8 May (before the lecture). Thanks, Hahn &... Read more Dear students of QMC 2017, Your final exam is scheduled on Friday, August 4 (14:0016:00). If this timing does not work out for you, please send us an email not later than 8:30 am Monday, 8 May (before the lecture). Thanks, Hahn & 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