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.



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


Dates and Locations

The course spans the winter term 2014/15.


The lectures take place on Tuesdays, 10-12 in seminar room 016 in building E1 3.


Further details are available at the dCMS.

Please login into the dCMS to get more information!


Dr. Jan Krčál


Hassan Hatefi, MSc.
Vahid Hashemi, MSc.


6 ECTS points

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)


Principles of Model Checking. Christel Baier and Joost-Pieter Katoen, MIT Press, 2008.