Séminaire du 22 janvier 2016

Lieu

IBISC, site IBGBI : comment y aller

Programme

14h00-15h00: Laure Petrucci (LIPN, Université Paris 13), "Parameter Synthesis for Parametric Interval Markov Chains" - joint work with Benoît Delahaye and Didier Lime

Abstract:transparents 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.

15h00-15h30 : Laure Millet (LIP6, UPMC), "Vérification et synthèse d’algorithmes de robots"

Abstract:transparents ce travail se situe dans un contexte particulier de l’algorithmique répartie, qui concerne les protocoles pour robots mobiles. Certains de ces protocoles étant critiques, il est nécessaire de s’assurer qu’ils satisfont bien leurs spécifications et, en amont, de pouvoir les générer automatiquement.

Afin d’obtenir des protocoles qui peuvent fonctionner dans des conditions difficiles, nous considérons des robots ayant des capacités limitées : ils ne disposent pas de mémoire, ni de sens de l’orientation, ni de la capacité à communiquer par échange de messages. En revanche, ils peuvent observer leur environnement et utiliser ces observations pour prévoir leurs déplacements.

Nous proposons un modèle général permettant d’exprimer ces protocoles avec différentes hypothèses d’atomicité pour les exécutions, lorsque les robots se déplacent sur un graphe fini. En implantant ce modèle dans le format d’entrée de DiVine, nous avons vérifié par model checking des instances de deux protocoles d’exploration proposés dans la littérature. En reformulant les problèmes de rassemblement comme des jeux d’accessibilité à deux joueurs, nous avons également synthétisé des protocoles (optimaux) résolvant ce problème dans le contexte le plus général d’exécutions asynchrones.

15h30-16h00: pause café

16h00-16h30: vie du groupe