Slides

Chapter 1 - Overview and Model Checking On-the-Fly

• transparencies
     1-up    2-up    4-up

Chapter 2 - F1S, S1S, and Translation into Büchi-Automata

• transparencies (fixed definition of transition profile automaton, states are 2^TP instead of TP)
     1-up    2-up    4-up

Chapter 3 - Abstractions, Bisimulations, and Simulations

• transparencies (fixed definition of refine algorithm where ... \ {emptyset} instead of ... \ emptyset is used)
     1-up    2-up    4-up

Chapter 4 - The μ-Calculus

• transparencies
     1-up    2-up    4-up    overlays

Chapter 5 - Real-Time Systems and Timed CTL

• transparencies
     1-up    2-up    4-up

Schedule

June 22

• Discussion of Exercises 20-23, Chapter 5

June 16

• Chapter 5

June 15

• Chapter 4 and 5

June 8

• Discussion of Exercises 17-19, afterwards Chapter 4

May 25

• Chapter 4

May 18

• Discussion of Exercises 15-16, afterwards Chapter 3 and Chapter 4

May 11

• Discussion of Exercise 14, afterwards Chapter 3

May 4

• Discussion of Exercises 9 - 13, afterwards Chapter 3

April 13

• Chapter 3

April 6

• Chapter 2-3

March 30

• Discussion of exercises

March 23

• Chapter 2

March 16

• Chapter 2

March 8

• Chapter 1