Mikołaj Bojańczyk

Automata, logic and games


This is a course about the interplay of automata, logic and games.

The automata are finite automata, but often on objects that are not necessarily finite words. The logic is usually monadic second-order logic. The point is that the automata and the logic define the same languages. The games are infinite duration games, which appear as technical tool in the analysis of automata and logics on infinite objects.

I will also use semigroups, as a third approach to defining languages.


Please submit any mistakes in the slides, or change requests, in this document.

Lecture 1. Automata & logic for finite words (October 11 and 13)

  • the subset construction for determining automata on finite words
  • monadic second-order logic (MSO) on finite words
  • the equivalence of MSO and automata for finite words
  • satisfiability for MSO is non-elementary

A good introduction that covers this material is Sections 2 and 3 of [Tho].

Lecture 2. Semigroups and compositionality of logic (October 13, 15, and 18)

  • monoids and semigroups
  • their equivalence to automata
  • Ehrenfeucht-Fraisse games
  • compositionality of both first-order logic and MSO

The material of this lecture is covered in more detail in Sections 2.1 and 2.2 of [Reco].

Lecture 3. First order logic and friends (October 18 and 22)

  • star-free languages and their equivalence to first-order logic
  • aperiodic monoids
  • linear temporal logic LTL (on finite words)
  • equivalence of first order logic, aperiodic monoids, and LTL
  • PSPACE completeness of LTL satisfiability, via alternating automata

A discussion of first-order logic is in Section 4 of [Tho]. The translation from aperiodic to LTL is based more on Section 2.2 of [Reco].

Lecture 4. MSO for ω-words and Büchi automata (October 26 and 28)

  • MSO on infinite words
  • Büchi automata and their necessary nondeterminism
  • Semigroups for infinite words (lightweight approach)
  • Equivalence of all models

The semigroup approach to Büchi automata is covered in more detail in Section 3.1 of [Reco].

Lecture 5. Determinization of ω-automata (October 28 and 30)

  • Muller automata
  • Automaton based determinization (inspired by Muller and Schupp)
  • Semigroup based determinization

The automaton determinization is described in Chapter 1 of [Toolbox]. The semigroup determinization is based on Section 3.1 of [Reco].

Lecture 6. Games and determinacy (November 1 and 3)

  • infinite games as a tool to define semantics of alternating automata
  • an example of an infinite game where none of the players wins
  • memoryless determinacy of parity games

A similar proof of memoryless determinacy is in Section 6.2 of [Tho].

Lecture 7. Muller vs parity, and alternating automata for ω-words (November 5 and 8)

  • from Muller to parity via latest appearance records
  • from alternating parity to nondeterministic Büchi

The latest appearance record structure is described in the proof of Theorem 6.5 in [Tho].

Lecture 8. Algorithms for solving parity games (November 8 – 12)

  • a quasi-polynomial time algorithm, using universal trees

Lecture 9. Finite trees (November 12)

  • finite trees and logic on them
  • nondeterministic automata, including bottom-up determinisation
  • equivalence of mso and automata

Lecture 10. Infinite trees (November 15)

  • MSO on infinite trees, and what can be expressed in this logic

Infinite trees and MSO on them are treated in Section 6 of  [Tho].

Lecture 11. Rabin’s Theorem (November 17 and 19)

  • parity automata on infinite trees: nondeterministic, and alternating
  • from alternating parity to nondeterministic parity
  • emptiness algorithm for nondeterministic parity, and regular trees

Automata on infinite trees, but without an emphasis on alternating automata are treated in Section 6 of  [Tho].

Lecture 12. Some logics on Kripke structures (November 19 and 22)

  • LTL and PSPACE-completeness of its model checking
  • modal logic
  • CTL
  • CTL*
  • alternating automata

Lecture 13. The μ-calculus (November 22 and 24)

  • fix-points and the μ-calculus
  • model checking using a parity game

Lecture 14. Graphs (November 26)

  • MSO on graphs, and its undecidability
  • treewidth

Lecture 15. MSO transductions

  • bounded treewidth as image of MSO transductions from trees
  • model checking on bounded treewidth
  • decidable satisfiability iff bounded treewidth