29 Février - 6 Mars


Retour à la vue des calendrier
Mardi 1 Mars
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Algèbre de Hopf cambrienne
Description: Grégory Châtel En 1998, Loday et Ronco décrivent une algèbre de Hopf combinatoire dont la base est indicée par des arbres binaires. Cette algèbre possède de nombreux liens avec divers résultats antérieurs. Son produit est en particulier lié aux intervalles du treillis de Tamari, structure d'ordre partiel dont les éléments sont des arbres binaires. En 2006, Reading définit la notion de treillis cambrien d'un groupes de Coxeter. Le treillis Cambrien généralise l'ordre de Tamari en utilisant des structures arborescentes qui généralisent les arbres binaires : les arbres cambriens. Une question naturelle se pose alors : est-il possible de généraliser l'algèbre de Hopf de Loday-Ronco aux arbres cambriens ? Dans cette présentation, j'expliquerai les résultats que nous avons obtenus avec Vincent Pilaud sur les arbres cambriens en type A.
Jeudi 3 Mars
Heure: 14:00 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Parameter Synthesis for Parametric Interval Markov Chains
Description: Laure Petrucci Interval Markov Chains (IMCs) are the base of a classic probabilistic specification theory introduced by Larsen and Jonsson in 1991. They are also a popular abstraction for probabilistic systems. In this paper we study parameter synthesis for a parametric extension of Interval Markov Chains in which the endpoints of intervals may be replaced with parameters. In particular, we propose constructions for the synthesis of all parameter values ensuring several properties such as consistency and consistent reachability in both the existential and universal settings with respect to implementations. We also discuss how our constructions can be modified in order to synthesise all parameter values ensuring other typical properties. Joint work with Benoît Delahaye and Didier Lime
Vendredi 4 Mars
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Caractérisation impérative des algorithmes séquentiels en temps quelconque, primitif récursif et polynomial
Description: Yoann Marquer Les fonctions calculables ont été formalisées par différents modèles de calcul (récursion, lambda-calcul, machines de Turing) ayant le même comportement entrées-sortie : c'est la thèse de Church. Par exemple, une machine de Turing à un ruban peut simuler les résultats calculés par une machine à deux rubans. Pourtant, pour la reconnaissance de palindrome la machine à un seul ruban nécessite une complexité en temps supérieure. Ainsi, il faut étudier les étapes intermédiaires. Nous définissons donc une simulation pas à pas entre exécutions, utilisant uniquement des variables temporaires et une dilatation temporelle.


La thèse de Church concernait donc les fonctions, et il nous faut une nouvelle thèse pour les algorithmes. Nous avons choisi celle de Gurevich pour sa présentation axiomatique : un algorithme séquentiel est un objet vérifiant les trois postulats de temps séquentiel, d'états abstraits et d'exploration bornée. De plus, il a montré que les algorithmes séquentiels coïncident avec son modèle des Abstract State Machines. Nous dirons donc qu'un modèle de calcul est algorithmiquement complet s'il existe une simulation mutuelle d'exécutions entre lui et les ASMs.


Pour obtenir des résultats sur des modèles de calcul plus usuels, nous formalisons les langages impératifs par un système de transition. En étudiant leur sémantique opérationnelle pas à pas et en développant une notion de graphe d'exécution, nous montrons qu'une variante du langage While de Jones est algorithmiquement complète. Ce résultat étant à structures de données près, il correspond donc à une équivalence entre les structures de contrôle des ASMs et des langages impératifs. De plus, étant préoccupés par la faisabilité des algorithmes, nous montrons que les structures du premier ordre utilisées par Gurevich permettent bien d'implémenter les structures de données usuelles.


Notre soucis de la faisabilité nous a également conduit à étudier en terme de complexité implicite deux restrictions des ASMs : celles en temps primitif récursif (les opérations usuelles et terminales) et celles en temps polynomial (les exécutions réalistes). Nous montrons d'une part que si les structures de données sont également primitives récursives, alors une variante LoopC du langage Loop de Meyer et Ritchie est complète pour les algorithmes en temps primitif récursif. D'autre part, une restriction syntaxique LoopCstat de LoopC est complète pour les algorithmes en temps polynomial, sans restriction sur les structures de données et en caractérisant syntaxiquement le degré du polynôme.