News

Starting from 22 April, the lectures on tuesdays will take place at 9.45AM in the seminar room of i2 (2nd floor of E1).
 Instead of having a written exam at the end of the course, we will organize oral examinations.
Schedule
Type  Day  Time  Hall  Start  Lecturer 

Lecture  Mon  12:15 – 13:45  AH 1  14 April  Katoen 
Tue  9:45 – 11:15  Seminar Room I2  15April  Katoen  
Exercise  Wed  13:30 – 15:00  Seminar Room I2  23 April  Dehnert / Sher 
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 modelchecking technology, and, on the other hand, modelchecking techniques for quantitative system aspects.
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 infinitestate 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 realtime 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).
Contents
 Summary of LTL and CTL model checking
 Equivalences and abstraction
 Partialorder reduction techniques
 Binary decision diagrams
 Timed automata
 Model checking timed CTL
Prerequisites
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.
Slides
No.  Date  Subject  Slides  Handout  Exercise  Solution 

1  14.4.14  Introduction  l1a+l1b  
2  15.4.14  CTL* and Bisimulation  l2  e1  s1  
3  22.4.14  Bisimulation Quotienting  l3  e2  s2  
4  28.4.14  Stutter Bisimulation  l4  e3  s3  
5  5.5.14  Divergence Sensitivity  l5  e4  s4  
6  12.5.14  Stutter Bisimulation Quotienting  l6  
7  13.5.14  Simulation Relations  l7  e5  s5  
8  19.5.14  Simulation and Universal CTL*  l8  
9  20.5.14  Simulation Quotienting  l9  e6  s6  
10  27.5.14  Ample Set Conditions  l10  e7  s7  
11  2.6.14 
PartialOrder Reduction (1) 
l11  
12  3.6.14  PartialOrder Reduction (2)  l12  e8  s8  
13  16.6.14 
Reduced Ordered Binary Decision Diagrams 
l13  e9  s9  
14  23.6.14 
Symbolic Model Checking with ROBDDs 
l14  e10  s10  
15  30.6.14 
Timed Automata 
l15  
16  1.7.14 
Verifying Timed Reachability Properties 
l16  e11  s11  
17  8.7.14 
Zonebased Reachability Analysis 
l17  
18  14.7.14 
Difference Bound Matrices 
l18 
Exam
 Exam: Monday August 25 and Friday September 26
Further information
 The lecture will be given in English. All course material (i.e., lecture notes and slides) will be in English.
 The students will be awarded 6 ECTS credits for the lecture after passing the final exam.
The course is based on the book: Principles of Model Checking by Christel Baier and JoostPieter Katoen. 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, SpringerVerlag, Texts in Theoretical Computer Science. An EATCS Series, 2004
 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