Mikołaj Bojańczyk

Automata, Logic and Games 2023

This is a course about the interplay of automata, logic and games.
Lecture: Wednesday 10:15, room 5840
Tutorial: Wednesday 12:15, same room

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.

I have updated the slides after the lecture. I have added examples, fixed some proofs and removed Muller from the lectures. The old slides can be found here.


Lecture 1. Automata & logic for finite words

  • 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].

Exam questions

  • Define MSO, and show that every regular language of finite words is definable in MSO
  • Show the opposite implication: if a language of finite words is definable in MSO, then it is regular


Lecture 2. Semigroups and compositionality of logic

  • 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].

Exam questions

  • Show that finite semigroups recognise exactly the regular languages
  • Show the equivalence of EF-games and first-order logic
  • Show that the language (aa)* is not first-order definable


Lecture 3. First order logic and friends

  • 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].

Exam questions

In the following questions, languages of finite words are considered.

  • star-free = first-order logic
  • LTL ⊆  first-order logic
  • first-order logic ⊆ aperiodic monoids
  • aperiodic monoids ⊆ LTL


Lecture 4. MSO for ω-words and Büchi automata

  • 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].

Exam questions

  • define Büchi automata, and show that deterministic ≠ nondeterministic
  • dhow that nondetermistic Büchi = semigroups (for ω-words)


Lecture 5. Determinization of ω-automata

  • Parity automata
  • Automaton based determinization
  • Semigroup based determinization

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

Exam questions

  • prove determination, using one of the two proofs; your choice


Lecture 6. Games and determinacy

  • 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].

Exam questions

  • show a game where none of the players wins
  • prove memoryless determinacy of parity games


Lecture 7. Alternating automata for ω-words and LTL

  • 3 paths from LTL to nondeterministic Büchi
  • from alternating parity to nondeterministic Büchi

Exam questions

  • define alternating parity automata on ω-words, and show that they are equivalent to nondeterministic ones


Lecture 8. Algorithms for solving parity games

This lecture was not used, so there are no exam questions.

  • a quasi-polynomial time algorithm, using universal trees

The paper with this algorithm is by Jurdziński and Lazić.


Lecture 9. Finite trees

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

Exam questions

  • describe the three models of automata for finite trees (nondet, det bottom-up, det top-down)
  • prove that MSO and automata are equivalent for finite trees

Lecture 10. Infinite trees

  • 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].

Exam questions

  • give two examples of decision problems that can be reduced to satisfiability of MSO on infinite trees

Lecture 11. Rabin’s Theorem

  • 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].

Exam questions

  • prove that alternating automata are equivalent to nondeterministic ones on infinite trees
  • decide emptiness for nondeterministic parity automata


Lecture 12. Some logics on Kripke structures

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

Exam questions

  • define LTL, CTL and CTL*
  • show that for languages of Kripke structures, alternating automata are bisimulation invariant


Lecture 13. The μ-calculus

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

Exam questions

  • define the μ-calculus and show its model checking game

Lecture 14. Graphs

  • 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