### News

- 05.09.2016: The
**second exam**is going to take place at**10.15AM (sharp) in AH4**. Please**be there**around**10AM**, so we can get started on schedule. - 30.07.2016: The inspection of the exam is going to take place on Tuesday, 2 August, at 1PM in our seminar room.
- 11.07.2016: The complexity of LTL model checking of formula F with fairness assumption fair is O(|T|.exp(|F|+|fair|)) by checking the LTL formula fair –> F using the standard nested DFS algorithm. It is also possible to adapt the nested DFS algorithm to directly deal with fair (using SCC analysis), avoiding the exponential blow-up. This yields a complexity of O(|T|.exp(|F|).|fair|), as indicated in the slides of lecture 21.
- 30.06.16: Next week, there will be a lecture on Friday July 8.
- 19.06.16: Since some of the given formulae were ambiguous in the absence of operator precedence rules, we have added some parentheses.
- 15.06.16: Fixed two typos on exercise sheet 7.
- 07.06.16: note that a lecture takes place on June 8 at the regular exercise class time (and place); the exercise class takes place instead at the lecture time (and place) on Friday June 10.
- 01.06.16: The sixth exercise sheet is available.
- 26.05.16: Slightly fixed sheet 5: new distribution of points and fixed incomplete task description in 4c).
- 25.05.16: The fifth exercise sheet is available.
- 13.05.16. The fourth exercise sheet is available.
- 08.05.16: You can
**register for the exam**until 20/05. We would advise you to do so as soon as possible! - 06.05.16: We made a fix in exercise one, the value alternates between zero and
*one***!** - 04.05.16: The third exercise sheet is available.
- 01.05.16: We made the formulation of the last task of sheet 2 a bit more precise.
- 27.04.16: The second exercise sheet is available.
- 24.04.16: The survey regarding the time slot for the tutorial is over. Most of you prefer to keep the time slot as is, so we are going to keep everything as planned.
- 20.04.16: First exercise sheet is available. If you have not already done so, please take part in the survey about the best time slot for the tutorial (see L2P).
- 18.04.16: Scheduled all exercise sheets.
- 15.04.16:
**IMPORTANT!**Please register for the tutorial (Übung) in Campus Office to get access to the L2P room as we will use this to provide material and announcements. - 29.03.16: Updated dates for lectures. Scheduled first exercise sheet.
- 23.02.16: We are online.

### Schedule

Type | Day | Time | Hall | Start | Lecturer |
---|---|---|---|---|---|

Lecture | Mon | 12:15 – 13:45 | AH I | 18.04. | Katoen |

Fri | 14:15 – 15:45 | AH III | 15.04. | Katoen | |

Exercise | Wed | 10:15 – 11:45 | 9U09 | 27.04. | Dehnert / Junges |

### Exam

You are allowed to bring your copy of the slides and the Principles of Model Checking book. No own notes are allowed.

The exam starts on Friday, 29/7 at 10h15 in the lecture hall AH4. Please be there at 10h00 in order to allow for a timely start.

The inspection of the exam is going to take place on Tuesday, 2 August, at 1PM in our seminar room.

### Slides

No. | Date | Topic | Slides |
---|---|---|---|

1 | 15.04. | Introduction | mc2016_slides_lec1 |

2 | 18.04. | Transition systems | mc2016_slides_lec2 |

3 | 22.04. | Concurrency | mc2016_slides_lec3 |

4 | 25.04. | Channel systems | mc2016_slides_lec4 |

5 | 29.04. | Linear-time properties | mc2016_slides_lec56 |

6 | 02.05. | Liveness and fairness | mc2016_slides_lec7 |

7 | 09.05. | Verifying regular safety properties | mc2016_slides_lec8 |

8 | 13.05. | Büchi automata (1) | mc2016_slides_lec9+10 |

9 | 23.05. | Büchi automata (2) | |

10 | 27.05. | Verifying omega-regular properties | mc2016_slides_lec11 |

11 | 30.05. | Linear temporal logic | mc2016_slides_lec12 |

12 | 06.06. | Expansion law, fairness, PNF | |

13 | 08.06. |
LTL model checking (1) | mc2016_slides_lec13+14 |

14 | 13.06. | LTL model checking (2) | |

15 | 20.06. | Complexity of LTL model checking | mc2016_slides_lec15 |

16 | 24.06. | Computation tree logic | mc2016_slides_lec16 |

17 | 27.06. | LTL versus CTL | mc2016_slides_lec17 |

18 | 01.07. | CTL model checking | mc2016_slides_lec18 |

19 | 08.07. |
CTL and fairness | mc2016_slides_lec20_part1 mc2016_slides_lec20_part2 |

20 | 11.07. | CTL+ and CTL* | mc2016_slides lec21 |

21 | 18.07. | Bisimulation and CTL* equivalence | mc2016_slides_lec22 |

22 | 22.07 | Solution to an old exam | old exam |

### Exercises

No. |
Handed Out On |
Date Due |
Exercise Sheet |
Solution |

1 | 20.04. | 27.04. | ex01 | sol01 |

2 | 27.04. | 04.05. | ex02 | sol02 |

3 | 04.05. | 11.05. | ex03 | sol03 |

4 | 13.05. | 25.05. | ex04 | sol04 |

5 | 25.05. | 01.06. | ex05 | sol05 |

6 | 01.06. | 10.06. | ex06 | sol06 |

7 | 10.06. | 22.06. | ex07 | sol07 |

8 | 22.06. | 29.06. | ex08 | sol08 |

9 | 29.06. | 06.07. | ex09 | sol09 |

10 | 06.07. | 20.07. | ex10 | sol10 |

### Motivation

In 2008, the ACM awarded the prestigious **Turing Award** – the Nobel Prize in Computer Science – to the pioneers of Model Checking: Ed Clarke, Allen Emerson, and Joseph Sifakis.

**Why?**

Because model checking has evolved in the last twenty-five years into a widely used verification and debugging technique for both software and hardware.

It is used (and further developed) by companies and institutes such as IBM, Intel, NASA, Cadence, Microsoft, and Siemens, to mention a few, and has culminated in a series of mostly freely downloadable software tools that allow the automated verification of, for instance, C#-programs or combinational hardware circuits.

Subtle errors, for instance due to multi-threading, that remain undiscovered using simulation or peer reviewing can potentially be revealed using model checking. Model checking is thus an effective technique to expose potential design errors and improve software and hardware reliability.

**But how does it work, that is, what are its underlying principles?
**That’s exactly the focus of this lecture series!

We will show that model checking is based on well-known paradigms from automata theory, graph algorithms, logic, and data structures. Its complexity is analyzed using standard techniques from complexity theory.

### Contents of the Lecture

Model checking is based on checking models. So, we first start by explaining what models are, and will make clear that so-called** labeled transition systems**, a model that is akin to automata, are suitable for modeling sequential, as well as multi-threading programs.

This is followed by a detailed study on various classes of system properties such as **safety**, **liveness**, and **fairness**. It will be shown how finite automata as well as variants thereof that accept infinite words are suitable for **verifying regular properties**.

The linear-time and branching time temporal logics **LTL** and **CTL** are then introduced and compared. Model checking algorithms for these logics together with detailed complexity considerations are covered.

Finally, abstraction techniques based on **bisimulation** and **simulation** relations are covered. These techniques are at key techniques to combat the state explosion problem.

### Prerequisites

We expect students to have some basic knowledge in:

- Automata Theory
- Mathematical Logic
- Discrete Mathematics
- Complexity Theory
- Algorithms and Data Structures

The course book (see below) will contain a summary of the issues in these areas that are relevant to this lecture series. We believe that this course is also well-suited for students in electrical engineeering and mathematics.

### Materials

The lectures and all materials are in english. The slides will be made available via this webpage during the course.

The course is based on:

Principles of Model Checking

by Christel Baier and Joost-Pieter Katoen

MIT Press, 2008.

An errata document to the book may be found here.

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.

The course will basically cover Chapters 1 through 7 (upto section 7.3).

Additional literature:

- E.M. Clarke, O. Grumberg, D.A. Peled: Model Checking, MIT Press, 1999

- 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