Mikołaj Bojańczyk

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 summer school (Warsaw, July 3-6, 2017)

Programme

Programme

 

Monday, July 3

8:50 - 9:00 Welcome 9:00 - 10:30 Moshe Vardi Linear-time verification and synthesis 10:30 - 11:00 Coffee break 11:00 - 12:30 Joël Ouaknine Linear recurrence sequences 12:30 - 14:00 Lunch 14:00 - 15:30 Stephan Kreutzer Algorithmic meta-theorems 15:30 - 16:00 Coffee break 16:00 - 17:30 Stephan Kreutzer Algorithmic meta-theorems

Tuesday, July 4

9:00 - 10:30 Moshe Vardi Linear-time verification and synthesis 10:30 - 11:00 Coffee break 11:00 - 12:30 Joël Ouaknine Linear recurrence sequences 12:30 - 14:00 Lunch 14:00 - 15:30 Stephan Kreutzer Algorithmic meta-theorems 15:30 - 16:00 Coffee break 16:00 - 17:30 Stephan Kreutzer Algorithmic meta-theorems

Wednesday, July 5

9:00 - 10:30 Moshe Vardi Linear-time verification and synthesis 10:30 - 11:00 Coffee break 11:00 - 12:30 Joël Ouaknine Linear recurrence sequences 12:30 - 14:00 Lunch 14:00 - 15:30 Mikołaj Bojańczyk What is a recognisable language? 15:30 - 16:00 Coffee break 16:00 - 17:30 Mikołaj Bojańczyk What is a recognisable language?

Thursday, July 6

9:00 - 10:30 Moshe Vardi Linear-time verification and synthesis 10:30 - 11:00 Coffee break 11:00 - 12:30 Joël Ouaknine Linear recurrence sequences 12:30 - 14:00 Lunch 14:00 - 15:30 Mikołaj Bojańczyk What is a recognisable language? 15:30 - 16:00 Coffee break 16:00 - 17:30 Mikołaj Bojańczyk What is a recognisable language?

Linear-time verification and synthesis

This one of the courses at the Lipa Summer School.

Moshe Vardi

Linear-time verification and synthesis

Algorithmic verification is one of the most successful applications of automated reasoning in computer science. In algorithmic verification one uses algorithmic techniques to establish the correctness of the system under verification with respect to a given property. Automama-theoretic Model checking is an algorithmic-verification technique that is based on a small number of key ideas, tying together graph theory, automata theory, and logic. In this self-contained tutorial I will describe how this "holy trinity" gave rise to algorithmic-verification tools, and discuss its applicability to both finite-state and infinite-state systems.

Decision Problems for Linear Recurrence Sequences

This one of the courses at the Lipa Summer School.

Joël Ouaknine

Decision Problems for Linear Recurrence Sequences

  Linear recurrence sequence (LRS), such as the Fibonacci numbers, permeate vast areas of mathematics, physics, and computer science. In this tutorial, I consider some fundamental decision problems for LRS over the integers, such as the Skolem Problem (does the sequence have a zero?) and the Positivity Problem (are all terms of the sequence positive?).
In general, the decidability of such problems is open, but various partial results are known. I will introduce some of the key mathematical tools for attacking these problems, and present some of the known results.

Algorithmic meta-theorems

This one of the courses at the Lipa Summer School.

Stephan Kreutzer

Algorithmic meta-theorems

  Abstract TBA

What is a recognisable language?

This one of the courses at the Lipa Summer School.

Mikołaj Bojańczyk

What is a recognisable language?

  This course is about the algebraic approach to regular languages, which uses algebras instead of automata. The emphasis is on the connection of recognisability and definability in monadic second-order logic MSO. Click the title links for slides. Part 1: finite words Classical results from the algebraic approach to finite words, where the algebras are monoids. As one example of the usefulness of monoids, I will present the Factorisation Forest Theorem of Imre Simon. Part 2: infinite words Monoids for infinite words, such as countable labelled linear orders. Part 3: monads  A bit of abstract nonsense, trying to answer the question: what is an algebra in general? The answer is to use Eilenberg-Moore algebras over a suitably chosen monad. Part 4: graphs Graphs. I will give half of the proof of the following result: for a class of graphs of bounded treewidth, being recognisable is equivalent to being definable in monadic second-order logic.  

Lipa

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