## Logique, automates, algèbre et jeux

#### Jour, heure et lieu

Le Mercredi à 14h, salle 4033

Le calendrier des séances (format iCal).

Pour ajouter le calendrier des séances à votre agenda favori, souscrire au calendrier en indiquant ce lien.

#### Contact(s)

Ce groupe de travail propose des exposés de deux heures au tableau sur des sujets classique ou plus récents traitant de logique, d'automates, de méthodes algébriques et de jeux.

Le groupe de travail se déroule environ toutes les deux semaines, en général les mercredi à 14h en salle 4033, bâtiment Sophie Germain.

### Séances passées

#### Année 2019

Logique, automates, algèbre et jeux

Mercredi 22 mai 2019, 14 heures 15, 3052

**Uri Zwick** (Blavatnik School of Computer Science) *Games on Graphs and Linear Programming Abstractions, Part 7/7: Lower bounds for Random-Facet and Random-Edge*

https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf

Logique, automates, algèbre et jeux

Mercredi 15 mai 2019, 14 heures 15, 3052

**Uri Zwick** (Blavatnik School of Computer Science) *Games on Graphs and Linear Programming Abstractions, Part 6/7: Lower bounds for Policy Iteration*

https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf

Logique, automates, algèbre et jeux

Mercredi 17 avril 2019, 14 heures 15, 3052

**Uri Zwick** (Blavatnik School of Computer Science) *Games on Graphs and Linear Programming Abstractions, Part 5/7: Parity Games*

https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf

Logique, automates, algèbre et jeux

Mercredi 10 avril 2019, 14 heures 15, 3052

**Uri Zwick** (Blavatnik School of Computer Science) *Games on Graphs and Linear Programming Abstractions, Part 4/7: Acyclic Unique Sink Orientations (AUSOs)*

https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf

Logique, automates, algèbre et jeux

Mercredi 3 avril 2019, 14 heures 15, 3052

**Uri Zwick** (Blavatnik School of Computer Science) *Games on Graphs and Linear Programming Abstractions, Part 3/7: Randomized sub-exponential time algorithm*

*sub-exponential*time. This is currently the fastest known algorithm for TBSGs, and also for MPGs and EGs, when there is no restriction on the edge costs. The algorithm is an adaptation of a randomized algorithms of Kalai and Matousek, Sharir and Welzl for solving linear programs. We also mention relations to abstractions of Linear Programming abstractions.

https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf

Logique, automates, algèbre et jeux

Mercredi 27 mars 2019, 14 heures 15, 3052

**Uri Zwick** (Blavatnik School of Computer Science) *Games on Graphs and Linear Programming Abstractions, Part 2/7: Mean Payoff games and Energy Games*

https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf

Logique, automates, algèbre et jeux

Mercredi 20 mars 2019, 14 heures 15, 3052

**Uri Zwick** (Blavatnik School of Computer Science) *Games on Graphs and Linear Programming Abstractions, Part 1/7: Two-player Turn-based Stochastic Games*

https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf

#### Année 2018

Logique, automates, algèbre et jeux

Mercredi 9 mai 2018, 14 heures, 3014

**Thomas Colcombet** (IRIF) *Superpolynomial lower bound for complementing unambiguous automata*

Logique, automates, algèbre et jeux

Mercredi 14 mars 2018, 14 heures, 4033

**Joanna Ochremiak** (Université Denis Diderot - Paris 7) *Proof complexity, constraint satisfaction and graph isomorphism*

Logique, automates, algèbre et jeux

Mercredi 14 février 2018, 14 heures, 4033

**Joanna Ocremiak** (Université Denis Diderot - Paris 7) *Proof complexity, constraint satisfaction and graph isomorphism*

#### Année 2017

Logique, automates, algèbre et jeux

Jeudi 23 novembre 2017, 10 heures, 4033

**Nathanaël Fijlakow** (Turing Institute / CNRS) *Quasi-polynomial algorithms for parity games*

#### Année 2016

Logique, automates, algèbre et jeux

Jeudi 16 juin 2016, 10 heures 30, 4033

**Florent Capelli** (Liafa) *Lyndon’s theorem*

In this presentation, we will give a panorama of various classical preservation theorems for first-order logic. We will then present a proof of Lyndon’s theorem, and a proof that it does not hold in the finite case (this last construction is a joint work with Arnaud Durant, Amélie Gheerbrant and Cristina Sirangelo).

Logique, automates, algèbre et jeux

Jeudi 4 février 2016, 10 heures 30, 4033

**Christoph Haase** (LSV) *A Survey on Classical and Novel Results on Presburger Arithmetic*

Logique, automates, algèbre et jeux

Jeudi 21 janvier 2016, 10 heures 30, 4033

**Christoph Haase** (LSV) *A Survey on Classical and Novel Results on Presburger Arithmetic*

Logique, automates, algèbre et jeux

Jeudi 7 janvier 2016, 10 heures 30, 4033

**Sylvain Schmitz** (LSV) *Ideals in VAS Reachability*

In this seminar, I will present the ideas behind the algorithms of Mayr, Kosaraju, and Lambert (the KLM algorithm) in the light of ideals of well-quasi-orders. The interest here is that ideals provide a semantics to the structures manipulated in the KLM algorithm, bringing some new understanding to its proof of correctness.

Joint work with Jérôme Leroux (LaBRI) presented at LICS’15; see http://arxiv.org/abs/1503.00745

#### Année 2015

Logique, automates, algèbre et jeux

Jeudi 17 décembre 2015, 10 heures 30, 4033

**Ranko Lazic** (Warwick university) *Rackoff’s Coverability Technique*

Joint work with Sylvain Schmitz presented at RP ’15; see https://hal.inria.fr/hal-01176755/.

Logique, automates, algèbre et jeux

Jeudi 3 décembre 2015, 10 heures 30, 2015

**Sylvain Schmitz** (LSV) *Ideals of Well-Quasi-Orders*

After defining ideals and establishing some of their properties, I will illustrate their use in a concrete setting. I will present some recent results by Czerwiński, Martens, van Rooijen, and Zeitoun (FCT’15) on the decidability of piecewise-testable separability in the light of ideals. This seminar is also a warm-up for the next seminar on reachability in vector addition systems.

Logique, automates, algèbre et jeux

Jeudi 12 novembre 2015, 10 heures 30, 2015

**Luc Segoufin** (LSV) *Abiteboul-Vianu theorem*

The most celebrated one is Fagin’s theorem linking the complexity class NP with the expressive power of existential second-order logic.

In this lecture we will study the Abiteboul-Vianu theorem saying that the separation of PTime and PSpace can be rephrased in terms of expressive powers of partial fixpoints versus least fixpoints.

Logique, automates, algèbre et jeux

Jeudi 5 novembre 2015, 10 heures 30, 2015

**Thomas Colcombet** (LIAFA) *“À la Bojańcyk” proof of limitedness*

In his recent LICS15 paper, Bojańczyk gave a much shorter and self-contained proof of the decidability of limitedness (and in fact also star-height). It relies on a reduction to finite games of infinite duration, and involves arguments of positionality of stragegies in quantitative games [C.&Löding08]. The topic of this talk is the presentation of this elegant proof.

The decidability of limitedness was already presented in the LAAG seminar (using the algebraic approach of stabilization monoids), but the proof here is entirely different.

Logique, automates, algèbre et jeux

Mercredi 1 juillet 2015, 10 heures, 4068

**Stefan Göller** (LSV) *Decidability of DPDA equivalence, part IV*

The main focus of these talks will be on the computational complexity of this problem. We will give a proof of Stirling’s result that DPDA equivalence is primitive recursive.

More precisely, we will present a recent paper by Jancar that shows that in case two DPDAs are inequivalent they can be distinguished by a word whose length is bounded by a tower of exponentials of elementary height.

As in Arnaud’s talk we will view DPDA equivalence in terms of trace equivalence of deterministic first-order grammars.

This talk aims at going hand-in-hand with Arnaud’s talk but is intended to be self-contained as well.

These talks will be completely self-contained and require no background knowledge.

Logique, automates, algèbre et jeux

Mercredi 17 juin 2015, 10 heures 30, 4068

**Stefan Göller** (LSV) *Decidability of DPDA equivalence, part III*

The main focus of these talks will be on the computational complexity of this problem. We will give a proof of Stirling’s result that DPDA equivalence is primitive recursive.

More precisely, we will present a recent paper by Jancar that shows that in case two DPDAs are inequivalent they can be distinguished by a word whose length is bounded by a tower of exponentials of elementary height.

As in Arnaud’s talk we will view DPDA equivalence in terms of trace equivalence of deterministic first-order grammars.

This talk aims at going hand-in-hand with Arnaud’s talk but is intended to be self-contained as well.

These talks will be completely self-contained and require no background knowledge.

Logique, automates, algèbre et jeux

Mercredi 3 juin 2015, 10 heures 30, 4068a

**Arnaud Carayol** (LIGM) *Decidability of DPDA equivalence, part II*

The aim of the talk is to present what seems to be the simplest self-contained proof of this result. We will present a proof based on the recent work of Petr Jancar which uses first-order grammars instead of deterministic pushdown automata. To keep the proof as simple as possible, we will present the proof giving two semi-decision procedures.

Logique, automates, algèbre et jeux

Mercredi 27 mai 2015, 10 heures 30, 4068a

**Arnaud Carayol** (LIGM) *Decidability of DPDA equivalence, part I*

The aim of the talk is to present what seems to be the simplest self-contained proof of this result. We will present a proof based on the recent work of Petr Jancar which uses first-order grammars instead of deterministic pushdown automata. To keep the proof as simple as possible, we will present the proof giving two semi-decision procedures.

Logique, automates, algèbre et jeux

Mercredi 15 avril 2015, 10 heures 30, 4067

**Nathanaël Fijalkow** (LIAFA) *Algorithmics Properties of Probabilistic Automata, part II*

The plan for this second session is:

- explain how to obtain a universally non-regular automaton (by adding one state to last time’s example),
- explain how to encode Minsky machines using bounded-error probabilistic automata, with two-way and one-way variants,
- explain how to encode probabilistic automata using only one random probabilistic transition,

show the decidability of two problems: the equivalence and the finiteness problem. Both proofs rely on one observation: the reals with the addition and the multiplication form a field, and some linear algebra.

Logique, automates, algèbre et jeux

Mercredi 1 avril 2015, 10 heures 30, 4068

**Nathanaël Fijalkow** (LIAFA) *The Naughty Side of Probabilistic Automata.*

In this talk, I will review some of the most important undecidability results, with new simplified constructions.

Logique, automates, algèbre et jeux

Mercredi 11 mars 2015, 10 heures 30, 4068

**Michał Skrzypczak** (LIAFA) *On topology in automata theory, Part II*

Logique, automates, algèbre et jeux

Mercredi 11 février 2015, 10 heures 30, 4068

**Michał Skrzypczak** (LIAFA) *On topology in automata theory, Part I*

During this talk I will introduce basic notions of topology and descriptive set theory focusing on the case of infinite words. I’ll say what is the Borel hierarchy and the Wadge order. Then I’ll show how these tools are related to automata theory. I’ll try to argue that even from purely automata theoretic point of view, it is possible to obtain new results and new proofs by referring to topological concepts.

Logique, automates, algèbre et jeux

Mercredi 28 janvier 2015, 10 heures 30, 4068

**Gabriele Puppis** (LABRI) *Non-determinism vs two-way.*

A classical result by Rabin and Scott shows that deterministic finite state automata are as expressive as their non-deterministic and two-way counterparts. The translation from two-way automata to one-way automata is easily seen to imply an exponential blowup in the worst case, even when one maps deterministic two-way models to non-deterministic one-way models. The converse translation, which is based on the subset construction and maps non-deterministic one-way automata to deterministic ones, also implies an exponential blowup. This latter translation, however, is not known to be optimal when one aims at removing non-determinism by possibly introducing two-wayness. In particular, the question of whether the exponential blowup is unavoidable in transforming non-determinism to two-wayness is open.

When one turns to models of transducers, some translations are not anymore possible. For example, one-way transducers (even those that exploit functional non-determinism) are easily seen to be less powerful than two-way transducers (even input-deterministic ones). A natural problem thus arises that amounts at characterizing the two-way transductions that can be implemented by one-way functional transducers. The latter problem was solved in recent paper by Filiot, Gauwin, Reynier, and Servais – however, some questions related to complexity remains open. Another interesting, but older, result by Hopcroft shows that functional non-determinism can be removed from two-way transducers, at the cost of an exponential blow-up. A similar transformation can be used to prove that two-way transducers are closed under functional composition.

#### Année 2014

Logique, automates, algèbre et jeux

Mercredi 17 décembre 2014, 10 heures 30, 4068

**Stefan Göller** (LSV) *Equivalence checking of infinite state systems: A couple of lower bounds*

Logique, automates, algèbre et jeux

Mercredi 3 décembre 2014, 10 heures 30, 4068

**Thomas Colcombet** (LIAFA) *Stabilization monoids and cost functions*

Logique, automates, algèbre et jeux

Mercredi 19 novembre 2014, 10 heures 30, 4068

**Thomas Colcombet** (LIAFA) *Decidability of Boundedness and Limitedness*

In this second part, we will establish the decidability of this second problem, following the ideas of Leung, Simon, and Kirsten.

Logique, automates, algèbre et jeux

Mercredi 5 novembre 2014, 10 heures 30, 4068

**Thomas Colcombet** (LIAFA) *The star-height problem and its link to boundedness and limitedness*

The goal of the first session is to present the famous (restricted) star-height problem, and show the first steps toward its resolution. The question is the following: given a regular language L and a non-negative integer k, can we decide whether L can bee represented as a regular expression of star-height (i.e., nesting of Kleene stars) at most k. This problem has been open for 25 years unit Hashiguchi provided a proof in a series of four paper, between 81 and 88. This proof is notoriously difficult, and the presentation here will be based on the ideas in the more modern, and much simpler, proof of Kirsten (2005).

The idea behind both these proofs is to reduce the original problem to a question of existence of bounds for a function computed by some specific forms of automata (distance automata, nested-distance desert automata, B-automata, …). This idea goes much beyond the scope of the star-height problem, and I will try to convey this idea through several examples.

Logique, automates, algèbre et jeux

Jeudi 10 avril 2014, 10 heures 30, 2014

**David Xiao** (LIAFA) *Une introduction aux graphes expandeurs*

Dans cet exposé nous présenterons les graphes expandeurs, leur(s) définition(s), quelques lemmes structurels fondamentaux, et quelques exemples de leur utilisation dans la dérandomisation. Nous esquisserons également la construction basée sur le produit zigzag.

Logique, automates, algèbre et jeux

Jeudi 27 mars 2014, 10 heures 30, 2014

**Michael Vanden Boom** (Oxford university) *Automata characterizations of WMSO*

In this talk, I will sketch the proofs showing the equivalence of WMSO and a form of automata called weak alternating automata. I will also prove Rabin’s characterization of WMSO: a language is weakly definable iff the language and its complement are recognizable by nondeterministic Büchi automata.

I will conclude by describing connections with recent work (joint with Thomas Colcombet, Denis Kuperberg, and Christof Löding) showing that given a Büchi automaton as input, it is decidable whether the language is definable in WMSO.

Logique, automates, algèbre et jeux

Jeudi 13 mars 2014, 10 heures 30, 2014

**Olivier Serre** (LIAFA) *Rabin theorem*

Hence, the structure of the talk will be as follows:

- Main definitions and examples : infinite trees, parity tree automata and regular tree languages
- Basic recalls on positional determinacy of two-player parity games on graphs (see previous LAAG seminar by Nathanaël Fijalkow)
- Acceptance game and emptiness game/test for parity tree automata
- Complementation of parity tree automata relying on positional determinacy and determinisation of automata on infinite words (see previous LAAG seminar).

I will assume no specific knowledge on automata nor games for that talk.

Logique, automates, algèbre et jeux

Samedi 1 mars 2014, 10 heures 30, 2014

**Nathanaël Fijalkow** (LIAFA) *Positional determinacy part II*

I will highlight the differences between the two approaches, and the applications of both techniques. In particular, I will explain why backward approaches naturally induce determinization procedures for automata over infinite words.

The talk will be self-contained, and in particular I will quickly recall all required definitions at the beginning.

Logique, automates, algèbre et jeux

Jeudi 6 février 2014, 10 heures 30, 2014

**Thomas Colcombet** (LIAFA) *Positional determinacy part I*

This is in preparation to the seminars after the holidays, that will aim at presenting the results on the monadic theory of the infinite binary tree.

#### Année 2013

Logique, automates, algèbre et jeux

Jeudi 19 décembre 2013, 10 heures 30, 4068

**Sylvain Schmitz** (LSV) *Complexity classes beyond elementary*

I plan to skim over the following topics:

- subrecursive hierarchies: these are functions and classes that allow to define rapidly-growing functions by recursion over ordinal indices,¡/li¿
- length function theorems for well-quasi-orders, which are the key combinatorial statements for the upper bounds of most of the non-elementary problems I will mention,¡/li¿
- the definition of fast-growing complexity classes and some easy properties.

The recent results will be taken from work together with S. Abriola, D. Figueira, S. Figueira, C. Haase, S. Haddad, and Ph. Schnoebelen.

Logique, automates, algèbre et jeux

Jeudi 28 novembre 2013, 10 heures 30, 4068

**Joël Ouaknine** (Oxford university) *Decision Problems for Linear Recurrence Sequences*

This is joint work with James Worrell.

Logique, automates, algèbre et jeux

Jeudi 7 novembre 2013, 10 heures 30, 4068

**Thomas Colcombet** (LIAFA) *Green’s relations and automata theory*

During this talk, I will present some of the key results concerning Green’s relations, emphasizing on how one can think about regular languages using them. I will also show how these can be used for deriving non-trivial automata related results (such as McNaughton’s determinization result, Schützenberger’s characterization of star-free languages, Simon’s factorization forest theorem, … though unfortunately I will not have time do to all these).

Logique, automates, algèbre et jeux

Jeudi 17 octobre 2013, 10 heures 30, 4068

**Arnaud Durand** (Université Denis Diderot - Paris 7) *How to count in weak formalisms?*

In this talk we will evocate these different methods and present a completely elementary (and constructive) approach to reprove uniformly all these results (based on an old paper with M. More and C. Lautemann). We will also review why some of these results cannot be extended.

Logique, automates, algèbre et jeux

Jeudi 13 juin 2013, 10 heures 30, 4068

**Łukasz Kaiser** (LIAFA) *Machine Learning Viewed by a Logician*

Logique, automates, algèbre et jeux

Jeudi 30 mai 2013, 10 heures 30, 4068

**Gabriele Puppis** (LABRI) *The Cost of Repairing Regular Specifications*

The presentation is based on joint works with Michael Benedikt, Cristian Riveros, Sławek Staworko, and Pierre Bourhis.

Logique, automates, algèbre et jeux

Jeudi 16 mai 2013, 10 heures 30, 4068

**Howard Straubing** (Boston college) *A New Proof of Simon’s Theorem, and Separation by Piecewise Testable Languages*

Logique, automates, algèbre et jeux

Jeudi 18 avril 2013, 10 heures 30, 4068

**Thomas Colcombet** (LIAFA) *Tree walking automata*

In this talk, we will cover several subjects related to tree walking automata, including, the separation properties (deterministic tree walking automata are strictly weaker than non-deterministic ones [BC06], which in turn are strictly weaker than regular languages [BC08]) and closure properties (under complementation in particular [MSS06]). We will also present the models of pebble automata and relate it to first-order logic with transitive closure [EH99]. We will conclude with the separation of this logic from monadic logic over finite trees [BSSS06,BS10].

Logique, automates, algèbre et jeux

Jeudi 4 avril 2013, 10 heures 30, 4068

**Achim Blumensath** (RWTH Aachen) *The Transduction Hierarchy and Definable Orderings*

Logique, automates, algèbre et jeux

Mercredi 20 mars 2013, 10 heures 30, 4068

**Christof Löding** (RWTH Aachen) *Definability of uniformisation and choice in monadic second order logic*

A consequence of this result is that MSO-definable relations of infinite trees cannot be uniformized in MSO (where a uniformization of a binary relation is a function that is a subset of the relation and has the same domain as the relation). One can also use the result to show that there are nondeterministic automata on infinite trees that are not equivalent to an unambiguous automaton, i.e., an automaton that has at most one accepting run for each input.

Logique, automates, algèbre et jeux

Jeudi 21 février 2013, 10 heures 30, 4068

**Christian Choffrut** (LIAFA) *Uniformization*

I will not give a survey, rather talk of what I know of the topic, which is mainly binary rational relations over finite and infinite words and some connected problems.

Logique, automates, algèbre et jeux

Jeudi 7 février 2013, 10 heures 30, 4068

**Thomas Colcombet** (LIAFA) *The construction of Safra*

Logique, automates, algèbre et jeux

Jeudi 17 janvier 2013, 10 heures 30, -

**Stefan Göller** (LSV) *Two lower bound techniques in formal verification*

Second, I will recall two classical results from complexity theory (i) PSPACE is serializable meaning roughly that for determining whether a word lies in a fixed PSPACE language one only needs to check if the yield (the leaf string) of the computation tree of an NP machine lies in a fixed regular language (ii) Converting a natural number in binary to its Chinese remainder representation is in NCˆ1. I plan to use these results for proving lower bounds for reachability problems and model checking problems for one-counter automata and timed automata, respectively.

#### Année 2012

Logique, automates, algèbre et jeux

Jeudi 20 décembre 2012, 10 heures 30, -

**Sam Van Gool** (LIAFA) *A topological proof of Gödel’s completeness theorem for first-order logic*

Logique, automates, algèbre et jeux

Jeudi 13 décembre 2012, 10 heures 30, -

**Colin Riba** (ENS Lyon) *A Model Theoretic Proof of Completeness of an Axiomatization of Monadic Second-Order Logic on Infinite Words*

Logique, automates, algèbre et jeux

Jeudi 14 juin 2012, 10 heures 30, -

**Frédéric Magniez** (LIAFA) *An Introduction to Communication Complexity*

Logique, automates, algèbre et jeux

Jeudi 31 mai 2012, 10 heures 30, -

**Thomas Colcombet** (LIAFA) *The collapse of monadic second order logic over countable linear orderings*

Logique, automates, algèbre et jeux

Jeudi 10 mai 2012, 10 heures 30, -

**Thomas Colcombet** (LIAFA) *The monadic theory of orderings*

Logique, automates, algèbre et jeux

Jeudi 3 mai 2012, 10 heures 30, -

**Michel De Rougemont** (LIAFA) *Games for Monadic Σ11 (EMSO) and probabilistic methods*

Logique, automates, algèbre et jeux

Jeudi 12 avril 2012, 10 heures 30, -

**Olivier Carton** (LIAFA) *Kamp's theorem*

Logique, automates, algèbre et jeux

Lundi 26 mars 2012, 10 heures 30, submarine

**Achim Blumensath** (LIAFA) *Stability theory*