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.

Mai 2021– Intelligence artificielle

« Vector-valued Prediction with RKHSs and Hard Shape Constraints  » par Zoltan Szabo (Polytechnique)

Date : 20 mai 2021
Orateur : Zoltan Szabo
Titre : Vector-valued Prediction with RKHSs and Hard Shape Constraints
Résumé : Abstract: Shape constraints (such as non-negativity, monotonicity, convexity, or supermodularity) provide a principled way to encode prior information in predictive models with numerous successful applications in econometrics, finance, biology, reinforcement learning, and game theory. Incorporating this side information in a hard way (for instance at all points of an interval) however is an extremely challenging problem. We propose a unified and modular convex optimization framework to encode hard affine SDP constraints on function derivatives into the flexible class of vector-valued reproducing kernel Hilbert spaces (RKHS). The efficiency of the technique is illustrated in the context of joint quantile regression (analysis of aircraft departures), convoy localization, safety-critical control (piloting an underwater vehicle while avoiding obstacles), and econometrics (learning of production functions). This is joint work with Pierre-Cyril Aubin-Frankowski. Preprint:

Mars 2021 — Calcul et Complexité

« Computations with ordinary differential equations  » par Olivier Bournez (Polytechnique)

Date : 25 mars 2021
Orateur : Olivier Bournez
Titre : Computations with ordinary differential equations
Résumé : Computability, complexity, programming, continuous time computations, old and recent analog models of computations: Why ordinary differential equations are fun and a pleasant way to do computer science in 2020. Olivier et ses co-auteurs François Fages, Guillaume Le Guludec et Amaury Pouly, ont reçu le prix 2019 du journal La Recherche pour leurs travaux sur les modèles de calcul analogiques et en particulier l’article Strong Turing Completeness of Continuous Chemical Reaction Networks and Compilation of Mixed Analog-Digital Programs.

Février 2021 — Géométrie et Topologie du Calcul

« Introduction aux Algèbres Géométriques et leur aspects calculatoires » par Vincent Nozick (Université Eiffel)

Date : 18 février 2021
Orateur : Vincent Nozick
Titre : Introduction aux Algèbres Géométriques et leur aspects calculatoires
Résumé : Les Algèbres Géométriques constituent un ensemble d’outils intuitifs permettant de créer et de manipuler des objets géométriques. Longtemps entre les mains des mathématiciens, les informaticiens commencent à se les approprier et à entrevoir leur potentiel. Cet exposé s’inscrit dans cette démarche d’explication simple et commencera par une introduction sur les fondements de ces algèbres, à savoir les vecteurs, les multivecteurs ainsi que quelques produits sur ces multivecteurs. Nous verrons ensuite comment les utiliser pour résoudre efficacement et très simplement des problèmes de géométrie, en portant une attention particulière sur l’aspect calculatoire.