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