Quantitative Model Checking

Quantitative Model Checking

Audience

This advanced course addresses Bachelor and Master students in Computer Science, Embedded Systems, or similar. Earlier participation in the module Verification or Embedded Systems are of advantage but not mandatory.

Objectives

Quantitative model checking is concerned with quantities (time, probability, temperature, pressure, concentration of NOx) changing dynamically as a consequence of the use of computerized systems.Such systems encompass space network, embedded systems, or biomedical contexts. Their underlying semantics are usually rooted in discrete-time and/or continuous-time Markov chains, possibly extended with nondeterminism. On the respective models, quantitative properties of interest can be verified.This course aims at covering both the model construction and the verification techniques for these systems.

Credits: 6 ECTS points -- 2 hours (or more) of lecture per week, 2 hours (or less) of tutorials per week, and some exercising

When and where?

• Lectures: TBD - once per week
• Tutorials (sometimes Lectures): TBD - once per week

Examination

The examination dates will be announced in due course.

Syllabus (tentative)

• Model Checking
• Probability Theory, Stochastic Processes
• Markov Chains in Discrete and Continuous Time
• Model Checking Markov Chains
• Non-Determinism and Markov Decision Processes (MDP)
• Model Checking Markov Decision Processes
• From Discrete to Continuous Time
• Model Checking Markov Chains in Continuous Time
• Composition and Closure Properties

Textbooks

• Principles of Model Checking. Christel Baier and Joost-Pieter Katoen, MIT Press, 2008