News
Practical AssignmentsWritten on 28.05.25 by Holger Hermanns We have graded the first practical assignment sheet and uploaded our feedback. To streamline the work on the second practical assignment sheet, we offer you the option to resort to sample solutions to exercises P1.1 and P1.2. You find them in the dCMS under Materials now. This might come in handy… Read more We have graded the first practical assignment sheet and uploaded our feedback. To streamline the work on the second practical assignment sheet, we offer you the option to resort to sample solutions to exercises P1.1 and P1.2. You find them in the dCMS under Materials now. This might come in handy in case your own solution had major flaws or was incomplete. Note that PCTL formulas correctly solving what was asked for in P1.2 can differ significantly from those appearing in the sample solution, depending on the exact modeling (e.g. how many steps were used to model a round in the game etc.). |
Office Hours next weekWritten on 23.05.25 by Holger Hermanns Next week will feature no lecture (again) due to Thursday being a public holiday. Instead, we are (again) arranging office hours for the discussion of lecture contents. Meet Gabriel (i) on Monday, May 26, 2 pm to 4 pm, and/or (ii) on Wednesday, May 28, 2 pm to 4 pm in room 533 of E1 3. Besides, you… Read more Next week will feature no lecture (again) due to Thursday being a public holiday. Instead, we are (again) arranging office hours for the discussion of lecture contents. Meet Gabriel (i) on Monday, May 26, 2 pm to 4 pm, and/or (ii) on Wednesday, May 28, 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. |
Material, office hours, and PrismWritten 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.) 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.) 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. |
Material and first assignment availableWritten 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 availableWritten 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