Registration for this course is open until Thursday, 17.04.2025 23:59.

News

Currently, no news are available

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 networks, 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: Thu 12:01 - 13:30 in HS 001 of E1 3
  • Tutorials (sometimes Lectures): Thu 14:29 - 16:00 in HS 001 of E1 3

First lectures on April 10.

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

Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators