Novembre 2018 — Intelligence Artificielle

« Décompositions et résolution de modèles graphiques » par C. Terrioux (LIS)
« Argument-based logics » par L. Amgoud (IRIT)
« Au coeur des démonstrateurs SAT » par G. Audemard (CRIL)

Orateur : Cyril Terrioux , LIS
Titre : Décompositions et résolution de modèles graphiques

Résumé : La notion de décomposition arborescente est, de nos jours, un sujet majeur pour l’étude théorique et la résolution pratique de problèmes NP-complets et au-delà. En intelligence artificielle, son utilisation est des plus prometteuses notamment dans le cadre des modèles graphiques (réseaux de contraintes, réseaux bayésiens, logique propositionnelle, …).

Dans cet exposé, nous illustrerons d’abord comment la décomposition arborescente peut être exploitée, d’un point de vue théorique, pour définir des classes polynomiales. Ensuite, nous nous intéresserons aux méthodes de calcul de décompositions arborescentes. Enfin, nous verrons quel peut-être l’apport de la décomposition arborescente pour la résolution pratique des instances.


Orateur : Leila Amgoud, IRIT
Titre : Argument-based logics
Résumé : Argumentation is a reasoning process based on the justification of claims by arguments. Due to its explanatory power, it has become a hot topic in Artificial Intelligence, and has been used for solving different problems including decision making under uncertainty, learning rules, modelling different types of dialogs, and more importantly reasoning about inconsistent information.
In this talk, I will focus on argument-based paraconsistent logics. Starting from a knowledge base encoded in a logical language, an argument-based logic defines arguments (supporting conclusions) and identifies conflicts between them. Then, it evaluates the strength of each arguments using what is called semantics in the argumentation literature. Finally, it infers conclusions that are supported by strong arguments. I will present two families of such logics: the family that uses extension semantics and the one that uses ranking ones for the evaluation of arguments. I discuss the outcomes of both families and compare them. I also compare the argumentation approach with other well-known paraconsistent logics.


Orateur : Gilles Audemard, CRIL
Titre : Au coeur des démonstrateurs SAT
Résumé : Aujourd’hui, les solveurs SAT se trouvent au coeur de nombreux domaines de recherche. Nous commencerons par une présentation des ingrédients essentiels des solveurs SAT. Ensuite, nous présenterons l’utilisation incrémentale des démonstrateurs SAT, c’est à dire l’appel multiple de solveurs sur des instances proches les unes des autres. Nous introduirons quelques exemples d’utilisation incrémentale de SAT. Enfin, nous ferons une petite analyse des compétitions SAT qui ont lieu tous les ans.

Septembre 2018 — Modèles de Calcul et Complexité

« Quantum control flow » par B. Valiron (LRI)
« Natural computing models of unusual complexity » par A.E. Porreca (LIS)
« Computability in closure spaces » par E. Jeandel (LORIA)

Orateur : Benoit Valiron (http://www.monoidal.net), CentralSupelec, LRI
Titre : Quantum control flow
Résumé : One perspective on quantum algorithms is that they are classical algorithms having access to a special kind of memory with exotic properties. This perspective suggests that, even in the case of quantum algorithms, the control flow notions of sequencing, conditionals, loops, and recursion are entirely classical. There is however, another notion of control flow, that is itself quantum. The notion of quantum conditional expression is reasonably well-understood: the execution of the two expressions becomes itself a superposition of executions. The quantum counterpart of loops and recursion is however not believed to be meaningful in its most general form. In this talk, using a detour through reversible computing we discuss how a reasonable notion of quantum loops and recursion is indeed possible.


Orateur : A.E. Porreca, LIS
Titre : Natural computing models of unusual complexity


Orateur : E. Jeandel, LORIA
Titre : Computability in closure spaces

Juin 2018 — Algorithmes et Structures Discrètes

« Hybrid tractable classes » par M. Cooper (IRIT)
« On Rationality of Nonnegative Matrix Factorization » par M. Shirmohammadi (LIS)
« Tout réseau hyperbolique a un coeur » par V. Chepoi (LIS)

Orateur : Martin Cooper, l’IRIT
Titre : Hybrid tractable classes
Résumé : The CSP (constraint satisfaction problem) is a generic problem over finite domains in which each constraint is a relation and a list of variables (its scope). Given the NP-completeness of the CSP, it is natural is to look for restrictions of the problem that allow polynomial-time solving. The two classical approaches consist in studying restrictions either on the language of relations or on the hypergraph defined by the constraint scopes. After 30 years of effort, dichotomies have been established for these two approaches. A third avenue consists in defining classes of CSP instances by forbidding patterns (generic sub-problems). This hybrid approach has led to the discovery of several new polynomial classes. I will present the state of the art in the characterization of forbidden patterns that define polynomial classes.


Orateur : Mahsa Shirmohammadi (LIS AMU, new MCF)
Titre : On Rationality of Nonnegative Matrix Factorization

Résumé : Nonnegative matrix factorization (NMF) is the problem of decomposing a given nonnegative n×m matrix M into a product of a nonnegative n×d matrix W and a nonnegative d×m matrix H. A longstanding open question, posed by Cohen and Rothblum in 1993, is whether a rational matrix M always has an NMF of minimal inner dimension d whose factors W and H are also rational. We answer this question negatively, by exhibiting a matrix for which W and H require irrational entries.

In this talk, we further exhibit a connection between Cohen and Rothblum’s question with a question posed by Paz, in his seminal 1971 textbook. The latter question asks, given a probabilistic automaton (PA) with rational transition probabilities, does there always exist a minimal equivalent PA that also has rational transition probabilities? The PA and its minimal equivalent PA accept all finite words with equal probabilities. We use the established connection to answer Paz’s question negatively, thus falsifying a positive answer claimed in 1974.
(This talk is based on two papers in ICALP 2016 and SODA 2017.)


Orateur : Victor Chepoi (LIS AMU)
Titre : Tout réseau hyperbolique a un coeur (ou « hyperbolicité pour tous »)

Résumé : In the first part of the talk, we will introduce Gromov hyperbolicity and recall several characterizations of delta-hyperbolic geodesic metric spaces and graphs. 

In the second part, we investigate the impact the negative curvature has on the traffic congestion in large-scale networks. We prove that every Gromov hyperbolic network G admits a core, thus answering in the positive a conjecture by Jonckheere, Lou, Bonahon, and Baryshnikov, Internet Mathematics, 7 (2011) which is based on the experimental observation by Narayan and Saniee, Physical Review E, 84 (2011)  that real-world networks with small hyperbolicity have a core congestion. Namely, we prove that for every subset X  of n vertices of a graph G with delta-thin geodesic triangles  there exists a vertex m of G such that the ball B(m,4delta)  of radius 4delta centered at m intercepts at least one half of the total flow between all pairs of vertices of X, where the flow between two vertices x,y of  X is carried by geodesic (or quasi-geodesic) (x,y)-paths.  We show that the point m can be constructed in the following way: take a median point m* of X (a point minimizing the sum of distances to the points of X) in the injective hull of G and then a closest to m* point in G. In the third part of the talk, (and if the time will permit), we will describe a simple factor 8 approximation algorithm for optimal hyperbolicity of an n-vertex graph in optimal O(n^2) time (assuming that the input is the distance matrix of the graph). 

The talk is based on the papers 
[1] V. Chepoi, F. Dragan, and Y. Vaxès, Core congestion is inherent in hyperbolic networks, SODA 2017, <http://arxiv.org/abs/1605.03059>
[2] J. Chalopin, V. Chepoi, F. Dragan, G. Ducoffe, A. Mohammed, and Y. Vaxès, <https://arxiv.org/abs/1803.06324> Fast approximation and exact computation of negative curvature parameters of graphs, SoCG 2018, <https://arxiv.org/abs/1803.06324>

Mars 2018 — Géométrie et Topologie du Calcul

« Homologie algorithmique pour les objets discrets » par A. Gonzales-Lorenzo (LIRIS)
« Topological and algorithmic tools for computability in distributed computing » par D. Imbs (LIS)
« Un contre-exemple à la conjecture de Thiagarajan sur les structures d’évènements régulières » par J. Chalopin (LIS)

Orateur : Aldo Gonzales-Lorenzo (post-doc LIRIS)
Titre : Homologie algorithmique pour les objets discrets

Résumé : La théorie de l’homologie formalise la notion de trou dans un espace. Pour un sous-ensemble de l’espace Euclidien, on définit une séquence de groupes d’homologie, dont leurs rangs sont interprétés comme le nombre de trous de chaque dimension. Ainsi, β0 (le rang du groupe d’homologie de dimension zéro) est le nombre de composantes connexes, β1 est le nombre de tunnels ou anses et β2 est le nombre de cavités. Ces groupes sont calculables quand l’espace est décrit d’une façon combinatoire, comme c’est le cas pour les complexes simpliciaux ou cubiques. À partir d’un objet discret (un ensemble de pixels, voxels ou leur analogue en dimension supérieure) nous pouvons construire un complexe cubique et donc calculer ses groupes d’homologie.

Dans cette présentation je parlerai de deux approches relatives au calcul de l’homologie sur des objets discrets. Primo, je présenterai le champ de vecteurs discret homologique, une structure combinatoire qui permet de calculer les groupes d’homologie. Secundo, je présenterai deux mesures (l’épaisseur et la largeur) associées aux trous d’un objet discret, ce qui permet d’obtenir une signature topologique et géométrique plus intéressante que les simples nombres de Betti.


Orateur : Damien Imbs (LIS AMU, new MCF)
Titre : Topological and algorithmic tools for computability in distributed computing

Résumé : One of the major breakthroughs in distributed computing was the discovery of its links with algebraic topology. This result earned its authors the Gödel prize in 2004. Topological tools are especially useful to prove impossibility results.

In this talk, I will present such topological tools and how to use them to prove the impossibility of distributed problems. In particular, I will show how to use Sperner’s Lemma to prove the impossibility of Set Agreement, a fundamental distributed problem, in a specific model. I will then present algorithmic techniques to extend this result to various distributed models of computation.


Orateur : Jeremie Chalopin (LIS AMU)
Titre : Un contre-exemple à la conjecture de Thiagarajan sur les structures d’évènements régulières
Résumé : On présente un contre-exemple à la conjecture de Thiagarajan (1996 et 2002) affirmant que les structures d’évènements régulières correspondent exactement à celles obtenues comme dépliages des réseaux de Petri 1-safe finis. Les structures d’évènements, les automates de trace sont des modèles fondamentaux pour la théorie de la concurrence. Il existe des interprétations élégantes de ces structures comme des objets combinatoires et géométriques, et on peut reformuler la conjecture dans ce cadre. Plus précisément, les domaines des structures d’évènements correspondent exactement aux graphes médians pointés et aux complexes cubiques CAT(0) pointés. Une condition nécessaire pour que la conjecture de Thiagarajan soit vérifiée est que les domaines des structures d’évènements régulières admettent un joli étiquetage régulier (regular nice labelling). Pour réfuter cette conjecture, on décrit le domaine d’une structure d’évènement régulière qui n’admet pas de tel étiquetage. Notre contre-exemple est basé sur une construction de Wise (1996 et 2007) d’un complexe de carrés de courbure non-positive dont le revêtement universel est un complexe de carrés CAT(0) contenant un plan muni d’un pavage apériodique.

Février 2018 — Logique et Méthodes Formelles

« When type theory meets model-checking » par C. Grellois (LIS)
« Programs as formulas » par M. Cristia (U. N. Rosario)
« On The Complexity of Resource-Bounded Logics » par S. Demri (LSV)

Orateur : Charles Grellois (LIS)
Titre : When type theory meets model-checking
Résumé : Type theory and model-checking are two formal methods, aiming at ensuring the correctness of programs. In type theory, the idea is to annotate the instructions of the program with the properties they satisfy, so as to statically control how they will evolve during the computation, and to conclude that the program is correct — or not. In model-checking, one typically abstracts the program as a mathematical model, as a graph for instance, representing an approximation of its behavior. Then, an appropriate logical formula is devised over this program, and an algorithm checks automatically whether the abstract model satisfies the requirement. In the analysis of functional programs, higher-order constructions are possible: one can define functions that themselves take functions as inputs. Type theory is particularly useful to analyze such situations, as I will explain during the talk. I will first give a brief idea of what model-checking is, then explain what are the basics of type theory, and in a third time show how they where combined by Kobayashi in 2009 to perform model-checking of functional programs. If time allows, I will spend the last minutes giving an overview of the research I did in the last years building up on Kobayashi’s work and its extension by Kobayashi and Ong.


Orateur : Maximiliano Cristia (U. N. Rosario)
Titre : Programs as formulas (not as proofs)
Résumé : After the Curry-Howard correspondence and the type theories developed in the past decades, it emerged the idea of programs as proofs (of their properties). That is, if we have a proof P of a theorem T, we can make P a program whose type is T. This theory was a major breakthrough in programming language design and software verification. However, in this talk, I’ll show you an alternative and, in some sense, previous view: programs as formulas. In other words, let’s make the very formula to be a program; that is, we don’t need to make a proof to have a program. In particular I’m going to show {log} (setlog), which is a programming language but also an automated theorem prover. In {log} formulas are programs, and programs are formulas. We can use the same tool and the same language to specify programs, to simulate these specifications, to generate test cases and to prove properties of them. {log} works with formulas over the theory of finite sets, which allows for the specification of large classes of programs.


Orateur : Stephane Demri (LSV)
Titre : On The Complexity of Resource-Bounded Logics
Résumé : We characterise the complexity of model-checking problems for resource-bounded logics by taking advantage of recent results on decision problems for alternating VASS. For instance, we show that the model-checking problem for the logic RBATL is 2EXPTIME-complete and we establish that for RBATL* the problem remains decidable. A parameterised version of the logics is also discussed. This is a joint work with Natasha Alechina, Nils Bulling and Brian Logan.