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.
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. Instructors
Assistant
Credits
Exam 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)
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 |