Mikołaj Bojańczyk

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 lecture is covered in the Automata Toolbox Book. Here are the slides

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

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

- a class of graphs is called MSO definable if it can be defined in monadic second-order logic (with counting quantifiers).
- 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.

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.

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.

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.

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.

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)

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)

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

Yet another talk on computation with atoms. (slides)

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)

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

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.

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

*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.

*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.

*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).

*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.

*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).

*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.

*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.

## Leave a Reply