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
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.
*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.