Mikołaj Bojańczyk

2024/2025

Języki, automaty i obliczenia II 2024 • Advanced topics in automata

Wykład przestawia wybrane tematy o automatach. Większość wykładu oparta jest na skrypcie Automata Toobox. W razie konsultacji zapraszam na konsultacje do mnie oraz do Lorenza Clemente i Łukasza Kamińskiego. Wszyscy mieszkamy w budynku CENT. Tutaj znajdują się zadania z ćwiczeń.

Zasady zaliczenia

Są dwie oceny z przedziału 2–5: ustny i zadania domowe. Ostateczna ocena to średnia ważona: 2/3 * ustny + 1/3 * zadania. Poniżej jest 11 tematów z pytaniami egzaminacyjnymi. Na egzaminy ustny można sobie wybrać podzbiór.
  • 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

Spis wykładów i tematy egzaminacyjne

  1. Parsowania gramatyk w czasie mnożenia macierzy Pytania na egzamin: przedstaw algorytm parsowania korzystający z mnożenia macierzy
  2. Algorytm Angluin. Pytania na egzamin: • przedstaw algorytm Angluin
  3. Systemy dodawania wektorów Pytania na egzamin: udowodnij nierozstrzygalność problemu stopu dla maszyn dwulicznikowych • udowodnij rozstrzygalność problemu "coverability" dla systemów dodawania wektorów
  4. Arytmetyka Presburgera Pytania na egzamin: • udowodnij eliminację kwantyfikatorów w arytmetyce Presburgera • pokaż, że arytmetyka Presburgera definiuje dokładnie zbiory semiliniowe
  5. Arytmetyka Tarskiego Pytania na egzamin: udowodnij rozstrzygalność teorii pierwszego rzędu dla ciała liczb rzeczywistych
  6. Prawa zero-jedynkowe Pytania na egzamin: udowodnij prawo zero-jedynkowe dla logiki pierwszego rzędu • pokaż, że nieskończony graf losowy jest jeden
  7. Automaty ważone i liniowe Pytania na egzamin: • pokaż, że automaty ważony i liniowe są równoważne • przedstaw algorytm równoważności dla tych automatów
  8. Automaty wielomianowe Pytania na egzamin: • czym są automaty wielomianowe • jak rozstrzyga się ich równoważność
  9. Automaty rejestrowe i orbitowo skończone Pytania na egzamin: co to jest zbiór orbitowo skończony • jak się rozstrzyga niepustość dla automatów orbitowo skończonych
  10. Gry nieskończone Pytania na egzamin: udowodnij pozycyjną determinację gier z warunkiem parzystości
  11. Determinizacja ω-automatów Pytania na egzamin: przedstaw podstawowe modele automatów dla ω-słów, czyli deterministyczne/niedeterministyczne automaty z warunkiem Büchiego/Mullera/parzystości • udowodnij determinizację (do warunku Mullera)
  12. Wysokość gwiazdkowa i gry Pytania na egzamin: algorytm rozstrzygający, czy automata distance jest ograniczon.
       

Automata and Logic in Beijing 2024

This is a mini-course on automata and logic, given at Peking University and ISCAS. Many thanks to Zhilin Wu for organising this! Lecture 1. Introduction to logic and automata We start with four examples of structures that have decidable/undecidable theories, and we show that decidability of one of them – natural numbers with addition – can be obtained using automata techniques. Lecture 2. Monadic second-order logic In this lecture, we introduce monadic second-order logic (MSO), which can quantify over sets of elements, and only elements. We show that over finite words, this logic has the same expressive power as automata. Lecture 3. Infinite words (no slides in 2024, but you can look here) In this lecture, we move to infinite words, where positions are indexed by ω. One of the appropriate automata models is nondeterministic Büchi automata; we show that these are closed under complementation. Lecture 4. Determinization of ω-automata Büchi automata do not determinize, as we saw in the previous lecture. However, if we extend the acceptance condition – to what is called the parity condition – then they do determinism, as we show in this lecture. Lecture 5. Games In this lecture, we discuss games of infinite duration, which will be used in the final part of our mini-course, about tree automata. We show that these games can be quite strange in general, but the special case of parity games – which is what we will need – is well behaved and has memoryless winning strategies. Lecture 6. The Rabin Theorem We finish our mini-course with the Rabin Theorem, which shows that MSO has the same expressive power as automata on infinite trees. In the proof, we use two kinds of automata – nondeterministic and alternating – and the key result is that they are equivalent. The equivalence uses all of the theory developed in the previous lectures.  

2023/2024

Złożoność Obliczeniowa / Computational Complexity 2023/2024

A course on computational complexity for 4th year students (1st year of MSc programme). Previous iterations of this course: 2022/2023 and 2020/2021

Języki, automaty i obliczenia II 2023• Advanced topics in automata

Wykład przestawia wybrane tematy o automatach. Większość wykładu oparta jest na skrypcie Automata Toobox. W razie konsultacji zapraszam na konsultacje do mnie oraz do Lorenza Clemente.

Zasady zaliczenia

Są dwie oceny z przedziału 2–5: ustny i zadania domowe. Ostateczna ocena to średnia ważona: 2/3 * ustny + 1/3 * zadania. Poniżej jest 11 tematów z pytaniami egzaminacyjnymi. Na egzaminy ustny można sobie wybrać podzbiór.
  • 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

Spis wykładów i tematy egzaminacyjne

Algorytm Angluin. Materiał: rozdział 15 w książce Toolbox. Pytania na egzamin: • przedstaw algorytm Angluin Automaty ważone i liniowe Materiał: rozdział 8 w książce Toolbox Pytania na egzamin: • pokaż, że automaty ważony i liniowe są równoważne • przedstaw algorytm równoważności dla tych automatów Automaty wielomianowe Materiał: rozdział 11 w książce Toolbox Pytania na egzamin: • czym są automaty wielomianowe • jak rozstrzyga się ich równoważność Arytmetyka Tarskiego Materiał: rozdział 10 w książce Toolbox. Treść tablicy na wykładzie Pytania na egzamin: udowodnij rozstrzygalność teorii pierwszego rzędu dla ciała liczb rzeczywistych Zbiory orbitowo skończone. Treść tablicy na wykładzie Materiał być może zbyt obfity: książka Slightly Infinite Sets  Pytania na egzamin: co to jest zbiór orbitowo skończony • jak się rozstrzyga niepustość dla automatów orbitowo skończonych Przestrzenie wektorowe orbitowo skończone  Treść tablicy na wykładzie Pytania na egzamin: co to jest przestrzeń wektorowa orbitowo skończona • udowodnij, że łańcuch podprzestrzeni są skończone Systemy dodawania wektorów Materiał: rozdział 9 w książce Toolbox Pytania na egzamin: udowodnij nierozstrzygalność problemu stopu dla maszyn dwulicznikowych • udowodnij rozstrzygalność problemu "coverability" dla systemów dodawania wektorów Parsowania gramatyk w czasie mnożenia macierzy Materiał: rozdział 12 w książce Toolbox Pytania na egzamin: przedstaw algorytm parsowania korzystający z mnożenia macierzy Determinizacja ω-automatów Materiał: rozdział 1 w książce Toolbox Pytania na egzamin: przedstaw podstawowe modele automatów dla ω-słów, czyli deterministyczne/niedeterministyczne automaty z warunkiem Büchiego/Mullera/parzystości • udowodnij determinizację (do warunku Mullera) Gry nieskończone Materiał: rozdział 2 w książce Toolbox Pytania na egzamin: udowodnij pozycyjną determinację gier z warunkiem parzystości Twierdzenie Rabina  Materiał: rozdział 5 w książce Toolbox Pytania na egzamin: udowodnij twierdzenie Rabina, zakładając wyniki z dwóch poprzednich wykładów.        

Przekształcenia automatowe • Transducers

This is the page for a transducer course, given at the University of Warsaw in 2024. The tutorials are by Aliaume Lopez, you can find the problems here.

Grading

Your grade is based on points.
  • 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
Therefore, if we ignore the star exercises, you can get 23 points. Since there is a lot of material, you do not need to get all points. Here are the thresholds for the various grades (see also the additional condition below):
  • 3: 9 points
  • 3+: 10 points
  • 4: 11 points
  • 4+: 13 points
  • 5: 15 points
Additional condition: regardless of the number of points you have, in order to pass you need to know at least 6 lectures for your oral exam.

Oral exam.

At the oral exam, you declare which of the lectures you have learned (but at least 6, as per the additional condition), and you will be asked some (not necessarily all) exam questions for your declared lectures. You can approach the oral exam as many times as you wish, but I will get annoyed if I have the feeling that you are abusing this (this does not happen in my experience). You can schedule the exam as you wish (up to July 5), but I would prefer if you used two either June 25 or July 2 for your first attempt; sign up here. If you want a second attempt (sesja poprawkowa), then the homeworks will no longer count, but the lectures will be worth 1.5 points instead of 1.

Lectures

1. Mealy machines

Slides
  • Definition of Mealy machines
  • Closure under composition
  • The Krohn-Rhodes Theorem
Exam questions:
  • Define Mealy machines, and show that they are closed under composition
  • Prove the Krohn-Rhodes Theorem about Mealy machines

2. Rational functions

Slides
  • Unambiguous nondeterministic automata with output
  • Eilenberg Bi-machines
  • Their equivalence
  • A Krohn-Rhodes decomposition
  • Deciding equivalence
Exam questions:
  • 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

3. Enter logic

Slides
  • MSO = regular languages
  • MSO relabelings = letter-to-letter rational
  • the first-order fragment of MSO
Exam questions:
  • 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

4. Two-way automata

Slides
  • Two-way automata with output (2DFA)
  • Closure under pre-composition
  • Decidable equivalence
Exam questions:
  • Warm-up: prove that 2DFA  are continuous
  • Prove that 2DFA are closed under composition
  • Prove that equivalence is decidable for 2DFA

5. MSO transductions

Slides
  • Definition of MSO transductions
  • Equivalence with previous two models
Exam questions:
  • Show that MSO transductions are closed under composition
  • Prove MSO transductions are the same as 2DFA

6. Streaming string transducers

Slides
  • Definition of copy less streaming stream transducers (SST)
  • Equivalence with two-way automata with output
Exam questions:
  • Show that SST are the same as 2DFA = MSO transductions

7. List functions

Slides
  • 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
Exam questions:
  • Define the linear list functions, and show that they are equivalent to 2DFA

8. Introduction to polyregular functions

Slides
  • Polynomial Krohn-Rhodes primes
  • Polynomial list functions
  • For-transducers
  • Equivalence of all three models
Exam questions:
  • 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)*

9. Pebble transducers

Slides
  • Pebble transducers
  • Their equivalence to the polynomial list functions and for transducers
Exam questions:
  • Prove pebble ⊆ polynomial list functions

10. A functional programming language

Slides
  • Polynomial list functions with λ
Exam questions:
  • 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.

11. Polynomial interpretations 1

Slides
  • First-order interpretations on general structures
  • Difficulties with MSO interpretations
Exam questions:
  • 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

12. Polynomial interpretations 2

Slides
  • The Simon Theorem on factorizations
  • Using it to for quantifier elimination
Exam questions:
  • Prove the Simon Theorem
  • Prove quantifier elimination for MSO interpretations

13. Polynomial interpretations 3

Slides
  • Quantifier-free interpretations are polyregular
Exam questions:
  • Show that every quantifier-free interpretation, of tree-to-string type, is polyregular
 

Research projects

Here is a list of open problems about polyregular functions.

   

2022/2023

Złożoność Obliczeniowa / Computational Complexity 2022/2023

A course on computational complexity for 4th year students (1st year of MSc programme).

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.

2021/2022

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.

2020/2021

Computational Complexity / Złożoność obliczeniowa 2020/2021

A course on computational complexity for 4th year students (1st year of MSc programme).

A tutorial on logic, biased towards automata, for the TCFS programme at Simons

This is a 3 part tutorial about logic. It is organised around algorithms for checking if a formula is true in a model.There are two central variants of this problem. In the model checking problem $$M \stackrel ? \models \varphi,$$ we are given the model and the formula, and we want to know it the formula is true in the model. In the satisfiability (dually, validity) problem $$? \models \varphi$$ we are only given the formula, and we want to know if it is true in some (dually, every) model (perhaps from some fixed class of models). There are three parts of the tutorial (each set of slides contains a soundtrack):
  1. 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.
  2. 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.
  3. 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.
There is also an abbreviated one-part version, without a soundtrack.  

2019/2020

Transducers and their Krohn-Rhodes decompositions

This is a course on transducers, given before the Trends in Transformations workshop at FSTTCS 2019. The course covers rational, regular and polyregular string-to-string functions. A special emphasis is made on theorems a la Krohn-Rhodes, which decompose complicated functions into simpler prime functions.
  1. Mealy machines, the classical Krohn-Rhodes theorem, and its corollaries for sequential and rational functions (slides).
  2. 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).
  3. Polyregular functions, and some of their equivalent representations (pebble transducers, for transducers, functional programs, mso interpretations). The prime polyregular functions (slides).

Algebraic language theory 2020

This course is about an alternative approach to regular languages, where one uses semigroups and monoids (and more fancy algebraic structures) instead of automata.

Soft skills

These are some slides for my Scientist's Workshop lecture.

2017/2018

Algebraic language theory (automaty a półgrupy)

This course is about an alternative approach to regular languages, where one uses monoids (and more fancy algebraic structures) instead of automata.  I use notes from this lecture, but I hope to create a new version in pdf for this one (this has not materialised, I'm sorry).

Advanced Topics in Automata 2017/2018 (Języki, Automaty i Obliczenia 2)

This lecture is a choice of slightly more advanced topics from automata theory.

2016/2017

Advanced Topics in Automata 2016/2017 (Języki, Automaty i Obliczenia 2)

This lecture is a choice of slightly more advanced topics from automata theory. The lecture is on Tuesdays, 12:15 in room 5820. The exercises are on Wednesdays, 16:15 in room 5820, with Wojciech Czerwiński. Here is a plan of the lecture. There was a similar lecture last year. Here are the topics for this year:
  1. automata on infinite words: determinisation
  2. games of infinite duration: the Büchi-Landweber theorem
  3. distance automata: decidability of limitedness
  4. treewidth and mso: Courcelle's theorem
  5. learning automata: the Angluin algorithm
  6. transducers
Exam. The exam is an oral exam, which is mainly questions about the proofs of theorems. Please email me to choose a time. You can improve your exam grade using the star exercises.  Choose any subset of the 6 topics in the list above, here is the exchange rate: • 2 topics: dostateczny • 3 topics: dobry • 4 topics: bardzo dobry

Infinite alphabets

This is a lecture on automata (and later other devices) that operate on infinite alphabets. The lecture is on Wednesdays at 12:15 in room 4060. The exercises are on Mondays at 14:15 in room 5050. The lecture and exercises are shared by Mikołaj Bojańczyk and Sławomir Lasota. Lecture notes Homework assignments Exam
  Here is an overview of the course Data words and their automata In the first half of the lecture, we discuss some concrete models, typically involving registers. The emptiness problem for most powerful of the models, data automata, will as hard as the famous reachability problem for vector addition systems, and the lecture will contain a description of the latter.
  1. Introduction to automata with registers
  2. Alternating automata with registers
  3. Data automata
  4. Logic on data words
  5. Reachability for vector addition systems
Sets with atoms In the second part of the lecture, we move to a more general setting, which describes some of the previous constructions in a cleaner mathematical model. This mathematical model will lead us to discover new questions.
  1. Sets with atoms and orbit-finiteness
  2. Automata in sets with atoms
  3. Atoms with structure other than equality
  4. Oligomorphism
  5. What is a computable function?
  6. Turing machines with atoms

Lipa

Lipa summer school 2017 (Warsaw, July 3-6)

The Lipa Summer School is a school on topics connected to logic in computer science. It is part of this grant. It was held in Warsaw, July 3-6 2017.  The school had 4 mini-courses given by:
  • Stephan Kreutzer (Berlin) Algorithmic meta-theorems (videos: 1, 2, 3, 4)
  • Joël Ouaknine (Saarbrücken) Decision Problems for Linear Recurrence Sequences (videos: 1234)
  • Moshe Vardi (Rice)  Linear-time verification and synthesis  (videos: 1234)
  • Mikołaj Bojańczyk (Warsaw, organiser) What is a recognisable language? (videos: 1234)
Each mini-course was 6 hours long (4 x 90 minutes). Here is the programme. Registration is closed. There will be free lunch and coffee breaks for registered participants, but not dinner (we will do an informal picnic on some evening without rain). The school is followed by ICALP.

Dates

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


Local information

The school was held at the University of Warsaw, in the Center of New Technologies, whose address is Banacha 2c. Be careful about the map on the Center's page, it's wrong, use the one below.   Picture of the conference venue and map below   A taxi from the airport should be around ≤ 20 PLN during the day (the official taxi queue is when you leave the airport, don't go with the people who whisper "taxi, taxi"). Here is a link for accessing the school from the airport using public transport (bus 175 or 188).  
The school is part of the grant Lipa that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 683080).

Lipa Summer School 2018 (June 25-28)

The Lipa Summer School is a school on topics connected to logic in computer science. It is part of this grant. This is the second edition, the first one was in 2017 (there are videos).  It will be held in Warsaw, June 25-28 2018.  The school consists of 4 mini-courses given by: Each mini-course is 6 hours long (4 x 90 minutes). Here is the program. Click on the talk titles to get descriptions and slides. There will be videos, but a few months after the school is over. Registration is free, and we might have a limited number of student dormitories for free.  We will likely (depending on the number of registrations) have  free lunch and coffee breaks for registered participants, but no dinner (we will do an informal picnic on some evening without rain).  

Dates

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

Venue

The school will be held in (room C of the) Auditorium Maximum of the university of Warsaw, in the historical center of Warsaw. Here is the building: Here is a map:
The school is part of the grant Lipa that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 683080).

2015/2016

Algebraic Language Theory

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.

Advanced Topics in Automata (Języki, Automaty i Obliczenia 2)

This lecture is a choice of slightly more advanced topics from automata theory. The lecture is on Tuesdays, 12:15 in room 5070. The exercises are on Wednesdays, 16:15 in in room 5820, with Wojciech Czerwiński.
  1. automata on infinite words: determinisation
  2. games of infinite duration: the Büchi-Landweber theorem
  3. weighted automata: decidable and undecidable problems
  4. distance automata: decidability of limitedness
  5. tree-walking automata: failure of determinisation
  6. transducers
  7. learning automata: the Angluin algorithm
  8. automata with infinite alphabets
  9. sets with atoms
Here are the star exercises and their solvers. Exam. The exam is an oral exam. Please email me to choose a time or use this link for Feb 15. Choose any subset of the 9 topics in the list above, here is the exchange rate: • 3 topics: dostateczny • 5 topics: dobry • 7 topics: bardzo dobry  

2014/2015

Algebraic Language Theory

This course is about an alternative approach to regular languages, where one uses monoids or semigroups instead of automata. Lecture: Tuesdays 8:45-10:15 (room 5070) Exercises: Tuesdays 10:25-11:55 (room 5070)

Języki i paradygmaty programowania

Laboratorium do wykładu Marcina Benke.

2013/2014

2011/2012

2009/2010

2008/2009