TACL 2015 Summer School

Automata, Logic and Games: Theory and Application

Course Abstract

In Part 1 of the course, we introduce the mathematical theory underpinning the model checking of computing systems. The main ingredients are:

1. Automata on infinite trees as a computational model of state-based systems.
2. Logical systems, such as the modal mu-calculus and monadic second-order logic, for describing correctness properties.
3. 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 Slides

1. Büchi automata and S1S
2. Parity games, tree automata and S2S
3. Higher-order model checking 1
4. Higher-order model checking 2

References

1. Luke Ong: Automata, Logic and Games, Lecture Notes, University of Oxford, 2015.
2. Luke Ong: Higher-Order Model Checking: An Overview, LICS 2015.