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.

If you would like to participate in this course, please register for it via the CMS. An explanation how to do that is here (requires Adobe Flash Player).

The course starts on April 14, 2010 and spans the summer term 2010.

Lectures take place each Wednesday at 08:30-10:00, in E1 3 - HS 1.

Tutorials timeslots are Fridays 12:30-14:00, starting April 23.

Further details are available at the CMS.

Prof. Dr.-Ing. Holger Hermanns

	David Spieler, Msc
	Moritz Hahn, Msc