Main Page

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

News

Material, office hours, and Prism

Written on 25.04.25 (last change on 26.04.25) by Holger Hermanns

The material of this week is available in dCMS since yesterday, including tutorial sheet and a second assignment. (We will stop announcing material availabilty from now on.)

Next week will feature no lecture due to Thursday being a public holiday. Instead, we are arranging office hours for the discussion of lecture contents. Meet Gabriel (i) on Tuesday, April 29, 2 pm to 4 pm, and/or (ii) on Friday, May 2, 2 pm to 4 pm in room 533 of E1 3. Besides, you are free to write emails to dengler@depend.uni-saarland.de anytime.

We will soon start with hands-on work using the probabilistic model checker PRISM. It is recommended to get it installed from https://www.prismmodelchecker.org/download.php, and you are invited to play around with it, e.g. by following the tutorial in https://www.prismmodelchecker.org/tutorial/die.php, but this is not essential for the tasks currently in focus.

HeHo

Material and first assignment available

Written on 17.04.25 by Holger Hermanns

The material of today's lecture is available in dCMS now. We also released the first theoretical assignment sheet, worth 20 points. Submission is due on May 8. Have a good Easter break, HeHo

Material available

Written on 10.04.25 by Holger Hermanns

The material of today's first lectures is now available in dCMS, also including a first tutorial sheet for you to chew on. Next week Thursday we first have a tutorial (taking up that tutorial sheet), then a lecture. Early next week we are populating the calender. Sorry for delay in this matter. HeHo

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

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