![]() |
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 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! ![]() ![]() Instructors ![]()
![]() Assistants ![]()
![]() Credits ![]()
![]() Syllabus (tentative) ![]()
![]() Textbook ![]() Principles of Model Checking. Christel Baier and Joost-Pieter Katoen, MIT Press, 2008. ![]() |
||||||||||
Dependable Systems & Software Group | Department of Computer Science | Universität des Saarlandes |