Mikołaj Bojańczyk

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