In Part 1 of the course, we introduce the mathematical theory underpinning the model checking of computing systems. The main ingredients are:
Some topics: decidability of the MSO theory of the full binary tree, and its consequences; connections between parity games, modal mu-calculus, and alternating parity tree automata, and the sense in which they are equivalent.
Building on these foundations, we discuss, in Part 2, recent developments in high-order model checking, the model checking of infinite trees generated by higher-order recursion schemes (or equivalently lambda-Y calculus). Some topics: decidability of higher-order model checking with respect to modal mu-calculus, and compositional model checking of higher-type Böhm trees.