Mikołaj Bojańczyk

## FoPSS School on Nominal Techniques 2019

A tutorial on sets with atoms.

## Logic and Computational Complexity 2018

A talk about programming with atoms. We consider programs, which manipulate certain kinds of infinite sets (called hereditarily definable sets). Examples of such sets include: the set of all natural numbers, the set of all sets of natural numbers that have at most two numbers missing, the set of all non-equal pairs of natural numbers. The talk discusses which properties of such sets should be called (a) decidable; (b) decidable in polynomial time. slides
a related programming language
another related programming language

## Lipa Summer School 2018

A tutorial about languages of graphs, discussing the relationship between recognisability and definability in monadic second-order logic. The first part (slides 1) is about Courcelle's definition of recognisability, although using monad terminology, and Courcelle's theorem that definability in monadic second-orde logic implies recognisability. The second part (slides 2a and slides 2b ) is about the opposite direction: for languages of bounded treewidth, recognisability implies definability in mso.

## WATA (Weighted Automata: Theory and Applications) 2018

A gentle introduction to decision procedures in algebraic geometry. The tutorial contains a proof of Tarski's theorem on the quantifier elminiation in the real field, and describes how the Hilbert Basis Theorem can be used to decide questions in automata and formal languages. The material from this tutorial is covered in the Automata Toolbox Book. Here are the slides

## Highlights 2017

On Courcelle’s conjecture, same talk as for IPEC below.

## IPEC (International Symposium on Parameterized and Exact Computation) 2017

Courcelle’s conjecture says that for classes of bounded treewidth, definability in MSO is the same as recognisability. More precisely, consider the following notions:

1. a class of graphs is called MSO definable if it can be defined in monadic second-order logic (with counting quantifiers).
2. a class of graphs is called recognisable if for each k there is a tree automaton which recognises width k tree decompositions of graphs satisfying the property.
Many natural graph classes are easily seen to satisfy (1), e.g. graphs with Hamiltonian (or Euler) paths, or 3-colourable graphs. Courcelle’s Theorem says that (1) implies (2). Courcelle’s Conjecture says that (2) implies (1) for classes of bounded tree width. The talk discusses a proof of this conjecture (joint work with Michał Pilipczuk). Slides.

## Lipa summer school 2017

A course at a summer school, to which I invited myself.

## ICALP (International Colloquium on Automata, Languages and Programming) 2017

This talk explains orbit-finite sets, which are a type of sets that are infinite but finite enough to have some algorithms run on them (see below for many talks on this topic, see also this book). The talk is dedicated to a general audience, and it uses choicless polynomial time as a point of departure. Slides.

## Automata, Concurrency and Timed Systems 2016

A talk about probabilistic extensions of monadic second-order logic. The idea is to consider monadic second-order logic over infinite trees together with a quantifier "almost surely a branch π satisfies property φ(π)". The resulting logic generalises (qualitative) probabilistic CTL, and the talk discusses the accompanying satisfiability question. here are the slides.

## Simons Institute Open Lecture 2016

This is an introduction to logic, automata and algebra intended for a general audience. The talk surveys classic results of Buchi, Schutzenberger etc., with the connections between monadic second-orderl logic, finite automata, and algebraic structures such as semigroups. You can see a video of the presentation and here are the slides.

## Symmetry, Logic, Computation 2016

This is a talk on programming with atoms, presented at a workshop at the Simons Institute. You can see a video of the presentation and here are the slides. The main message is: a) when the atoms are oligomorphic, definable sets are the same as hereditarily orbit-finite; b) these sets can be programmed using something like while programs (similar to LOIS). A related talk by Bartek Klin at the same event is about functional programming.

## Mathematical Foundations of Computer Science (MFCS) 2016

This talk asks: what can you add to MSO so that it remains decidable? The talk discusses two ideas: the unbounding quantifier, and probabilistic quantifiers. (slides)

## Computability in Europe 2016

This is a tutorial on recognisable languages, with a spin about monads at the end, an extended version of my talk for the Schützenberger conference. The tutorial gives a proof of the Büchi theorem, which says that MSO = recognisable, for finite words, ω-words, and also the extension to countable chains. The proof is automata-free, and uses mainly the composition method. (slides)

## Conference dedicated Marcel Schützenberger 2016

What is a Recognisable Language? And why is it definable in MSO? (slides)

## AAA (Arbeitstagung Allgemeine Algebra) 2016

A talk about the first-order definability question for tree languages. (slides)

## Forum Matematyków Polskich 2015

O automatach (slides)

## LCC (Logic and Computational Complexity) 2015

Yet another talk on computation with atoms. (slides)

## Jewels of Automata 2015

I propose to use monads as a generalisation of monoids, semigroups, ω-semigroups, forest algebras, etc. It turns out that anything that can be described as monad, e.g. all of the algebras from the previous sentence, will automatically have several good properties, like syntactic algebras, or pseudovariety theorems, or profinite objects. (slides, paper)

## Abstraction and Verification in Semantics 2014

Part of a trimester at the Institut Henri Poincare. Yet another talk (slides) about sets with atoms.

## FREC (Frontiers of Recognizability) 2014

A talk (slides) on the current state of MSO+U. One of the themes highlighted in the talk is the role of topology, which is important in the undecidability proof for MSO+U on infinite trees.

## CALCO (Conference on Algebra and Coalgebra) 2013

A tutorial on logic and automata. It covers the classics: monadic second-order logic and the corresponding automata on words, infinite words, and infinite trees. The slides are meant to be stand-alone, and they contain proofs of: equivalence of MSO and nondeterministic Büchi automata on infinite words, determinisation of Büchi automata into Muller and parity automata, positional determinacy of parity games, equivalence of MSO and nondeterministic parity automata on infinite trees.

## WOLLIC (Workshop on Logic, Language, Information and Computation) 2013

Yet another talk about computation with atoms. Slides same as Champery below.

## Logic Colloquium 2013

Yet another talk about computation with atoms. Slides

## RP (Reachability Problems) 2012

Computation with Atoms (slides) The talk is very similar to the one at Games (below), but there are several more slides for timed automata. The slides for the winter school at Champery are more complete, so it is better to look at them.

## Conference of the Games network 2012

Computation with Atoms (slides) The talk is very similar to the one at CSR (below), but the name is now "sets with atoms" instead of "Fraenkel-Mostowski sets", and there is more on Turing machines and timed automata. I apologize for the constant name-changing. The slides for the winter school at Champery are more complete, so it is better to look at them.

## CSR (Computer Science Symposium in Russia) 2012

Infinite Sets that are Finite up to Permutation (slides) (The slides for the winter school at Champery are more complete, so it is better to look at them.) The talk is about an approach to infinite state systems (such as automata and logics for data words). The approach is to use a different set theory, namely Fraenkel-Mostowski sets theory (also known under the following names: nominal sets, sets with ur-elements, sets with atoms, permutation models). In Fraenkel-Mostowski, there are more sets than in usual set theory, but what is most important to us, there are more finite sets. Even though the notion of finiteness is more relaxed, it is still possible to do a lot of computer science, such as programming, automata or logic.

## RTA (Rewriting Techniques and Applications) 2010

Automata for data words and data trees (slides) I talk about automata that work with data words, i.e. words where each position has a label from a finite alphabet (e.g. {a,b,c}) and a data value from an infinite domain (e.g., all natural numbers).

## Gandalf 2010

Automata for XML (slides) Very smiliar to talk to RTA above.

## STACS (Symposium on Theoretical Aspects of Computer Science) 2010

Beyond omega-regular languages (slides). I argue that there are robust classes of infinite word langauges that extend the currently accepted notion of regularity. The examples presented are mainly types of counter automata with acceptance conditions of the sort: counter c tends to infinity.

## MEMICS 2009

Automata for XML (slides) I talk about automata that work with data words, i.e. words where each position has a label from a finite alphabet (e.g. {a,b,c}) and a data value from an infinite domain (e.g., all natural numbers).

## Conference of the Games network 2009

Beyond omega-regular languages (slides). I argue that there are robust classes of infinite word langauges that extend the currently accepted notion of regularity. The examples presented are mainly types of counter automata with acceptance conditions of the sort: counter c tends to infinity.

## CSL (Computer Science Logic) 2009

Algebra for Tree Languages (slides). This talk is about the search for an algebraic for tree languages, similar to the theory of monoids for words. I talk about existing approaches, including forest algebra. Ideally, the algebra would be used to give an effective characterization of first-order logic for trees.