Advanced Model Checking

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 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).

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.

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

Partial-Order Reduction (1)

 l11
12 3.6.14 Partial-Order 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

Zone-based 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.
Literature

The course is based on the book: Principles of Model Checking by Christel Baier and Joost-Pieter 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, Springer-Verlag, 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