Retour à l'index du GREYC

Séminaire Algorithmique

Site du CNRS

Séminaire Algorithmique

Le séminaire a lieu le mardi à 11 h 45 (sauf modification exceptionnelle), au campus Côte de Nacre, bâtiment Sciences 3, salle S3 351, 3ème étage.

Résumé du séminaire du Mardi 13 Mars 2007

Vérification probabiliste et approximation

par Richard Lassaigne (Equipe de Logique Mathématiques/Paris 7)

Cet exposé présente un état de l'art de résultats récents concernant deux types d'approximation qui peuvent être utiles dans le contexte de la vérification pour réduire la complexité en temps et en espace. Dans le premier cas, on introduit une notion d'approximation sur les données, c'est-à-dire sur le modèle à vérifier, définie a l'aide d'une distance. Il est alors possible de concevoir des algorithmes probabilistes permettant de décider, en temps indépendant de la taille du modèle, si la propriété considérée est satisfaite ou si elle est loin, à epsilon près au sens de la distance, de l'être. Dans le second cas, on définit une méthode d'approximation pour la vérification de propriétés quantitatives sur des systèmes probabilistes. Les algorithmes probabilistes d'approximation ainsi obtenus permettent de réduire de manière exponentielle la complexité en espace. Ces algorithmes ont été implémentés de manière distribuée dans un model checker probabiliste qui s'est révélé très efficace.

GREYC
Campus Côte de Nacre, boulevard du Maréchal Juin
BP 5186
14032 Caen Cedex
FAX : +33 (0)2 31 56 73 30
http://www.greyc.fr