 Tutorials by Simon Castellan. The tutorials page is here.

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:

Course 6 (March, 28th)

Regular Properties:
 Regular Safety
 Büchi Automata and ωRegular expressions.
 Deterministic Büchi automata.

Regular Properties:

Course 7 (April, 4th)
 Generalized Büchi automata and closure under intersection of ωregular expressions.

Linear Temporal Logic (LTL):
 Syntax and Semantics.

Course 8 (April, 11th)

Linear Temporal Logic (LTL):
 Translation to Büchi automata.

Linear Temporal Logic (LTL):

Course 9 & 10 (April 28th and May 2nd)

HennessyMilner Logic and Bisimulation

Bisimulation:
 Definition and Examples
 Bisimilarity and Trace Equivalence

HennessyMilner Logic:
 Definition
 Bisimilarity implies Logical Equivalence

From Logical Equivalence to Bisimilarity:
 HennessyMilner Theorem
 Modal Saturation
 Modal Saturation by Ultrafilter Extensions

Bisimulation:

HennessyMilner Logic and Bisimulation
Back home.