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.
The course will be given on Zoom (until further notice).
The lectures will take place here:
The Passcode is: ALG2021