Infinite Automata 2025/26 (University of Warsaw, Poland)

Lectures: Henry Sinclair-Banks, hsb (at) mimuw (dot) edu (dot) pl.
Tutorials: Wojciech Czerwiński.
USOS webpage: Infinite Automata (1000-2M22AN).
Timing and location: Winter semester, Thursdays 1215 to 1345, in MIMUW 2.070.
WoW: Here is a 10 minute and 30 second advert for the course.

Starred Exercises

• Starred Exercises Series 1.
  Published: 1200 (CET), 6th November 2025.
  Deadline: 2359 (CET), 10th December 2025.

Lectured Topics

• Lecture 1: course introduction, NL, reachability in directed graphs, and reachability in one-counter machines.
  Course introduction. Lecture Notes 1.
• Lecture 2: reachability in one-counter machines, VAS, VASS, and comparing VASS with PDAs.
  Lecture Notes 2.
• Lecture 3: unary encoding vs binary encoding and reachability in binary-encoded 1-VASS is in NP.
  Lecture Notes 3.
• Lecture 4: well-quasi orders, finiteness of reachability sets, coverability separators, and coverability in VASS is decidable.
  Lecture Notes 4.
• Lecture 5: universality of VASS (is decidable) and Karp-Miller coverability trees.
  Lecture Notes 5.
• Lecture 6: correctness of Karp-Miller coverability trees and Parikh's theorem.
  Lecture Notes 6.
• Lecture 7: proof of Parikh's theorem, systems of (non-)homogeneous integer linear equations, and Pottier's lemma.
  Lecture Notes 7.
• Lecture 8: bounded 1-VASS, counter-stack automata, and subset-sum games.
  Lecture Notes 8.

Tutorial Exercises

• Tutorial 1: combinatorics of hill cutting, pushdown automata, and two-stack pushdown automata.
  Exercise Sheet 1.
• Tutorial 2: reachability in binary 1-VASS, reachability in binary 1-VAS, and path length bounds.
  Exercise Sheet 2.
• Tutorial 3: reachability in binary-encoded 1-dimensional linear path schemes, Carathéodory theorems, and reachability in multi-counter machines.
  Exercise Sheet 3.
• Tutorial 4: König's Lemma, Dickson's Lemma, well-quasi order examples, and Higman's Lemma.
  Exercise Sheet 4.
• Tutorial 5: coverability separators, ordered downward closed sets, and VASS with large reachability sets.
  Exercise Sheet 5.
• Tutorial 6: VAS can simulate VASS, semilinear sets, 3-VASS reachability sets, and solution sets to ILPs are semilinear.
  Exercise Sheet 6.
• Tutorial 7: linear path schemes are semilinear, semilinear sets are closed under intersection, semilinear sets can have linearly independent periods.
  Exercise Sheet 7.

Previous Teaching Duties (University of Warwick, UK)

I was a Senior Graduate Teaching Assistant at the University of Warwick, UK during my PhD from October 2020 to March 2024.

• January to March 2024 (term two 2023/24): Associate Tutor for Formal Languages (CS259).
• October to December 2023 (term one 2023/24): Associate Tutor* for Complexity of Algorithms (CS301).
• January to March 2023 (term two 2022/23): Associate Tutor for Approximation and Randomised Algorithms (CS356).
• October to December 2022 (term one 2022/23): Associate Tutor for Mathematics for Computer Scientists 1 (CS130).
• January to March 2022 (term two 2021/22): Associate Tutor for Approximation and Randomised Algorithms (CS356).
• October to December 2021 (term one 2021/22): Associate Tutor for Complexity of Algorithms (CS301) and Algorithms (CS260).
• January to March 2021 (term two 2020/21): Associate Tutor for Approximation and Randomised Algorithms (CS356).
• October to December 2020 (term one 2020/21): Associate Tutor for Algorithms (CS260).

*I also delivered a (48-minute) lecture about polynomial space Turing machines, as part of the Complexity of Algorithms (CS301) course, for third year undergraduate students.