IRIF members and visitors are asked to comply with the COVID-19 Directives of CNRS and Université de Paris.

IRIF, the Research Institute on the Foundations of Computer Science, is a research laboratory of CNRS and Université de Paris, also hosting one Inria project-team.

The research conducted at IRIF is based on the study and understanding of the foundations of all computer science, in order to provide innovative solutions to the current and future challenges of digital sciences.

IRIF hosts about 200 people. Six of its members have been distinguished by the European Research Council (ERC), five are members of the Institut Universitaire de France IUF), two are members of the Academia Europæa, and one is member of Académie des sciences.

22.1.2021
IRIF is associated to two projects selected under the call “Émergence en Recherche” of Université de Paris: IDiLL, co-instigated by Michele Pagani with LIPN, and SPECTRANS by Jean-Baptiste Yunès with CLILLAC-ARP and LIPADE.

22.1.2021
French president Emmanuel Macron has presented a national plan for quantum technologies, including some aspects of quantum computing and communications. This is based on a parliamentary report co-written by Iordanis Kerenidis. More from CNRS including a special edition on the quantum revolution.

15.1.2021
V. Berthé (IRIF) & J. Barral spearhead the creation of 𝘎𝘋𝘙 Multifractal analysis and self-similarity as a renewal of `GDR Multifractal analysis' with a move towards symbolic dynamic systems.

4.1.2021
P. Fraigniaud (IRIF), F. Le Gall (Nagoya University), H. Nishimura (Nagoya University), and A. Paz (Universität Wien) will present at ITCS 2021 a quantum approach of distributed certification, for checking the consistency of large data sets replicated at several nodes of a network.

5.1.2021
Geoffroy Couteau (IRIF), Pooya Farshim (University of York), and Mohammad Mahmoody (University of Virginia) will present at ITCS 2021 a new framework for proving black-box separations in cryptography in a composable way.

4.1.2021
Frédéric Magniez (IRIF CNRS member) holds the 2020–2021 chair on Computer Science at Collège de France (in partnership with Inria), where he will present a course on Quantum Algorithms.

(These news are displayed using a randomized-priority ranking.)

Enumerative and analytic combinatorics
Wednesday January 27, 2021, 10:30AM, Virtuelle
Franz Lehner (TU Graz) To be announced.

Proofs, programs and systems
Thursday January 28, 2021, 10:30AM, Online
Jérôme Feret (INRIA) Conservative approximation of systems of polymers

We propose a systematic approach to approximate the behavior of models of polymers with synthesis and degradation. Our technique consists in discovering time-dependent lower and upper bounds for the concentration of some quantities of interest. These bounds are obtained by approximating the state of the system by a hyper-box,. The evolution of the position of each hyper-face is defined by the means of differential equations which are obtained by pessimistically bounding the derivative with respect to the corresponding coordinate on this hyper-face.

The over-approximation of each derivative relies on symbolic reasoning. We use Kappa to describe our models. Kappa is a site-graph rewriting languages which is popular to describe protein-protein interaction networks. The main ingredients of Kappa, graph patterns, can be interpreted in two ways. Intensionally by the means of embeddings between graphs, or extensionally as the (potentially infinite) multi-sets of the complete graphs they occur in. This second interpretation leads to the definition of positive series of concentration of species. Interestingly, it can be proven that some universal constructions between graphs induce generic methods to prove the well-posedness of some numerical series, and some equality and inequality among them, hence providing a convenient tool-kit for symbolic reasoning

PhD defences
Thursday January 28, 2021, 3PM, Online
Léonard Guetta (IRIF) Homology of strict omega-categories

The objective of this thesis is to compare the homology of the nerve of an ω-category, invariant coming from the homotopy theory of strict ω-categories, with its polygraphic homology, invariant coming from higher rewriting theory. More precisely, we prove that both homologies generally do not coincide and call homologically coherent the particular strict ω-categories for which polygraphic homology and homology of the nerve do coincide. The goal pursued is to find abstract and concrete criteria to detect homologically coherent ω-categories.

Automata
Friday January 29, 2021, 2:30PM, Salle 3052
Stefan Göller (University of Kassel) Bisimulation Finiteness of Pushdown Systems Is Elementary

It is shown that if a pushdown system is bisimulation equivalent to a finite system, there is already such a finite system whose size is elementary in the description size of the pushdown system. As a consequence, it is elementarily decidable if a pushdown system is bisimulation-finite. This is joint work with Pawel Parys.TBA

Graph Transformation Theory and Applications
Friday January 29, 2021, 3PM, (online)
Leen Lambers & Fernando Orejas (Hasso-Plattner-Institut Potsdam, Germany & Technical University of Catalonia (UPC), Spain) Confluence of Graph Transformation

Confluence has been studied for graph transformation since several decades now. Confluence analysis has been applied, for example, to determining uniqueness of model transformation results in model-driven engineering. It is strongly related to conflict analysis for graph transformation, i.e. detecting and inspecting all possible conflicts that may occur for a given set of graph transformation rules. The latter finds applications, for example, in software analysis and design. Both conflict and confluence analysis rely on the existence and further analysis of a finite and representative set of conflicts for a given set of graph transformation rules.

Traditionally, the set of critical pairs has been shown to constitute such a set. It is representative in the sense that for each conflict a critical pair exists, representing the conflict in a minimal context, such that it can be extended injectively to this conflict (M-completeness). Recently, it has been shown that initial conflicts constitute a considerably reduced subset of critical pairs, being still representative in a slightly different way. In particular, for each conflict there exists a unique initial conflict that can be extended (possibly non-injectively) to the given conflict (completeness). Compared to the set of critical pairs, the smaller set of initial conflicts allows for more efficient conflict as well as confluence analysis.

We continue by demonstrating that initial conflicts (critical pairs) are minimally complete (resp. minimally M-complete), and thus are both optimally reduced w.r.t. representing conflicts in a minimal context via general (resp. injective) extension morphisms. We proceed with showing that it is impossible to generalize this result to the case of rules with application conditions (equivalent to FOL on graphs). We therefore revert to a symbolic setting, where finiteness and minimal (M-)completeness can again be guaranteed. Finally, we describe important special cases (e.g. rules with negative application conditions), where we are able to obtain minimally complete (resp. M-complete) sets of conflicts in the concrete setting again.

Verification
Monday February 1, 2021, 11AM, BBB link
François Schwarzentruber (IRISA, ENS Rennes) Connected multi-agent path finding

Motivated by the increasing appeal of robots in information-gathering missions, we study multi-agent path planning problems in which the agents must remain interconnected. We model an area by a topological graph specifying the movement and the connectivity constraints of the agents. In the first part of the talk, we study the theoretical complexity of the reachability and the coverage problems of a fleet of connected agents. We also introduce a new class called sight-moveable graphs which admit efficient algorithms. In the second part, we re-visit the conflict-based search algorithm known for multi-agent path finding, and define a variant where conflicts arise from disconnections rather than collisions.

Graphs
Tuesday February 2, 2021, 2PM, Salle 1007
Zhouningxin Wang Density of $C_{-4}$-critical signed graphs

By extending the notion of indicator to signed graphs, we show the problem of $4$-coloring is captured by the problem of $C_{-4}$-coloring (mapping signed graphs to a negative $4$-cycle). Moreover, we extend the notion of $H$-critical to $(H, \pi)$-critical. In this talk, we prove that any $C_{-4}$-critical signed graph on $n$ vertices, except for one particular signed bipartite graph on $7$ vertices and $9$ edges, must have at least $4n/3$ edges. As an application to planarity, we conclude that every signed bipartite planar graph of negative girth at least $8$ admits a homomorphism to $C_{-4}$ and show that this bound is the best possible, which is relevant to a bipartite analog of Jaeger-Zhang conjecture.