Mikołaj Bojańczyk

2023/2024

- na ocenę 5 trzeba się nauczyć 9 tematów
- na ocenę 4 trzeba się nauczyć 6 tematów
- na ocenę 3 trzeba się nauczyć 4 tematów

- 5 points for each of the two homeworks
- 1 point for learning the theory in each of the 13 lectures, tested at the oral exam
- bonus points for star exercises

- 3: 9 points
- 3+: 10 points
- 4: 11 points
- 4+: 13 points
- 5: 15 points

- Definition of Mealy machines
- Closure under composition
- The Krohn-Rhodes Theorem

- Define Mealy machines, and show that they are closed under composition
- Prove the Krohn-Rhodes Theorem about Mealy machines

- Unambiguous nondeterministic automata with output
- Eilenberg Bi-machines
- Their equivalence
- A Krohn-Rhodes decomposition
- Deciding equivalence

- Prove the equivalence between bi-mcahines and unambiguous nondeterministic automata with output
- Prove the Krohn-Rhodes Theorem for this model (which is called rational functions)
- Show that equivalence is decidable for rational functions

- MSO = regular languages
- MSO relabelings = letter-to-letter rational
- the first-order fragment of MSO

- Prove that MSO=regular languages
- Prove that a language is first-order definable if and only if it is recognised by a counter-free automaton

- Two-way automata with output (2DFA)
- Closure under pre-composition
- Decidable equivalence

- Warm-up: prove that 2DFA are continuous
- Prove that 2DFA are closed under composition
- Prove that equivalence is decidable for 2DFA

- Definition of MSO transductions
- Equivalence with previous two models

- Show that MSO transductions are closed under composition
- Prove MSO transductions are the same as 2DFA

- Definition of copy less streaming stream transducers (SST)
- Equivalence with two-way automata with output

- Show that SST are the same as 2DFA = MSO transductions

- Definition of the linear list functions
- Their first-order fragment
- Proof that they define the same functions as two-way transducers
- Krohn-Rhodes decomposition for linear regular functions

- Define the linear list functions, and show that they are equivalent to 2DFA

- Polynomial Krohn-Rhodes primes
- Polynomial list functions
- For-transducers
- Equivalence of all three models

- Define the polynomial Krohn-Rhodes primes, and show that they are continuous
- Define the polynomial list functions, and show how split and reverse are redundant
- Define for-transducers, and show that each one can be converted into prenex normal form (all loops on the outside)
- Prove (Krohn-Rhodes primes)* ⊆ polynomial list functions
- Prove polynomial list functions ⊆ for-transducers
- Prove for-transducers ⊆ (Krohn-Rhodes primes)*

- Pebble transducers
- Their equivalence to the polynomial list functions and for transducers

- Prove pebble ⊆ polynomial list functions

- Polynomial list functions with λ

- Define the syntax and semantics of the λ-calculus extension of polynomial list functions
- What is β-reduction on λ-terms, and what are normal forms
- Show that one step of β-reduction can be implemented by a for-transducer.

- First-order interpretations on general structures
- Difficulties with MSO interpretations

- Define first-order interpretations, and prove that they are closed under composition
- Define MSO interpretations, and prove that they need not be closed under compositions

- The Simon Theorem on factorizations
- Using it to for quantifier elimination

- Prove the Simon Theorem
- Prove quantifier elimination for MSO interpretations

- Quantifier-free interpretations are polyregular

- Show that every quantifier-free interpretation, of tree-to-string type, is polyregular

2022/2023

2021/2022

2020/2021

- Part 1 (slides ) discusses the variant of the model checking problem where the model is fixed and only the formula is given on the input. (This is also known as deciding the theory of the model.) I will particularly focus on cases where the problem can be solved using automata, and hence the corresponding logic is going to be monadic second-order logic, which is an old friend of automata.
- Part 2 (slides) discusses the satisfiability problem. Here, again, the main focus is on variants of the problem that can be solved using automata, namely monadic second-order logic on words, trees and graphs of bounded treewidth.
- Part 2 (slides) discusses the variant of the model checking problem where the formula is fixed and the model is the input. Apart from results that use automata (mainly Courcelle's theorem about MSO model checking on graphs of bounded treewidth), I will also discuss some results about first-order logic on sparse graph classes.

2019/2020

- Mealy machines, the classical Krohn-Rhodes theorem, and its corollaries for sequential and rational functions (slides).
- Regular functions, and some of their equivalent representations (two-way transducers, mso transductions, streaming string transducers, and regular list functions). The prime regular functions (slides).
- Polyregular functions, and some of their equivalent representations (pebble transducers, for transducers, functional programs, mso interpretations). The prime polyregular functions (slides).

2017/2018

2016/2017

- automata on infinite words: determinisation
- games of infinite duration: the Büchi-Landweber theorem
- distance automata: decidability of limitedness
- treewidth and mso: Courcelle's theorem
- learning automata: the Angluin algorithm
- transducers

Here is an overview of the course

- Introduction to automata with registers
- Alternating automata with registers
- Data automata
- Logic on data words
- Reachability for vector addition systems

- Sets with atoms and orbit-finiteness
- Automata in sets with atoms
- Atoms with structure other than equality
- Oligomorphism
- What is a computable function?
- Turing machines with atoms

Lipa

- Stephan Kreutzer (Berlin)
*Algorithmic meta-theorems*(videos: 1, 2, 3, 4) - Joël Ouaknine (Saarbrücken)
*Decision Problems for Linear Recurrence Sequences*(videos: 1, 2, 3, 4) - Moshe Vardi (Rice)
*Linear-time verification and synthesis*(videos: 1, 2, 3, 4) - Mikołaj Bojańczyk (Warsaw, organiser)
*What is a recognisable language?*(videos: 1, 2, 3, 4)

~~May 30 Registration with request for student accommodation~~~~June 20 Registration without request for student accommodation~~~~July 3-6 School~~

The school is part of the grant

- Rajeev Alur (UPenn)
*Regular processing of data streams* - Matt Valeriote (McMaster)
*Finite algebras and connections with tree languages* - Igor Walukiewicz (Bordeaux)
*MSOL and higher-order computation* - Mikołaj Bojańczyk (Warsaw, organiser)
*Recognisable languages of graphs*

~~May 15 End of~~**registration**with request for student accommodation~~June 15 End of registration without request for student accommodation~~- June 25-28 School

The school is part of the grant

2015/2016

The general theme is monoids instead of automata. We will go deep (e.g. on the structure of finite monoids) and wide (on "monoids" for infinite words etc.)

**Lecture**: Thursday 12:15 – 13:45 (room 3170)
**Exercise**: Thursday 14:15 – 15:45 (room 3170)

I will use the notes from my previous course, but modified.

- automata on infinite words: determinisation
- games of infinite duration: the Büchi-Landweber theorem
- weighted automata: decidable and undecidable problems
- distance automata: decidability of limitedness
- tree-walking automata: failure of determinisation
- transducers
- learning automata: the Angluin algorithm
- automata with infinite alphabets
- sets with atoms

2014/2015

2013/2014

2011/2012

2009/2010

2008/2009