News
Final grades available, re-exam informationWritten on 05.08.19 (last change on 05.08.19) by Daniel Stan Final GradesDear students, As stated in the title, the final grades of the exam have just been entered on the website. Despite the difficulty of the exam, all of you achieved more than 50 points hence passed the class, congratulations! Considering the (excessive) length of the examination, the… Read more Final GradesDear students, As stated in the title, the final grades of the exam have just been entered on the website. Despite the difficulty of the exam, all of you achieved more than 50 points hence passed the class, congratulations! Considering the (excessive) length of the examination, the grade scale has been revised to reflect this difficulty, namely achieving all exercises except the last one (14 points) already grants you a 1.0. Bonus was then added to the final grade according to the rule explained in Lecture 01, slide 19. Due to some request, the exam file and some sample solution are available in the material section, enjoy! InspectionI am available in my office E1 3, 532 everyday from 2pm to 4pm from Tuesday 06.08.2019 to Monday 12.08.2019 in order to let you check/inspect your exam. Shall you want to inspect your exam after this date, please send me an email to make sure I am around. Re-ExamI recall that a re-exam is scheduled on Monday 16.09.2019, 2pm. Due to the low number of students that may want to take part in it, we have decided to organize an oral examination instead. This oral (re)-examination will take place at the same place and date and will be evaluated by Prof. Hermanns and myself. Please register on LSF and this website at least one week before, if you want to retake this exam.
Shall we not meet each other again, I hope you enjoyed this class and wish you all the best, in particular great vacations! -- |
Examination detailsWritten on 24.07.19 by Daniel Stan Dear students, As a recall of last lecture, I remind you the examination of the lecture takes place next week from 2:30pm to 4:30pm (sharp) in HS 002. It is a written examination. Although the exam is closed-book, you are allowed to bring a hand-written cheat-sheet in A4 format, one-sided. Also,… Read more Dear students, As a recall of last lecture, I remind you the examination of the lecture takes place next week from 2:30pm to 4:30pm (sharp) in HS 002. It is a written examination. Although the exam is closed-book, you are allowed to bring a hand-written cheat-sheet in A4 format, one-sided. Also, don't forget to register on the system to take the exam, and bring an ID and immatriculation number. I can provide −per request− an office hour next Monday at 2pm, in case you need feedback about the assignments (or want to consult them).
Best regards, -- |
Exercise sheet 6 submission openWritten on 12.06.19 by Daniel Stan Dear students, It appears that the submission entry file for exercise sheet 6, due for today, was not available, it is now the case so you can now submit your solution.
I'm taking the opportunity of this message to notify that some previous exercise/tutorial sheets have been augmented with… Read more Dear students, It appears that the submission entry file for exercise sheet 6, due for today, was not available, it is now the case so you can now submit your solution.
I'm taking the opportunity of this message to notify that some previous exercise/tutorial sheets have been augmented with some sample solutions, sometimes handwritten. More are to come. Also, several new exercise grades and project feedbacks will be available by Friday!
Best regards, -- |
Quantitative Model Checking
Daniel STAN (instructor)
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 10, April 14:00 - 16:00, 2019 in the seminar room 528 in E1 3,
afterwards every Monday 14:00 - 16:00 in the seminar room 528 in E1 3, starting on April 15, 2019,
Tutorials: every Wednesday 14:00 - 16:00 in the seminar room 528 in E1 3, starting on April 17, 2019
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.
During the semester, starting from Tuesday 23rd, an exercise will be due each Tuesday. The exercise could be either practical or theoretical, The theoretical exercises will be released one week before while more time will be given for the practical exercises.
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