- Learn the theoretical foundations of the automata theoretic approach to model checking.
- Read and present a paper in the area.

Model checking is a collection of algorithms that allow one to decide, given a formal model of a system and a formal specification, whether or not the model satisfies the specification. In the automata theoretic approach both the model and the specification are formalised as automata, and the problem then reduces to a combinatorial problem about automata. This approach yields asymptotically optimal algorithms.

The focus of this course is on finite-state models and linear-time and branching-time specifications. We will introduce all relevant definitions  (automata on words and trees), give lots of examples, and prove many of the relevant theorems (closure under Boolean operations, complexity of testing emptiness).

The course is based on the following seminal papers:
- Vardi: An Automata theoretic approach to linear temporal logic (1994).
- Kupferman, Vardi, Wolper : An automata theoretic approach to branching time model checking (1999).
- Kupferman: Automata theory and model checking (to appear in the Handbook of Model Checking, used with permission).

ECTS-BREAKDOWN:
- 30 hours of lectures
- 25 hours of reading lecture material outside of class.
- 20 hours for preparing and presenting a paper from the literature (each student can pick a paper of interest, from a range of theoretical and practical papers).

presentations, and interacting in class

Prerequisites for this course are exposure to classical automata theory (e.g., regular languages, automata operating on finite words), and temporal logics (e.g., LTL, CTL, CTL*).