News
 Due to illness, the lecture on Wednesday January 18 does not take place.
 Note that there is no exercise class in the week of January 914, 2017.
 The kickoff lecture takes place on Tuesday October 18, 2016.
Schedule
Type  Day  Time  Hall  Start  Lecturer 
Lecture  Tue  14:15 – 15:45  9U10  18.10  Katoen 
Wed  10:15 – 11:45  5052  19.10  Katoen  
Exercise  Wed  14:15 – 15:45  4201b  26.10  Quatmann, Volk 
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 particular realtime aspects.
More concretely, the course will –after a summary of the main modelchecking techniques for LTL and CTL– treat state space reduction techniques. This ranges from algorithms to minimise statespace representations using equivalences and preorders (bisimulation and simulation relations), techniques to avoid representing all possible interleaving of concurrent components (partialorder 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”. The model of timed automata, their infinitestate semantics, and finite abstractions thereof will be treated. This is complemented by a treatment of algorithms for checking timed reachability properties. This results in an effective framework that is used for checking realtime properties of embedded systems, communication protocols, robotics, and so on.
Contents
 Different notions of bisimulation and their minimization algorithms
 Simulation preorders, and checking simulation preorders
 Partialorder reduction techniques
 Symbolic model checking using binary decision diagrams
 Other symbolic modelchecking techniques
 Timed automata
 Timed reachability
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, starting from October 19, 2017.
Slides
No.  Date  Subject  Slides  Exercise 

1  18.10  Introduction  amc16_orga amc16_lecture1 

2  19.10  CTL* and Bisimulation  amc16_lecture2  ex01 
3  25.10  Bisimulation Quotienting  amc16_lecture3  
4  26.10  Stutter Bisimulation  amc16_lecture46  ex02 
5  02.11  Divergence Sensitivity  ex03  
6  08.11  Stutter Bisimulation Quotienting  amc16_lecture6  ex04 
7  16.11  Simulation and Universal CTL*  amc16_lecture7  
8  23.11  Simulation Quotienting  amc16_lecture8  ex05 
9  29.11  Ample Set Conditions  amc16_lecture9  
10  30.11  PartialOrder Reduction (1)  amc16_lecture10  ex06 
11  06.12  PartialOrder Reduction (2)  amc16_lecture11  ex07 
12  13.12  Reduced Ordered Binary Decision Diagrams  
13  14.12  Symbolic Model Checking with ROBDDs  amc16_lecture13  ex08 
14  10.01  Bounded Model Checking 
See also sections 3+4 in: bmc_material 

15  11.01  Bounded Model Checking  ex09  
16  17.01  Timed Automata  amc16_lecture16  ex10 
17  31.01  Time Divergence, Timelock, and Zenoness  amc16_lecture17  
18  01.02  Decidability of Timed Reachability  amc16_lecture18 number_of_regions  ex11 
19  07.02  ZoneBased Reachability and Difference Bound Matrices  amc16_lecture19 amc16_lecture20 
Exam
TBA
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, in particular Chapters 6.7, 7, 8 and 9 and additional material on timed automata not covered in the book. It is possible to buy a book (about 38 euros), but there is no real need to do so as there are various copies of the book available at the CS library.
Additional literature can be found in:
 M. Huth and M.D. Ryan: Logic in Computer Science — Modelling and Reasoning about Systems, Cambridge University Press, 2nd edition, 2004.
 E.M. Clarke, O. Grumberg, D.A. Peled: Model Checking, MIT Press, 1999.
 K.L. McMillan: Symbolic Model Checking, Kluwer Academic, 1993.
Links
 Errata for Principles of Model Checking