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 an approach for verifying systems exibihting random phenomena. Such systems include networked, embedded, and more recently biological systems. They have usually discrete-time and/or continuous-time Markov chains, together with their extensions with nondeterminism, as their underlying semantics. With quatitative model checking technique properties of interest can be verified against the respective models. The properties can be specified by PCTL, LTL, PCTL* 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 2013/14.


The first meeting will take place in 401, E 1.3 on 17/10/2013, Thursday, 4PM-5:30PM.


The second lecture at 2PM-4PM, Tuesday, Oct 22, 2013 will take place in E2.5 SR 4 (U.16).


All remaining lectures will take place in 528, E1.3, Tuesday, 2PM-4PM.


Tutorials will take place in 528, E1.3, Tuesday, 10AM-12PM.

For those who cannot make it, you can find us in 534, E1.3, Monday, 10AM-12PM.


Dr. Lei Song


MSc. Hassan Hatefi


6 ECTS points


Final written Exam will take place in E1.3, 528, on Tue, February 18, 2014, 2pm 4pm (90min).

In order to participate the final exam, you need to get at least 50% points for both theoretical and practical exercises. You can ask Hassan for your latest 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.