Un polynôme est hyperbolique si toutes ses racines sont réelles. Un système polynomial est dit hyperbolique positif si toutes ses solutions complexes sont réelles et appartiennent à l'orthant positif. Lors de cet exposé, nous allons décrire une construction combinatoire de tels systèmes qui s'applique à un grand nombre de familles connues de polytopes. (basé sur un travail en commun avec Pierre-Jean Spaenlehauer, CR Inria Nancy).
Travail en collaboration avec Arkady Leiderman, Ben Gurion University, Beer-Sheva, Israel. Un espace topologique $L$ est un espace ordonnable lorsqu'il existe un ordre total $leq$ sur $L$ tel que la topologie sur $L$ est engendrée par les intervalles ouverts (non nécessairement bornés) à extrémités dans $L$ (exemples: $N$, $Z$, $Q$, $R$; contre-exemple: $C$). Un espace $L$ est un espace héréditairement ordonnable si toute image continue de $L$ est ordonnable. On montre le résultat suivant: Si $L$ est un espace héréditairement ordonnable alors $L$ est un espace dénombrable et compact (i.e. un sous-espace compact de $R$, qui est donc homéomorphe a un ordinal dénombrable ayant un plus grand élément). En fait on montre un résultat plus général.
Bisimulation is used in concurrency theory as a proof method for establishing behavioural equivalence of processes. Up-to techniques are a means of enhancing this proof method. In this talk I will argue that up-to techniques can be of general use, and discuss how this is supported by our coalgebraic framework of up-to techniques, that provides enhanced proof techniques for a wide variety of systems and a wide variety of properties. I will discuss our recent work on extending this framework to cover equivalences for systems that involve silent transitions.
On étudie les complexifications topologiquement minimales du plan affine euclidien R² à isomorphisme près et à difféomorphismes birationnels près. Un faux plans réel est une surface géométriquement intègre non singulière définie sur R telle que : • Le lieu réel S(R) est difféomorphe à R²; • La surface complexe S_C(C) a le type d’homologie rationnelle de A²_C(C).; • S n’est pas isomorphe à A²_R en tant que surface définie sur R. L’étude analogue dans le cas compact, c’est-à-dire la classification des complexifications du plan projectif réel P²(R) possédant l’homologie rationnelle du plan projectif complexe est bien connue : P²_C est l’unique telle complexification. Nous prouvons que les faux plans réels existent en donnant plusieurs exemples et nous abordons la question : existe-t-il un faux plan réel S tel que S(R) n’est pas birationnellement difféomorphe à A²_R(R) ? (Travail en commun avec Adrien Dubouloz.) Deux articles à ce sujet : http://arxiv.org/abs/1507.01574 (soumis) et ``Real frontiers of fake planes'', European Journal of Math, DOI 10.1007/s40879-015-0087-8 (2015).
Dans ce travail en collaboration avec François Delarue (Nice) et Nicolas Vauchelet (Paris 6), nous étudions l'ordre d'approximation du schéma décentré amont pour le transport conservatif (équation de continuité) en dimension d'espace quelconque, sur maillage cartésien, pour des champs de vitesse lipschitziens à droite. La difficulté est que ces champs de vitesse peuvent être discontinus et qu'en conséquence les solutions sont des mesures. L'analyse du caractère bien posé repose sur les travaux de Filippov pour les équations différentielles, et de Poupaud et Rascle pour les EDP, dont nous utilisons les outils et les résultats. Notre analyse est basée sur une interprétation probabiliste de l'algorithme (déterministe), dont nous montrons qu'il est l'espérance d'un algorithme aléatoire (ce travail est l'extension d'un résultat obtenu avec François Delarue il y a quelques années pour des champs de vitesse lipschitziens sur maillages quelconques).
Le traitement catégorique de la théorie des probabilités formulé par Giry et Lawvere, basé sur la monade de probabilité G, permet de manipuler de façon élégante des probabilités d'ordre supérieur. Dans ce cadre, je présenterai une reconstruction du processus de Dirichlet, un objet largement utilisé en inférence bayésienne. Ce processus prend la forme d'une famille de mesures dans GG(X) indexée par M(X), où X est un espace Polonais et M(X) est l'espace des mesures finies non-zéro sur X. Sa construction repose sur deux outils dont l’intérêt dépasse le simple cas de la construction de Dirichlet. Le premier de ces outils est une version fonctorielle du théorème d'extension de Bochner adapté au cadre Polonais, qui permet d'étendre une famille projective de probabilités en une probabilité limite. Le second outil est une méthode de ``décomposition'' qui associe à tout espace Polonais zéro-dimensionnel une famille projective d'espaces finis, dont la limite projective est une compactification de l'espace originel. La combinaison de ces deux outils avec des propriétés bien connues de Dirichlet sur les espaces finis nous permet de reconstruire Dirichlet comme une transformation naturelle de M vers GG. Cette construction améliore les précédentes en ce qu'elle prouve la continuité de Dirichlet en ses paramètres.
PML est un langage de programmation en appel par valeurs similaire à ML, avec une syntaxe à la Curry (c'est à dire, pas de types dans les termes) et basé sur une logique d'ordre supérieur classique. Les termes apparaissent dans les types via un prédicat d'appartenance t ∈ A et un opérateur de restriction A | t ≡ u. La sémantique de ces deux constructeurs de types utilise une relation d'équivalence (observationnelle) sur les programmes (non typés). L'opérateur de restriction est utile pour l'écriture de spécifications tandis que l'appartenance permet d'encoder les types dépendants. La présence de l'équivalence nous permet également de relâcher la « value restriction » pour obtenir un type produit dépendant compatible avec la logique classique (ce qui n'avait pas été fait avant).
La théorie des jeux à champ moyen a été initée par Lasry et Lions il y a une dizaine d'années. Le but est de décrire le comportement asymptotique d'équilibres de Nash sur une grande population de joueurs en interaction champ moyen. Dans ce cadre, très peu de critères sont connus pour garantir l'unicité des équilibres asymptotiques. Inspirés par la théorie des EDO et EDS, nous posons ici la question du rétablissement de l'unicité par randomisation des solutions.
We call a closed basic semialgebraic subset X of R^n homogeneous if it is defined by a finite system of strict inequalities with homogeneous polynomials. We prove an effective version of the Putinar and Vasilescu Positivstellensatz for positive homogeneous polynomials on homogeneous semialgebraic sets.
L'espace des arcs centrés en un point donné d'une variété a une structure de cône, qui induit une structure d'algèbre graduée sur l'algèbre de l'espace des arcs. La série de Hilbert-Poincaré associée à cette algèbre est un invariant des singularités. Je vais introduire cet invariant, parler de son calcul pour certaines singularités et d'une relation entre cette série et une fameuse identité de la théorie des partitions, qui est due à Rogers et à Ramanujan. C'est un travail en commun avec Clemens Bruschek et Jan Schepers.
Le ``size-change principle'' (SCP) est un algorithme simple donnant un test partiel de terminaison qui s'adapte très bien aux langages fonctionnels où les fonctions sont définies de manière récursive par pattern-matching. En présence de constructeurs paresseux, le SCP donne également un test (partiel) de productivité : c'est sur ce principe que les tests (terminaison + productivité) de PML et Agda reposent. Malheureusement, en présence de type coinductifs, certaines définitions récursives bien typées terminent (i.e. sont productives) mais sont incorrectes et rendent Agda/PML inconsistants. En utilisant les travaux de L. Santocanale sur les preuves circulaires et les jeux de parité, je montrerais comment utiliser le SCP pour implanter un test partiel de totalité des définitions récursives qui généralise le test de terminaison/productivité, et garantie qu'une définition est correcte vis à vis de son type.
Le travail à présenter est une contribution à la spécification et la vérification des Systèmes à Base de Composants (SBC) modélisés avec le langage SysML. Les SBC sont largement utilisés dans le domaine industriel et ils sont construits en assemblant différents composants réutilisables, permettant ainsi le développement de systèmes complexes en réduisant leur coût de développement. Malgré le succès de l’utilisation des SBC, leur conception est une étape de plus en plus complexe qui nécessite la mise en œuvre d’approches plus rigoureuses. Dans ce contexte, nous allons traiter principalement deux problématiques: La première est liée à la difficulté de déterminer quoi construire et comment le construire, en considérant seulement les exigences du système et des composants réutilisables, donc la question qui en découle est la suivante : comment spécifier une architecture SBC qui satisfait toutes les exigences du système ? Nous proposons une approche de vérification formelle incrémentale basée sur des modèles SysML et des automates d’interface pour guider, par les exigences, le concepteur SBC afin de définir une architecture de système cohérente, qui satisfait toutes les exigences SysML proposées. Dans cette approche nous exploitons le Model Checker SPIN et la LTL pour spécifier et vérifier les exigences. La deuxième problématique traitée concerne le développement par raffinement d’un SBC modélisé uniquement par ses interfaces SysML. Notre contribution permet au concepteur des SBC de garantir formellement qu’une composition d’un ensemble de composants élémentaires et réutilisables raffine une spécification abstraite d’un SBC. Dans cette contribution, nous exploitons les outils : Ptolemy pour la vérification de la compatibilité des composants assemblés, et l’outil MIO pour la vérification du raffinement.
In this talk we will focus on two-fluid formulations where the fluids are assumed to be compressible and viscosity effects are included in the momentum equations. In the introduction we try to motivate for the study of this model: why can such models be a useful tool for engineers. Then we will narrow the scope and describe a two-fluid model for cell migration. This model can be understood as a generalization of more classical Keller-Segel type of models for cell migration due to random motion and chemotaxis. The model takes the form of a (weakly) compressible two-fluid model with non-conservative pressure terms and interaction terms that play a key role in the momentum equations. The link to Keller-Segel type of models is established by imposing simplifying assumptions and making a specific choice of the interaction term. Existence of global regular solutions for the proposed model for cell migration is then obtained for sufficiently small and regular initial data. The central ingredient in the proof is a basic energy estimate which is combined with certain higher order estimates of cell mass, water mass, and mass of the chemical agent. We also include some examples of numerical solutions of the proposed model that demonstrate pattern formation properties characteristic for Keller-Segel type of models. Sensitivity to different parameters is explored. Finally, we also show some numerical results for a 2D version of a similar model.