This is a mini-course on automata and logic, given at Peking University and ISCAS. Many thanks to Zhilin Wu for organising this!

Lecture 1. Introduction to logic and automata
We start with four examples of structures that have decidable/undecidable theories, and we show that decidability of one of them – natural numbers with addition – can be obtained using automata techniques.

Lecture 2. Monadic second-order logic
In this lecture, we introduce monadic second-order logic (MSO), which can quantify over sets of elements, and only elements. We show that over finite words, this logic has the same expressive power as automata.

Lecture 3. Infinite words (no slides in 2024, but you can look here)
In this lecture, we move to infinite words, where positions are indexed by ω. One of the appropriate automata models is nondeterministic Büchi automata; we show that these are closed under complementation.

Lecture 4. Determinization of ω-automata
Büchi automata do not determinize, as we saw in the previous lecture. However, if we extend the acceptance condition – to what is called the parity condition – then they do determinism, as we show in this lecture.

Lecture 5. Games
In this lecture, we discuss games of infinite duration, which will be used in the final part of our mini-course, about tree automata. We show that these games can be quite strange in general, but the special case of parity games – which is what we will need – is well behaved and has memoryless winning strategies.

Lecture 6. The Rabin Theorem
We finish our mini-course with the Rabin Theorem, which shows that MSO has the same expressive power as automata on infinite trees. In the proof, we use two kinds of automata – nondeterministic and alternating – and the key result is that they are equivalent. The equivalence uses all of the theory developed in the previous lectures.