Quantitative Model Checking Ernst Moritz Hahn

News

21.06.2017

Clarification Practical Exercise Sheet 2

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.... 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 5

Dear all,

results of the 5th theoretical assignment is online now.

Thanks,

Hahn and Hashemi

19.06.2017

Practical Exercise Sheet 2

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... 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 schedule

Dear students of QMC 2017,

Your final exam is scheduled on Friday, August 4 (14:00-16: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:00-16: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 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



If you encounter technical problems, please contact the administrators