On monday, at 2pm - UPEC CMC - Room P2-131

April 20, 2020


Arnaud de Mesmay (LIGM)


March 23, 2020


Barnaby Martin (Durham)


March 16, 2020

Infinite time computations and ranks in descriptive set theory

Philipp Schlicht (University of Bristol)

What happens when you let a Turing machine run for infinite time? This question has been studied for a very natural machine model, the infinite time Turing machines of Hamkins and Kidder. Of course these machines become more powerful as the length of computations increases. A series of works explains their precise power, in particular where they fit in the hierarchy of sets studied in descriptive set theory.

We study the question ‘given a set A and an infinite string w, how hard is it to determine whether w ∈ A?’ in the context of infinite time Turing machines. We interpret this as the time needed to decide membership in A. What is the supremum of countable decision times? We give precise answers to this and related questions.

Concepts analogous to halting and decision times are ubiquitous in descriptive set theory in the form of ranks. A fundamental example is the rank of a wellorder on the natural numbers. I will explain how our results also work for such ranks and give applications in descriptive set theory on the level of Π11 and Σ12 sets.

This is joint work in progress with Philip Welch and Merlin Carl.

March 9, 2020

Modular coinduction up-to for higher-order languages via first-order transition systems

Jean Marie Madiot (INRIA Paris)

The bisimulation proof method can be enhanced by employing ‘bisimulations up-to’ techniques. A comprehensive theory of such enhancements has been developed for first-order (i.e., CCS-like) labelled transition systems (LTSs) and bisimilarity, based on abstract fixed-point theory and compatible functions. We transport this theory onto languages whose bisimilarity and LTS go beyond those of first-order models. The approach consists in exhibiting fully abstract translations of the more sophisticated LTSs and bisimilarities onto the first-order ones. This allows us to reuse directly the large corpus of up-to techniques that are available on first-order LTSs. The only ingredient that has to be manually supplied is the compatibility of basic up-to techniques that are specific to the new languages. We investigate the method on the π-calculus, the λ-calculus, and a (call-by-value) λ-calculus with references.

This is a new version of a previous work, joint work with Damien Pous and Davide Sangiorgi, upgraded with shiny new tools in coinduction.

March 2, 2020

Un algorithme stochastique pour résoudre les jeux stochastique simples

David Auger (Université de Versailles)

The best algorithm so far for solving Simple Stochastic Games is Ludwig’s randomized algorithm [Ludwig, 1995] which works in expected 2^{O(sqrt{n})} time. We first give a simpler iterative variant of this algorithm, using Bland’s rule from the simplex algorithm, which uses exponentially less random bits than Ludwig’s version. Then, we show how to adapt this method to the algorithm of Gimbert and Horn [Gimbert and Horn, 2008] whose worst case complexity is O(k!), where k is the number of random nodes. Our algorithm has an expected running time of 2^{O(k)}, and works for general random nodes with arbitrary outdegree and probability distribution on outgoing arcs.

February 24, 2020

Décider (ℝ,+,<,1) dans (ℝ,+,<,ℤ)

Alexis Bes (LACL - UPEC)

La structure (R,+,<,Z), où R désigne l'ensemble des réels et Z le prédicat unaire "être un entier", admet l'élimination des quantificateurs et est décidable. Elle intervient notamment dans le domaine de la spécification et la vérification de systèmes hybrides. Elle peut être étudiée via les automates, en considérant des automates de Büchi qui lisent des réels représentés dans une base entière fixée. Boigelot et al. ont démontré en particulier que la classe des relations définissables dans (R,+,<,Z) coïncide avec celle des relations reconnaissables par automate en toute base. Une autre structure intéressante est (R,+,<,1), qui est moins expressive que (R,+,<,Z) mais définit les mêmes relations bornées. On présente une caractérisation topologique des relations définissables dans (R,+,<,Z) qui sont définissables dans (R,+,<,1), et on en déduit que le problème de savoir si une relation définissable dans (R,+,<,Z) est définissable dans (R,+,<,1) est décidable.
Travail en commun avec Christian Choffrut.

February 3, 2020

Network Inference: Graph reconstruction and verification

Hang Zhou (LIX - Polytechnique)

How efficiently can we find an unknown graph using shortest path queries between its vertices? This is a natural theoretical question from the standpoint of recovery of hidden information. This question is related to discovering the topology of Internet networks, which is a crucial step for building accurate network models and designing efficient algorithms for Internet applications.

In this talk, I will introduce the problems of graph reconstruction and verification via oracles. I will investigate randomized algorithms based on a Voronoi cell decomposition. I will also analyze greedy algorithms, and prove that they are near-optimal.

The talk is based on joint work with Claire Mathieu and Sampath Kannan.