Quantitative Model Checking

Quantitative Model Checking

Audience

This advanced course addresses Bachelor and Master students in Computer Science, Embedded Systems, or Bioinformatics. 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 in computerized systems. Such systems include networked, embedded, or biological systems. Their underlying semantics are usually Markov chains, possibly extended with nondeterminism, or hybrid automata. 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?

We so far assume classical on-campus teaching, but we will observe the situation. Video recordings of lectures will be made available. 

• Lectures: each Monday 10:00 - 12:00 in HS 001 of E1 3,
• Tutorials (sometimes Lectures): each Wednesday 14:00 - 16:00 in HS 001 of E1 3.

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 MDP
• Hybrid Systems and Hybrid Automata
• Switching Systems
• Stability and Reachability in Hybrid and Switching Systems
• Numerical Simulation

Textbooks

• Principles of Model Checking. Christel Baier and Joost-Pieter Katoen, MIT Press, 2008 (also available from the library)
• Lecture notes on Hybrid Systems. John Lygeros, 2004 (available online).