Title: “Automata, Logic and Games for Higher-Order Model Checking”
Course description: In Part 1 of the course, we introduce the mathematical theory underpinning the model checking of computing systems. The main ingredients are:
- Automata on infinite trees as a computational model of state-based systems.
- Logical systems, such as the modal mu-calculus and monadic second-order logic, for describing correctness properties.
- Two-person games as a conceptual basis for understanding the interactions between a system and its environment.
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.
Lecture notes 1: Automata Logic Games 2015
Lecture notes 2: Higher-Order Model Checking: An Overview
Slides and more on Luke Ong’s webpage of the course
Lecture 1 video
Lecture 2 video
Lecture 3 video
Lecture 4 video