Séminaires
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:
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: 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.