 Tutorials by Simon Castellan.

The course closely follows the book:
 Baier, C. and Katoen, J.P., Principles of Model Checking, MIT Press, 2008.
Courses

Course 1 (Feb. 14th)
 General overview of the course.
 Modelling Concurrent Systems (part. 1).

Course 2 (Feb. 28th)
 Modelling Concurrent Systems (part. 2).

LinearTime Properties:
 General definition and Examples.

Course 3 (March 7th)

LinearTime Properties:
 Some basic properties.
 Safety: Definition, Examples and Basic properties.

LinearTime Properties:

Course 4 (March, 14th)
 Some topological considerations.

Course 5 (March, 21st)

LinearTime Properties:
 Liveness.
 Every L.T. prop. is the intersection of a Safety prop. and a Liveness prop.
 Fairness assumptions.

LinearTime Properties:
Back home.