Postponed to a date TBA.

One of the most fascinating phenomena in game theory is the Braess paradox, which occurs when adding an additional route to a network leads to increased congestion and travel times for everyone. In this talk, after introducing some basic concepts and presenting the paradox, I will describe a few other scenarios in which improving the productivity of individuals counter-intuitively leads to degraded group productivity.

Ontology-mediated query answering (OMQA) is a promising approach to data access and integration that has been actively studied in the knowledge representation and database communities for more than a decade. The vast majority of work on OMQA focuses on conjunctive queries, whereas more expressive queries that feature counting or other forms of aggregation remain largely unexplored. We introduce a general form of counting conjunctive query (CCQ), relate it to previous proposals, and study the complexity of answering such queries in the presence of ontologies expressed in the description logic ALCHI or its sublogics. As the general case of CCQ answering is intractable and often of high complexity over such ontologies, we consider two practically relevant restrictions, namely rooted CCQs and Boolean atomic CCQs, for which we establish improved complexity bounds.

Graph databases are now playing an important role because they allow us to overcome some limitations of relational databases. In particular, graph databases differ from relational databases in that the topology of data is as important as the data itself. Thus, typical graph database queries are navigational, asking whether some nodes are connected by paths satisfying some specific properties.

While relational databases were designed upon logical and algebraic foundations, the development of graph databases has been quite ad-hoc. In this sense, the aim of this paper is to provide them with some logical foundations. More precisely, in previous work we introduced a navigational logic, called GNL (Graph Navigational Logic) that allows us to describe graph navigational properties, and which is equipped with a deductive tableau method that we proved to be sound and complete.

In this presentation we will introduce a new formal model for property graphs. Then, we will show how graph queries à la Cypher can be expressed using a fragment of GNL, defining for them a logical and an operational semantics, based on the inference rules for GNL. Finally, we show that both semantics are equivalent.

Zoom meeting registration link

YouTube live stream

Event logs are often one of the main sources of information to understand the behavior of a system. While numerous approaches have extracted partial information from event logs, we aim at inferring a global model of a system from its event logs.

We consider real-time systems, which can be modeled with Timed Automata: our approach is thus a Timed Automata learner. There is a handful of related work, however, they might require a lot of parameters or produce Timed Automata that either are undeterministic or lack precision. In contrast, we propose an approach, called TAG, that requires only one parameter and learns, without any a-priori knowledge, a deterministic Timed Automaton having a good tradeoff between accuracy and automata complexity. This allows getting an interpretable and accurate global model of the considered real-time system. Experiments compare our approach to related work and demonstrate its merits.

In the context of large-scale networks, fault tolerance is a necessity. Self-stabilization is an algorithmic approach to fault tolerance in distributed systems. Its aim is to manage processors' memory corruption due to transient failures. The efficiency of a self-stabilizing algorithm is characterized by several parameters, including (1) the time taken by the system to return to a legal configuration after an arbitrary corruption of its processors' memory, and (2) the memory space used by the processors to execute the algorithm. Minimizing memory space is motivated by many aspects, such as networks (e.g. sensor networks) with limited memory space, minimizing data exchanges between processors, and limiting information storage to use redundancy techniques. This seminar will present self-stabilization through two main classical problems: constructing spanning trees, especially those of minimum weight, and electing a leader. It will cover the links between self-stabilization and distributed decision techniques, including computing lower bounds on memory space needed to solve the aforementioned problems using self-stabilizing algorithms.

Starting from Doeblin's observation on the Poissonian nature of occurrences of large digits in typical continued fraction expansions, I will outline some recent work on rare events in measure preserving systems (including spatiotemporal and local limit theorems) which, in particular, allows us to refine Doeblin's statement in several ways.

(Part of this is joint work with Max Auer.)

Cut-reduction procedures for classical sequent calculus are notoriously non-deterministic and non-confluent, both in the original formulation by Gentzen and in later reformulations. It is natural to ask whether those instances of non-confluence are superficial in nature, i.e. whether syntactically distinct normal forms of the same derivation are in fact correlated in a non-trivial way, as is the case in the intuitionistic and linear versions of sequent calculus. A famous counter-example by Lafont purports to show that the answer is negative, that is, every interpretation of derivations in LK that is invariant under classical cut-elimination must be a trivial one that identifies at least all proofs of the same sequent. A long-standing open question has then been whether it could be possible to work around Lafont's example by natural and non-trivial adjustments of the calculus and/or of cut-reduction steps, without resorting to symmetry-breaking techniques like polarization or embeddings into intuitionistic or linear logic.

Working within the propositional fragment of the context-sharing formulation of LK — where parallel logical rules permute freely — we show that the graph constructed by tracing the history of atomic formula occurrences through axiom and cut rules is invariant under arbitrary rule permutations in cut-free proofs, thus providing a canonical representation of normal-form proofs.

We then introduce a refinement of the notion of axiom-induced graph that allows extending the invariance result to proofs with cuts, although at the cost of a strong assumption on the shape of derivations. Because cut-reduction in this formulation of LK can be implemented entirely by logical rule permutations plus a pair of local rewriting steps that preserve the refined axiom graphs, the result yields a non-trivial invariant of cut-reduction.

The problem of reconfiguring independent sets belongs to the broader field of combinatorial reconfiguration problems. It can be formulated as follows: given a collection of tokens placed on the vertices of an independent set of a graph, is it possible to move one by one these tokens to another target independent set, such that two tokens are never neighbors throughout the transformation? After a general introduction to combinatorial reconfiguration and the independent set reconfiguration problem, we will focus on the “Token Sliding” variant. In this variant, one step of the transformation consists in moving a token from a vertex to a neighboring vertex. We will focus on the parameterized complexity of this problem in sparse classes of graphs and on the new tools we have recently designed for the development of FPT algorithms.

Dans cet exposé très informel à propos d'un travail en cours, je souhaiterais discuter de différents styles pour définir (en Coq) la sémantique d'un langage de programmation. Une de mes motivations est d'obtenir une sémantique au moins partiellement exécutable dans Coq et d'en tirer un mécanisme d'exécution symbolique qui pourrait être exploité dans un système de vérification de programmes.

Au cours de l'exposé, je présenterai deux styles de sémantique (pour un langage sans effets de bord, hormis divergence et plantage), et au-dessus de chacun d'eux, je construirai une logique de Hoare. Le premier style, “monadique jusqu'au bout”, reproduit des idées que l'on trouve dans la littérature: un premier interprète est exprimé dans une monade libre bien choisie, puis, dans un second temps, les habitants de cette monade sont traduits dans d'autres monades (monade des interaction trees; monade de spécification). Le second style, “à pas amples”, est hybride: dans une couche inférieure, on conserve le même interprète monadique, exprimé dans la monade libre; dans une couche supérieure, on raisonne à l'aide d'une sémantique opérationnelle à petits pas. J'aimerais recevoir des commentaires et suggestions du public afin de prévoir les prochaines étapes: ajout du non-déterminisme, du parallélisme, de l'état mutable, puis construction d'une logique de programmes de la famille Iris.