Juin 2023 — Intelligence Artificielle

Speaker : Liva Ralaivola ( Criteo AI Lab)
Title : Differentially-Private Sliced Wasserstein Distance
Abstract: Developing machine learning methods that are privacy preserving is today a central topic of research, with huge practical impacts. Among the numerous ways to address privacy-preserving learning, we here take the perspective of computing the divergences between distributions under the Differential Privacy (DP) framework — being able to compute divergences between distributions is pivotal for many machine learning problems, such as learning generative models or domain adaptation problems. Instead of resorting to the popular gradient-based sanitiziation method for DP, we tackle the problem at its roots by focusing on the Sliced Wasserstein Distance and seamlessly making it differentially private. Our main contribution is as follows: we analyze the property of adding a Gaussian perturbation to the intrinsic randomized mechanism of the Sliced Wasserstein Distance, and we establish the sensitivity of the resulting differentially private mechanism. One of our important finding is that this DP mechanism transforms the Sliced Wasserstein distance into another distance, that we call the Smoothed Sliced Wasserstein Distance. This new differentially-private distribution distance can be plugged into generative models and domain adaptation algorithms in a tranparent way, and we empirically show that it yields highly competitive performance compared with gradient-based DP approaches from the literature, with almost no loss in accuracy for the domain adaptation problems that we consider. (Joint work with A. Rakotomamonjy, Criteo AI Lab)

Speaker : Van-Giang Trinh (LIS)
Title : Efficient enumeration of fixed points in complex Boolean networks using answer set programming
Abstract: Boolean Networks (BNs) are an efficient modeling formalism with applications in various research fields such as mathematics, computer science, and more recently systems biology. One crucial problem in the BN research is to enumerate all fixed points, which has been proven crucial in the analysis and control of biological systems. Indeed, in that field, BNs originated from the pioneering work of R. Thomas on gene regulation and from the start were characterized by their asymptotic behavior: complex attractors and fixed points. The former being notably more difficult to compute exactly, and specific to certain biological systems, the computation of stable states (fixed points) has been the standard way to analyze those BNs for years. However, with the increase in model size and complexity of Boolean update functions, the existing methods for this problem show their limitations. To our knowledge, all the state-of-the-art methods for the fixed point enumeration problem rely on Answer Set Programming (ASP). Motivated by these facts, in this work we propose two new efficient ASP-based methods to solve this problem. We evaluate them on both real-world and pseudo-random models, showing that they vastly outperform four state-of-the-art methods as well as can handle very large and complex models.

Avril 2023 : Complexité et Modèles de Calculs

Speaker : Sebastien Tavenas ( LAMA, Université de Savoie Mont-Blanc)
Title : SuperPolynomial lower bounds for circuits of constant depth
Any multivariate polynomial P(X_1,…,X_n) can be written as a sum of monomials, i.e., a sum of products of variables and constants of the field. The natural size of such an expression is the number of monomials. But, what happens if we add a new level of complexity by considering expressions of the form: sum of products of sums (of variables and constants)? Now it becomes less clear how to show that a given polynomial has no small expression. In this talk we will solve exactly this problem. More precisely, we prove that some explicit polynomials do not have polynomial-sized sum-of-products-of-sums (SPS) representations. We can also obtain similar results for SPSPs, SPSPSs, etc. for all expressions of constant depth. We will see also why this problem can be seen an important step for obtaining lower bounds on the size of algebraic circuits.

Speaker : Antonio E. Porreca (CANA, LIS)
Title : The algebra of alternation and synchronisation of finite dynamical systems
Many phenomena of scientific and engineering interest can be modelled as finite dynamical systems, that is, as deterministic transition functions iterated over an abstract set of states. Dynamical systems can be put together (or, from the opposite point of view, analysed) in terms of composition operations, among which two of the most basic ones are alternative and synchronous execution. These give rise to a commutative semiring (a “ring without subtraction”) over dynamical systems up to isomorphism, with some rather complex algebraic properties, notably the lack of unique factorisation into irreducibles. Several interesting decomposition properties can then be expressed in terms of polynomial equations. We discuss computability and complexity issues in solving these equations (most interesting cases are intractable, and the general problem is undecidable), as well as some properties of irreducible systems and the (possible) existence of prime ones.

Speaker : Cameron Calk (Postdoc, LIS)
Title : Coherence via rewriting in higher Kleene algebras.
Squier’s coherence theorem and its generalisations provide a categorical interpretation of contracting homotopies via confluent and terminating rewriting. In particular, this approach relates standardisation to coherence results in the context of higher dimensional rewriting systems. On the other hand, modal Kleene algebras (MKAs) have provided a description of properties of abstract rewriting systems, and classic (one-dimensional) consistency results have been formalised in this setting.
In this talk, I will recall the notion of higher Kleene algebra, introduced as an extension of MKAs, and which provide a formal setting for reasoning about (higher dimensional) coherence proofs for abstract rewriting systems. First, I will briefly discuss how rewriting techniques are captured in MKAs before showing how these techniques may be extended to higher dimensions.

Février 2023 — Algorithmique et Structures Discrètes

Speaker : Bernadette Charron-Bost ( DIENS )
Title : Distributed Computation of the Average.
Abstract: Computing the average of initial values in a multi-agent system is a fundamental problem in distributed control theory. Unfortunately, an impossibility result by Boldi and Vigna shows that deterministic, anonymous agents communicating by broadcast cannot compute functions dependent on the multiplicity of the input values. In particular, they cannot compute the average of their initial values.
I will first recall the proof developed by Boldi and Vigna using the theory of graph fibrations, and will then review various approaches for circumventing the impossibility result of computing the average. I will notably present a randomized algorithm that computes the average in linear time in the size $n$ of the network, but only with high probability. I will also present a deterministic algorithm, inspired by the popular Metropolis-Hasting method in statistical physics, that computes the average in $O(n^4)$ rounds, under the additional assumption of bidirectional links.
(Joint work with Patrick Lambein-Monette.)

Speaker : Oscar Defrain (LIS – ACRO team)
Title : Minimal dominating sets enumeration in bipartite graphs.
Abstract : Minimal dominating sets enumeration has gained considerable attention since it has been shown equivalent to the long-standing open problem of dualizing a pair of monotone Boolean functions, i.e., deciding whether two positive CNF and DNF are equal. This result, obtained by Kanté, Limouzy, Mary and Nourine in 2014, holds even in the very restricted case of co-bipartite graphs (the vertex set of the graph may be partitioned into two cliques), and was strengthened by a tractable result on split graphs (the vertex set may be partitioned into a clique and an independent set). This has left the case of bipartite graphs (the vertex set may be partitioned into two independent sets) at the center of the attention in the subsequent years. We show it to be tractable inspired by a technique by Eiter, Gottlob and Makino from 2003.
(This is a joint work with Marthe Bonamy, Marc Heinrich, Michał Pilipczuk, and Jean-Florent Raymond.)

Speaker : Pablo Concha Vega (LIS – CANA team)
Title : On the Complexity of Stable and Biased Majority.
Abstract: A majority automata is a two-state cellular automata, where each cell updates its state according to the most represented state in its neighborhood. A question that naturally arises in the study of these dynamical systems asks whether there exists an efficient algorithm that can be implemented in order to compute the state configuration reached by the system at a given time-step. This problem is called the prediction problem. In this work, we study the prediction problem for a more general setting in which the local functions can be different according to their behavior in tie cases. We define two types of local rules: the stable majority and biased majority. The first one remains invariant in tie cases, and the second one takes the value 1. We call this class the heterogeneous majority cellular automata (HMCA). For this latter class, we prove that in two or more dimensions, the problem is P-Complete as a consequence of the capability of the system of simulating Boolean circuits.

December 2022 – Géométrie et topologie du calcul

Orateur : Mathieu Desbrun (website), GeomeriX team, Inria/Ecole Polytechnique

Titre : Exploiting the unreasonable effectiveness of geometry in computing

Résumé : While the fields of geometric design and numerical simulation have mostly evolved independently, we are now witnessing a convergence of thought: from isogeometric analysis, to geometric integrators and discrete exterior calculus, it has been repeatedly noted that the quality of computational tools ultimately boil down to properties of a fundamentally geometric or topological nature. This talk will describe a brief overview of our approach to computing through the lens of geometry to offer a versatile and efficient toolbox for a variety of applications, from shape processing to tangent vector field editing, and from fluid simulation to non-linear dimensionality reduction if time allows. We will point out how a strong grasp of classical differential geometry paired with a good understanding of the typical computational constraints in research and industry can bring forth novel theoretical and practical foundations for general-purpose computations. The importance of preserving differential geometric notions in the discrete setting will be a recurring theme throughout the talk to demonstrate the value of a geometric approach to computations.

Mathieu Desbrun, GeomeriX team, Inria/Ecole PolytechniqueBio: After obtaining a PhD in computer graphics in Grenoble, France, Desbrun joined Caltech as a postdoctoral fellow in 1998. He joined the CS department at the University of Southern California as an Assistant Professor in January 2000, where he remained for four years in charge of the GRAIL lab. He then became an Associate Professor at Caltech in the CS department in 2003, where he started the Applied Geometry lab and was awarded the ACM SIGGRAPH New Researcher award. He took on administrative duties after he became a full professor, becoming the founding chair of the Computing + Mathematical Sciences department and the director of the Information Science and Technology initiative from 2009 to 2015. More recently, he has been the Technical Papers Chair for the ACM SIGGRAPH 2018 conference, spent a sabbatical year at ShanghaiTech in the School of Information Science and Technology, and was elected as ACM Fellow in 2020. He is now working at LIX as both an advanced researcher at Inria Saclay, and a Professor at Ecole Polytechnique. He started the Geomerix research team with three local colleagues to focus on geometric numerics, covering data analysis, machine learning, and simulation.

Orateur : Aldo González Lorenzo (webpage), LIS

Titre :  A Heuristic for Short Homology Basis of Digital Objects

Résumé : Finding the minimum homology basis of a simplicial complex is a hard problem unless one only considers the first homology group. In this talk, we introduce a general heuristic for finding a short homology basis of any dimension for digital objects (that is, for their associated cubical complexes) with complexity $\mathcal{O}(m^3 + \beta_q \cdot n^3)$, where $m$ is the size of the bounding box of the object, $n$ is the size of the object and $\beta_q$ is the rank of its q-th homology group. Our heuristic makes use of the thickness-breadth balls, a tool for visualizing and locating holes in digital objects. We evaluate our algorithm with a data set of 3D digital objects and compare it with an adaptation of the best current algorithm for computing the minimum radius homology basis by Dey, Li and Wang.

Orateur : Yann-Situ, LIS

Titre : Étude d’objets homologiques computationnels

Résumé : En géométrie algorithmique, de nombreux travaux ont pour objectif d’analyser, comprendre ou classifier des formes. En raison de ses propriétés computationnelles, l’homologie constitue un descripteur topologique intéressant. En effet, il est possible de calculer un grand nombre d’informations homologiques à partir d’une représentation discrète d’objets (complexes de chaîne, complexes simpliciaux…). Il existe diverses méthodes de calcul homologique, fournissant des informations plus ou moins complexes et pertinentes. Nous introduirons ainsi plusieurs objets mathématiques associés à ces informations homologiques. Nous discuterons de leurs différences, leurs propriétés calculatoires, leurs relations d’un point de vue théorique et nous présenterons certaines pistes de recherche.

November 2022 – Logique et méthodes formelles

Orateur : Olga Kouchnarenko (website, scholar), femto-st & INRIA Lille, project team SPIRALS
Titre :  Testing Dynamic Reconfigurations of Component-based Systems w.r.t. Adaptation Policies
Résumé : Component systems are designed as sets of components that may reconfigure themselves according to adaptation policies. Adaptation policies are seen as artifacts that describe desirable behavior of the system without enforcing a specific one. An adaptation policy is designed as a set of rules that indicate, for a given set of configurations, which reconfiguration operations can be triggered, with  fuzzy values representing their respective utility. 
In this context, we present a model-based testing approach which aims to generate large test suites in order to measure the occurrences of reconfigurations and compare them to their utility values specified in the adaptation rules. This process is based on a usage model of the system used to stimulate the system and provoke reconfigurations. As the system may reconfigure dynamically, this online test generator observes the system responses and evolution in order to decide the next appropriate test step to perform. In the end, the relative frequencies of the reconfigurations are measured in order to determine if the adaptation policy is faithfully implemented. The approach is illustrated by simulations for platoons of (semi-)autonomous vehicles.

Orateur : Rim Saddem ( scholar), LIS, equipe Mofed
Titre :  Business Processes Meet Spatial Concerns: the sBPMN Verification Framework.
Résumé : BPMN is the standard for business process modeling. It includes a rich set of constructs for control-flow, inter-process communication, and time-related concerns. However, spatial concerns are left apart while being essential to several application domains. We propose a comprehensive extension of BPMN to deal with this. Our proposal includes an integrated notation, a first-order logic semantics of the extension, and tool-supported verification means through the implementation of the semantics in TLA+. Our tool support and our model database are open-source and freely available online.

Orateur : Julie Parreaux ( website), LIS, equipe Move
Titre :  Playing Stochastically in Weighted Timed Games to Emulate Memory.
Résumé : Weighted timed games are two-player zero-sum games played in a timed automaton equipped with integer weights. We consider optimal
reachability objectives, in which one of the players, that we call Min, wants to reach a target location while minimising the
cumulated weight. While knowing if Min has a strategy to guarantee a value lower than a given threshold is known to be undecidable (with two or more clocks), several conditions, one of them being the divergence, have been given to recover decidability. In such weighted timed games (like in untimed weighted games in the presence of negative weights), MinPl may need finite memory to play (close to) optimally. This is thus tempting to try to
emulate this finite memory with other strategic capabilities. In this work, we allow the players to use stochastic decisions, both in the choice of transitions and of timing delays. We give for the first time a definition of the expected value in weighted timed games, overcoming several theoretical challenges. We then show that, in divergent weighted timed games, the stochastic value is indeed equal to the classical (deterministic) value, thus proving that Min can guarantee the same value while only using stochastic choices, and no memory. This work is join with Benjamin  Monmege and Pierre-Alain Reynier.

Juin 2022 — Intelligence Artificielle

Orateur : Joao Marques-Silva (website, scholar), IRIT ANITI
Titre : Logic-Based Explainability in Machine Learning
Résumé : The forecast applications of machine learning (ML) in high-risk and safety-critical applications hinge on systems that are robust in their operation and that can be trusted. This talk gives a broad overview of ongoing efforts in applying logic-enabled automated reasoning tools for explaining black-box ML models. The talk details the computation of rigorous explanations for the predictions black-box models, and illustrates how these serve to assess the quality of widely used heuristic explanation approaches. The talk also overviews properties relating different kinds of rigorous explanations. Finally, the talk briefly overviews a number of emerging topics of research in formal explainability.

Orateur : Stéphane Grandcolas, LIS
Titre : WRM: a metaheuristic algorithm for ship weather routing
Résumé : In recent years ship weather routing has attracted a lot of interest, resulting of the significant increase of transport by sea. The primary objective is to limit the costs, but other parameters, such as time, safety or preservation of the environment, can also be considered. These aspects and the fact that the domains of the variables are continuous make the problem difficult to solve. We propose a metaheuristic algorithm called WRM (for Weather Routing Metaheuristic) that aims at finding routes of minimal cost within a given time period. The cost can be the fuel oil consumption, the amount of greenhouse gas emissions or any other measure. It depends on the weather conditions that are expected and on the speed of the vessel, which can vary all along the route. Constraints forbidding or penalizing the navigation in specific conditions or in some given areas can be easily enforced. The method is simple and general. It converges progressively towards the most promising regions, generating new potential way points which are not derived from a predefined mesh. Simulating the fuel oil consumption of the vessel according to the expected wind and waves conditions, we have performed experimentations that show the efficiency of the approach.

Orateur : Matthieu Py, LIS
Titre : Production de certificats pour le problème Max-SAT
Résumé : Dans cet exposé, on s’intéresse à la production de certificats pour le problème de satisfiabilité maximum. Le problème de satisfiabilité maximum, ou problème Max-SAT, consiste, étant donnée une formule propositionnelle sous forme normale conjonctive, à trouver comment affecter à chaque variable de la formule une valeur booléenne afin de satisfaire le plus de clauses possible, ou, de manière équivalente, de falsifier le moins de clauses possible. Les travaux présentés portent sur la génération de certificats d’optimalité pour le problème Max-SAT, c’est à dire, non seulement être en capacité de donner le nombre minimum de clauses devant être falsifiées, mais produire en plus une preuve d’optimalité de la valeur trouvée.

Pour produire de tels certificats, on s’intéresse d’abord à une première problématique qui est l’adaptation des réfutations par résolution en max-réfutations. Une réfutation par résolution est un certificat d’insatisfiabilité d’une formule, autrement dit c’est une preuve qu’un ensemble de clauses ne peut être satisfait. Ces réfutations par résolution sont très utiles dans le cadre du problème SAT, mais sont inutilisables dans le cadre du problème Max-SAT. En effet, si exhiber une réfutation par résolution d’une formule permet bien de démontrer qu’il est toujours nécessaire de falsifier au moins une clause de la formule, exhiber dix réfutations par résolution d’une même formule ne permet pas de démontrer qu’il est toujours nécessaire de falsifier au moins dix clauses. Il est donc nécessaire d’adapter ces réfutations par résolution pour qu’elles soient utilisables dans le cadre de Max-SAT. Ces réfutations par résolution, adaptées pour Max-SAT et appelées max-réfutations, formeront un maillon essentiel des certificats pour le problème Max-SAT.

Grâce aux travaux portant sur l’adaptation des réfutations par résolution en max-réfutation, on montrera comment générer des certificats pour le problème Max-SAT. Pour cela, on fait itérativement appel à un oracle SAT pour calculer une réfutation par résolution de la formule courante, puis on transforme cette réfutation en max-réfutation et l’applique sur la formule courante. Ce processus est répété jusqu’à ce que la formule courante devienne satisfiable, et l’ensemble des max-réfutations calculées plus l’interprétation permettant de satisfaire la dernière formule calculée forment un certificat pour le problème Max-SAT. Ainsi, pour démontrer que l’optimum Max-SAT d’une formule est de satisfaire 40 clauses d’une formule possédant 50 clauses, on pourra calculer et exhiber 10 max-réfutations (afin de démontrer qu’il est nécessaire de falsifier au moins 10 clauses) et exhiber une interprétation satisfaisant la formule obtenue après application des 10 max-réfutations (afin de démontrer qu’il est possible de falsifier exactement 10 clauses).

Mai 2022 — Complexité et Modèles de calculs

Cette demi-journée aura lieu le 5 mai à Luminy, en salle 04.05 du TPR2, à 10h.

Orateur : Édouard Bonnet
Titre : Graph decompositions and their algorithms
Résumé : Through simple examples, we take a representative glimpse at forty years of using width parameters for algorithmic purposes. The talk will be biased towards revisiting this history through the lens of contraction sequences, which are at the basis of the recently introduced twin-width. 

Orateur : Karoliina Lehtinen
Titre : Un peu de non-déterminisme peut aller loin: un aperçu des automates déterministes en histoire
Résumé : Le non-déterminisme permet surement à votre modèle d’automate préféré plus expressif, ou du moins plus succinct que le déterminisme. Cela se fait généralement au au prix d’une complexité algorithmique plus importante. Les classes d’automates intermédiaires, entre déterministes et non-déterministes, présentent des compromis intéressants en ce qui concerne l’expressivité, la succincté et les propriétés algorithmiques.

Les automates déterministes en histoire sont des automates non-déterministes dans lesquels les choix non-déterministes peuvent être faits sans connaître le futur du mot d’entré. Ils combinent une partie de la succincté et de l’expressivité des automates non déterministes avec certaines des propriétés algorithmiques utiles des automates déterministes. En particulier, les jeux avec des conditions gagnantes données par des automates déterministes en histoire ont tendance à être plus simples à résoudre que les jeux dont les conditions de gain sont non-déterministes.

Dans cet exposé, je donnerai une vue d’ensemble des automates déterministes en histoire, de leur relation avec divers problèmes de synthèse et des développements récents dans le domaine pour différentes classes d’automates.

Orateur : Nathan Lhote
Titre : Minimisation des transductions rationnelles
Résumé : La notion d’automate minimal (ou de monoïde syntaxique) fournit pour les langages réguliers un objet canonique qui capture beaucoup de propriétés intrinsèques d’un langage. Par exemple le théorème de Schützenberger nous dit qu’un langage est définissable en logique du premier ordre FO[<] si et seulement si son automate minimal est sans compteur. Depuis de nombreux résultats similaires ont été obtenus, faisant des liens entre expressivité dans une certaine logique et propriété de l’automate minimal.

Un transducteur est un automate équipé de sorties. Contrairement au cas des langages, les transducteurs ne sont pas toujours déterminisables. Pour les transducteurs, il n’existe certes pas d’automate minimal mais on montre qu’il existe un nombre fini de bimachines (modèle de calcul introduit par Schützenberger et étudié par Eilenberg) qui capturent (dans le même sens que l’automate minimal pour les langages) les propriétés d’une transduction.

Janvier 2022 — Algorithmique et Structures Discrètes

Cette demi-journée aura lieu le 20 janvier sur zoom.

Orateur : Alessia Milani (LIS)
Titre : Concurrent Counters with Polylogarithmic Step Complexity
Résumé : Shared data objects are an essential abstraction in distributed computing, as they provide a consistent interface for multiple processes to interact via shared data. Linearizability is the main consistency criterion that formalizes the correctness of shared object implementations. Linearizable shared objects are intuitive to use, but they can be expensive to implement. 

In this talk, I will consider a widely-used shared object, the counter. I will present a fundamental lower bound on the worst-case complexity of fault-tolerant implementations of counters and two ways of circumventing it. In particular,  in 2000, Jayanti, Tan and Toueg proved a linear lower bound on the worst-case step complexity of obstruction-free implementations, from read and write operations, of a large class of shared objects, including counters. In 2012, Aspnes, Attiya and Censor-Hillel observed that the lower bound holds only when numerous operations are applied to the object and does not rule out the possibility of obtaining algorithms whose step complexity is sub-linear when the number of operations is bounded. 

We recently prove that there exists deterministic counters implementations with sub-linear amortized step complexity regardless of how many operations are performed on the object. This is a joint work with Mirza Ahad Baig, Danny Hendler and Corentin Travers 

The talk will be self-contained.

Orateur : Eloi Perdereau (LIS)
Titre : Accords Approchés et Asymptotiques pour les Adversaires de Message
Résumé : En calculabilité des systèmes distribués, les problèmes du Conensus et de l’Accord k-Ensembliste sont beaucoup étudiés car permettent de mettre en valeur des aspects fondamentaux des modèles. L’objet de notre travail est de proposer et d’étudier des relaxations du problème de l’Accord k-Ensembliste, sous l’angle de l’approximation géométrique de valeurs, à l’instar du Consensus Approché. Nous proposons deux nouveaux problèmes : l’Accord k-Convexe Approché et l’Accord k-Convexe Asymptotique, et étudions leur calculabilité pour des algorithmes de moyennes.

Le modèle distribué est celui des adversaires de message qui se base sur des séquences de graĥes dynamiques définissant les exécutions. Les scénarios considérés sont clos par suffixes et ont des comportements de récurrence bornée soit par l’apparition des arcs (BRec et FRec), soit par l’influence de certains sommets sur les autres (BISC et FISC). Ces adversaires forment une hiérarchie de fait et nous allons montrer que ces deux problèmes permettent de les séparer du point de vue de la calculabilité distribuée.

Novembre 2021 — Géométrie et Topologie du Calcul

Cette demi-journée pôle calcul aura lieu le 18 novembre. Nous aurons la chance d’avoir trois orateurs.

Orateur : Dmitry Sokolov (LORIA)
Titre : How to compute locally invertible maps
Résumé : Mapping a triangulated surface to 2D plane (or a tetrahedral mesh to 3D space) is the most fundamental problem in geometry processing. The critical property of a good map is a (local) invertibility, and it is not an easy one to obtain. We propose a mapping method inspired by the mesh untangling problem. In computational physics, untangling plays an important role in mesh generation: it takes a mesh as an input, and moves the vertices to get rid of foldovers. In fact, mesh untangling can be considered as a special case of mapping, where the geometry of the object is to be defined in the map space and the geometric domain is not explicit, supposing that each element is regular. This approach allows us to produce locally invertible maps, which is the major challenge of mapping. In practice, our method succeeds in very difficult settings, and with less distortion than the previous work, both in 2D and 3D.

Orateur : Corentin Travers (LABRI)
Titre : Synchronous t-Resilient Consensus in Arbitrary Graphs
Résumé : We study the number of rounds needed to solve consensus in a synchronous network G where at most t nodes may fail by crashing. This problem has been thoroughly studied when G is a complete graph, but very little is known when G is arbitrary. We define a notion of radius that considers all ways in which t nodes may crash, and present an algorithm that solves consensus in radius rounds. Then we derive a lower bound showing that our algorithm is optimal for vertex-transitive graphs, among oblivious algorithms.

Our lower bound technique is inspired by the topological techniques for distributed computing. It is similar to the connectivity analysis of the protocol complex, the structure of states at the end of executions of an algorithm after a certain number of rounds. However, instead of working with the protocol complex, we consider an information flow directed graph version based on failure patterns.

Joint work with Armando Castaneda, Pierre Fraigniaud, Ami Paz, Sergio
Rajsbaum, and Matthieu Roy

Orateur : Victor Chepoi (LIS)
Titre : 1-safe Petri nets and special cube complexes
Résumé : In the talk, I will explain the following bijection between 1-safe Petri nets and finite special cube complexes: the event structures arising as unfolding of 1-safe Petri nets are exactly the event structures whose domains arise as principal filters of the universal cover of a finite 1-safe Petri net.

This can be viewed as a positive answer to the (disproved) conjecture by Thiagarajan that the event structures arising as unfolding of 1-safe Petri nets are exactly the regular event structures. If the time permits, I will give some (positive and negative) applications of this bijection.

Joint work with Jérémie Chalopin.

Octobre 2021 — Logique et méthodes formelles

Le 14 octobre à la FRUMAM – de 9h30 à 12h30.

Orateur : Ugo Dal Lago (UniBo)
Titre : On Higher-Order Cryptography
Résumé : Type-two constructions abound in cryptography: adversaries for encryption and authentication schemes, if active, are modeled as algorithms having access to oracles, i.e. as second-order algorithms. But how about making cryptographic schemes higher-order themselves? Moreover, how about seeing cryptographic reductions as higher-order functions? We give an answer to this question, by first describing why higher-order cryptography is interesting as an object of study, and then showing how the concept of probabilistic polynomial time algorithm can be generalised so as to encompass algorithms of order strictly higher than two. We then prove some positive and negative results about the existence of higher-order cryptographic primitives, namely authentication schemes and pseudorandom functions. The talk is based on some joint work with Boaz Barak and Raphaëlle Crubillé.

Orateur : Pierre Clairambault (LIS)
Titre : Games with no Winner: an Introduction to Game Semantics
Résumé : How to define rigorously the behaviour of programs under execution?
Program semantics is a necessary first step in order to prove that a program or program transformation is correct, and is of course a preliminary to any theoretical question on programming languages. Game semantics is one of many approaches to program semantics. It represents a program by recording the exchange of observable computational events with its execution environment, phrased as a play in a two-player game that the program plays with its context. In game semantics there is no winner: it is about the journey, not the destination!

Most of my talk will be an introduction to game semantics. I will first focus on some old (but nice) results, namely the so-called « semantic cube » following which game semantics exactly captures the observable behaviour of programs with various computational effects (notably, mutable state and non-local control). I will show how this allows one to prove results about computational effects and their interferences.

Time permitting, I will then talk about some of my own recent work on a game semantics for concurrent programs. The semantics builds on so-called « true concurrency » models such as event structures, and provides a causal description of the behaviour of concurrent programs with rich computational features.

Orateur : Raphaelle Crubillé (LORIA)
Titre : Sémantique dénotationelle pour les languages de programmation probabilistes
Résumé : La sémantique dénotationelle est un champs de recherche centré sur la construction de modèles mathématiques des languages de programmation, visant à produire des techniques de preuve pour l’équivalence de programmes. Dans les dix dernières années, l’usage des probabilités pour la programmation a été transformé par les dévelopements en programmation statistique et en apprentissage, ce qui a stimulé un intérêt renouvelé pour les méthodes formelles pour des languages probabilistes. Cet exposé présente un bref panorama de la sémantique dénotationelle des langages de programmation probabilistes, en tentant d’expliciter à la fois ses enjeux, ses outils et ses perspectives.