MSO transductions are binary relations between classes of structures which are defined using monadic second-order logic. An example of an MSO transduction is the relation that consists of pairs (G,T) where G is some graph and T is one of its spanning trees. MSO transductions form a category, since they are closed under composition. In my talk, I will discuss this category, and show its usefulness by explaining how many notions, such as tree decompositions or recognizability, can be defined by only using MSO transductions. Part of this is rooted in classical results of Courcelle and Engelfriet, but there are new results as well. (This talk was a last missing replacement for one of the actual invited speakers at the conference.) Slides.
Transducers of polynomial growth. The polyregular functions are a class of string-to-string functions that have polynomial size outputs, and which can be defined using finite state models. There are many equivalent definitions of this class, with roots in automata theory, programming languages and logic. The talk surveys recent results on polyregular functions. It presents five of the equivalent definitions, and gives self-contained proofs for most of the equivalences. Decision problems as well as restricted subclasses of the polyregular functions are also discussed. Slides.
A view on weighted languages that uses monads and distributive laws.
A talk at a centennary event for Trakhtenbrot, about the transducer approach to automata and logic. Slides.
A tutorial on sets with atoms.
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
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.
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
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:
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 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 )
A talk about the first-order definability question for tree languages. ( 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 )
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.
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.
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.
COMMENTS
October 25, 2023
Hi Shashwat, I'm not sure if I will find funding, but please send me your cv so that I can search for any possibilities. Mikołaj
Shashwat Kasliwal
October 25, 2023
Amazing Work,Professor Are you taking Undergraduate Research Interns this year?