QUANTITATIVE MODEL CHECKING

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.

The course spans the period 24. Augst -- 18 September, 2009.

Lectures and tutorials take place on Aug. 24 -- 27, Aug. 31 -- Sep. 3, and Sep. 7--10.

On these days lectures are generally from 09:15 to 11:00. Tutorials start 14:15 and run until about 15:30. The lectures will take place in E1 3 - HS III.

Further details are available at the CMS.

Dr. Lijun Zhang

Moritz Hahn, Msc