Vérification probabiliste et approximation

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.