Echantillonnage preferentiel pour le model checking statistique

摘要

Le model checking statistique est une alternative interessante au model checking numerique lorsque les modeles probabilistes etudies sont de tres grande taille. Cependant l'approche statistique ne permet pas d'evaluer les probabilites des evenements rares. Afin de resoudre ce probleme, nous developpons ici une nouvelle approche basee sur l'echantillonnage preferentiel. Alors que la plupart des techniques d'echantillonnage preferentiel sont basees sur des heuristiques, nous etablissons des resultats theoriques, Moyennant certaines hypotheses, ces resultats garantissent une reduction de la variance lors de l'application de l'echantillonnage preferentiel. Nous caracterisons des situations qui verifient les hypotheses et etendons notre approche dans les autres situations mais cette foisci sans garantie theorique. Nous avons implemente cette approche a l'aide de l'outil COSMOS apres avoir ajoute des fonctionnalites. Enfin nous presentons l'evaluation de notre methode sur deux exemples et analysons les experimentations.