Advanced Model Checking
Graduate course - Summer Term 12
Lehrstuhl für Informatik 2
Schedule
Type | Time | Place | Start | Lecturer |
V4 | Mo 13:30 - 15:00 | AH I | 16.04.2012 | |
Tue 8:15 - 9:45 | 5054 | 03.04.2012 | ||
Ü2 | Wed 13:30 - 15:00 | 5054 | 18.04.2012 |
Correction
- 03.07 : In light of recent remonstrance, I have included some correction to the exercise sheet.
- 19.06 : I found an error in the question 2 of exercise sheet 8. I'll remedy it in the exercise class. Sorry for the inconvenience.
- 21.05 : Today (21.05.12) the lecture will take place in the seminar room of I2.
- 03.04 : The first exercise sheet will be issued on 11.04. The first exercise hour takes place on 18.04. Please hand in your solutions on 18.04, before the exercise hour begins.
- 04.04 : Change of lecture hall! From today on, the Tuesday lectures in AHII will take place in Room 5054. The lecture time keeps as before, i.e. from 8:15 to 9:45.
- 04.04 : Change of exercise hall! From today on, the exercise class in AHIII will take place in Room 5054. The time of exercise class keeps as before, i.e. from 13:30 to 15:00.
- 17.04 : Cancel of exercise hour! There is no exercise class on 02.05.
- 24.04 : There is no lecture on Monday, the 30.04.
- 07.05 : Tomorrow's lecture (08.05) will take place as usual (room 5054, 8:15--9:45).
- 09.05 : There is an additional lecture on 15.05 (Tuesday), at 4. pm, in the seminar room of i2 (room 4201b).
Exam
Information regarding the exam:
- All students who want to participate in the exam should
register via the CAMPUS system. - The exam takes place on August 10, 9:00-12:00
Motivation and background
This course is concerned with model checking, an automated technique to verify properties of hardware and software systems. Whereas the focus of the course Model Checking is on the elementary techniques of model checking, this course is focused on two main topics: advancing current model-checking technology, and, on the other hand, model-checking techniques for quantitative system aspects.
More concretely, the course will -–after a summary of the main model-checking techniques for LTL and CTL-– treat state space reduction techniques. This ranges from algorithms to minimise state-space representations using equivalences and pre-orders (bisimulations and simulation relations), techniques to avoid representing all possible interleaving of concurrent components (partial-order reduction) and data structures for the succinct representation of state spaces (e.g., binary decision diagrams).
In the second part of the course, models and algorithms are treated for the verification of timed properties, such as ``is it possible that the system will crash within 30 seconds'', and properties that involve random phenomena (e.g., ``the probability to reach a bad state within 44 minutes is below 0.0001''). Models such as timed automata, their infinite-state semantics, and finite abstractions thereof will be treated. This is complemented by a treatment of algorithms for checking timed CTL. This results in an effective framework that is used for checking real-time properties of embedded systems, communication protocols, and so on.
Probabilistic models are the key to model random phenomena as they occur in distributed algorithms that use randomisation to break the symmetry between processes, or to reason about quality of service parameters such as dependability, performance, and survivability. This course will deal with the basic algorithms and logics for verifying properties of fully probabilistic models such as Markov chains, and (if time permits) models that also exhibit nondeterminism (Markov decision processes).
More concretely, the course will -–after a summary of the main model-checking techniques for LTL and CTL-– treat state space reduction techniques. This ranges from algorithms to minimise state-space representations using equivalences and pre-orders (bisimulations and simulation relations), techniques to avoid representing all possible interleaving of concurrent components (partial-order reduction) and data structures for the succinct representation of state spaces (e.g., binary decision diagrams).
In the second part of the course, models and algorithms are treated for the verification of timed properties, such as ``is it possible that the system will crash within 30 seconds'', and properties that involve random phenomena (e.g., ``the probability to reach a bad state within 44 minutes is below 0.0001''). Models such as timed automata, their infinite-state semantics, and finite abstractions thereof will be treated. This is complemented by a treatment of algorithms for checking timed CTL. This results in an effective framework that is used for checking real-time properties of embedded systems, communication protocols, and so on.
Probabilistic models are the key to model random phenomena as they occur in distributed algorithms that use randomisation to break the symmetry between processes, or to reason about quality of service parameters such as dependability, performance, and survivability. This course will deal with the basic algorithms and logics for verifying properties of fully probabilistic models such as Markov chains, and (if time permits) models that also exhibit nondeterminism (Markov decision processes).
The lecture will be given in English.
All course material (i.e., lecture notes and slides) will be in English.
All course material (i.e., lecture notes and slides) will be in English.
Contents
- Summary of LTL and CTL model checking
- Equivalences and abstraction
- Partial-order reduction techniques
- Binary decision diagrams
- Timed automata
- Model checking timed CTL
Prerequisites
Basic knowledge of automata theory, complexity theory, and data structures and algorithms. The course is a follow-up course of Model Checking. It is highly recommended to have basic knowledge of model checking, although this is not mandatory.
ECTS Credits
The student will be awarded 6 ECTS credits for the lecture after passing the final exam.
Exercises
- Exercises can be worked on in groups of at most two students.
- To achieve a certificate to this course or to be admitted to the final exam, at least half of the exercises has to be reasonably dealt.
- The exercise sheets will be issued weekly.
Lecture Slides
All slides and exercise sheets will be made available here.
Date | Lecture | Subject | Slides | Exercise Sheet | Solution | |
|---|---|---|---|---|---|---|
03.04 | 1 | Introduction |   | |||
10.04 | 2 | Bisimulation vs. CTL* Equivalence |  |  | ||
16.04 | 3 | Bisimulation Quotienting |  | |||
17.04 | 4 | Stutter Trace and Bisimulation |  |  | ||
24.04 | 5 | Divergence Sensitivity |  |  | ||
08.05 | 6 | Stutter Bisimulation Quotienting |  |  | ||
14.05 | 7 | Simulation Relations & CTL* |   | |||
15.05 | 8 | Computing Simulations |  | |||
15.05 | 9 | Partial Order Reduction (1) |  |  | ||
21.05 | 10 | Ample Sets |  | |||
22.05 | 11 | POR for CTL |  |  | ||
04.06 | 12 | Reduced OBDD |  | |||
05.06 | 13 | continue... |  |  | ||
11.06 | 14 | Timed Automata |  | |||
12.06 | 15 | Time Divergence, Timelock and Zenoness | | | ||
25.06 | 16 | Timed CTL Model Checking | | | ||
26.06 | 17 | Zone Based Reachability | | |||
02.07 | 18 | Difference Bound Matrices | | | ||
03.07 | 19 |
Literature
| |
 |
The course is based on the recently published book:
Principles of Model Checking
by Christel Baier and Joost-Pieter Katoen.
by Christel Baier and Joost-Pieter Katoen.
An errata document to the book may be found here. The errata document will change during the semester.
It is possible to buy a book (about 40 euros), but there is no need to do so as there are various copies of the book available at the CS library.
Additional literature can be found in:
- J. Rutten, M. Kwiatkowska, G. Norman and D. Parker: Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, Volume 23 of CRM Monograph Series. American Mathematical Society, P. Panangaden and F. van Breugel (eds.), March 2004.
- M. Huth and M.D. Ryan: Logic in Computer Science -- Modelling and Reasoning about Systems, Cambridge University Press, 2nd edition, 2004
- K. Schneider: Verification of Reactive Systems, Springer-Verlag, Texts in Theoretical Computer Science. An EATCS Series, 2004
- J.-P. Katoen: Concepts, Algorithms and Tools for Model Checking, Erlangen: Institut für Mathematische Maschinen und Datenverarbeitung, 1999
- E.M. Clarke, O. Grumberg, D.A. Peled: Model Checking, MIT Press, 1999
- K.L. McMillan: Symbolic Model Checking, Kluwer Academic, 1993
Links
- PRISM model checker WebPage
- MRMC model checker WebPage
- Uppaal model checker WebPage
- Infostudium.de
- meinprof.de
