Lecture: Quantitative Model Checking (QMC) – SS12

Leave a comment Go to comments

Lecturer: David Spieler
Assistant: Aleksandr Andreychenko

Responsible Professor: Prof. Verena Wolf

Start: 23. April 2012

Schedule: Monday 8:30 – 10.00 a.m., E1 3 room 528

Exercises: Friday 2:15-15:45 p.m., E1 3 room 328

Credits: 6 ECTS points (Advanced course)

Description:
Quatitative model checking is an approach for verifying systems exhibiting random phenomena. Such systems include networked, embedded, and more recently biological systems. They have usually discrete-time and/or continuous-time Markov chains, together with their extensions with nondeterminism, as their underlying semantics. With quatitative model checking techniques, properties of interest can be verified against the respective models. The properties can be specified by logics like PCTL, LTL, and PCTL* for discrete-time models, and CSL for continuous-time models. This course aims to cover both the model construction and the verification techniques for these systems.

Prerequisites:
The course is open to all students who have basic knowledge of verification, linear algebra, numerics and logics. Successful completion of the core lecture “Verification” and/or the basic course “Nebenläufige Programmierung“ and/or being familiar with the first seven chapters of the book “Principles of Model Checking” (C. Baier, J.-P. Katoen) is an advantage. Further we will use Java 6 for the practical assignments.

Certification conditions:
There will be a written exam at the end of the course as well as one re-exam which can be taken when the ordinary exam has not been passed. Depending on the number of participants the re-exam might be oral. In order to pass the course, one of the two exams has to be graded 4.0 or better. In order to be allowed to take part in the exams, the students must have achieved at least 50% of the accumulated points of the theoretical as well as of practical exercise sheets. There might be a bonus on the grade for extraordinary achievements in the exercises (to be discussed in the first lecture).

Please register at the HISPOS system in order to comply to examination regulations.

Exam schedule:
The exam is scheduled on the 30th of July, 8:30-10:00 in E 1 3 room 528. It will cover all lectures as well as the material discussed in the exercise groups.

Syllabus:

  • Model Checking
  • Probability Theory
  • Stochastic Processes
  • Discrete-Time Markov Chains (DTMC)
  • Transient, Steady State and Reachability Analysis for DTMC
  • Probabilistic Computation Tree Logic (PCTL)
  • Probabilistic Bisimulation (DTMC)
  • Continuous-time Markov Chains (CTMC)
  • Transient and Steady State Analysis for CTMC
  • Continuous Stochastic Logic (CSL)
  • Probabilistic Bisimulation (CTMC)
  • Rewards
  • Non-Determinism and Markov Decision Processes
  • Markov Population Models (MPM) and Transition Classes (TC)
  • Transient and Steady State Analysis for Infinite State MPM induced by TC
  • Application of MPM in Systems Biology
  • Parameter Estimation for MPM

Lecture Slides:

Exercise Sheets:
Please hand in your solutions to the theoretical exercise sheets at the beginning of the next lecture and send your solutions of the practical exercise sheets including the whole framework + your implementations as <YourLastName><SheetNumber>.tgz, e.g. Spieler03.tgz, to Sascha (s9sazick |at| stud.uni-saarland.de).

Textbooks:

  • Principles of Model Checking. Christel Baier and Joost-Pieter Katoen, MIT Press, 2008. (Amazon link)
  1. No comments yet.
  1. No trackbacks yet.
You must be logged in to post a comment.