QUANTITATIVE MODEL CHECKING

Audience

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.

 


Objectives

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.

 


Registration

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


Dates and Venue

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.


Instructor

Prof. Dr.-Ing. Holger Hermanns

Assistants

David Spieler, Msc
Moritz Hahn, Msc