Quantitative Model Checking Holger Hermanns, Martina Maggio



Delayed start on May 4.

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