News
Final written examWritten on 02.05.17 (last change on 31.07.17) by Vahid Hashemi Dear students of QMC 2017, Your final exam is scheduled on Friday, August 4 (13:30-16:30). For the exam, we allow you to use a cheat sheet. Carefully read the following: the cheat sheet must be a single DIN A4 paper. It may only be written on one side. Also, it must be hand-written, not… Read more Dear students of QMC 2017, Your final exam is scheduled on Friday, August 4 (13:30-16:30). For the exam, we allow you to use a cheat sheet. Carefully read the following: the cheat sheet must be a single DIN A4 paper. It may only be written on one side. Also, it must be hand-written, not printed. Also, you have to show us the cheat sheet before the exam. We will take a photo of each cheat sheet to ensure that indeed only one is used by each student. Thanks, Hahn & Hashemi
|
Quantitative Model Checking
Ernst Moritz Hahn (instructor)
Vahid Hashemi, Yuliya Butkova (assistants)
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 discrete-time and/or continuous-time 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 discrete-time models, and CSL for continuous-time 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
- Discrete-Time Markov Chains (DTMC)
- Probabilistic Computation Tree Logic (PCTL)
- Model Checking DTMC
- Probabilistic Bisimulation (DTMC)
- Continuous-time Markov Chains (CTMC)
- Continuous Stochastic Logic (CSL)
- Model Checking CTMC
- Probabilistic Bisimulation (CTMC)
- Logical Characterization
- Non-Determinism and Markov Decision Processes (MDP)
- Model Checking MDP
- Bisimulation and Logical Characterization (MDP)
Textbooks
- Principles of Model Checking. Christel Baier and Joost-Pieter Katoen, MIT Press, 2008 (also available from the library)
- First Look at Rigorous Probability Theory. Jeffrey S Rosenthal, World Scientific Publishing Company, 2006