Oral Exam Registrations

Written on 19.08.22 by Holger Hermanns

Dear students of QMC,

The oral exams are scheduled to take place on August 30, August 31, and September 6. Detailled timing follows.

It should by now be possible to register for the examination in LSF/HISPOS. Please register there before August 23, 2022.

Thank you,
   H H

Delayed start on May 4.

Written on 03.05.22 (last change on 03.05.22) by Holger Hermanns

Dear students of QMC,

Due to a conflicting appointment, the start of tomorrow's lecture (May 4) is delayed to 2:40 pm, we then continue without break until 4 pm.

See you,
  Holger Hermanns

Quantitative Model Checking


This advanced course addresses Bachelor and Master students in Computer Science, Embedded Systems, or Bioinformatics. Earlier participation in the module Verification or Embedded Systems are of advantage but not mandatory.


Quantitative model checking is concerned with quantities (time, probability, temperature, pressure, concentration of NOx) changing dynamically in computerized systems. Such systems include networked, embedded, or biological systems. Their underlying semantics are usually Markov chains, possibly extended with nondeterminism, or hybrid automata. On the respective models, quantitative properties of interest can be verified. This course aims at covering both the model construction and the verification techniques for these systems.

Credits: 6 ECTS points -- 2 hours (or more) of lecture per week, 2 hours (or less) of tutorials per week, and some exercising

When and where?

We so far assume classical on-campus teaching, but we will observe the situation. Video recordings of lectures will be made available. 

  • Lectures: each Monday 10:00 - 12:00 in HS 001 of E1 3,
  • Tutorials (sometimes Lectures): each Wednesday 14:00 - 16:00 in HS 001 of E1 3.
First Lecture on Wednesday, 13 April 14:00 - 16:00 in HS 001 of E1 3.



The examination dates will be announced in due course.

Syllabus (tentative)

  • Model Checking
  • Probability Theory, Stochastic Processes
  • Markov Chains in Discrete and Continuous Time
  • Model Checking Markov Chains
  • Non-Determinism and Markov Decision Processes (MDP)
  • Model Checking MDP
  • Hybrid Systems and Hybrid Automata
  • Switching Systems
  • Stability and Reachability in Hybrid and Switching Systems
  • Numerical Simulation


Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators