We will investigate the theoretical foundations of verification:
- Automata over infinite words: acceptance conditions, expressive power, algorithms, and constructions.
- Translations between types of automata.
- Temporal logic: Linear Temporal Logic (LTL), Monadic Second Order Logic (MSO) and its fragment S1S, Buchi's theorem.
- Translation of LTL to automata, LTL model checking.
- Games: parity games and their solution, LTL synthesis using parity games.
The course material is theoretical, and will not require any programming.