Sylvain Peyronnet (LRI, Orsay)

Le Model Checking (“vérification de modèle”) est un ensemble de techniques algorithmiques qui permettent de vérifier des propriétés de systèmes logiques. Le problème principalement rencontré en Model Checking n’est pas celui de la complexité des algorithmes (qui sont polynomiaux en la taille du système, voire linéaires), mais celui de la taille du système : c’est le phénomène de l’explosion combinatoire du nombre d’états. Une des principales techniques pour lutter contre ce phénomène est la mise au point d’abstraction du système.

Après avoir présenté le cadre général du Model Checking, je présenterai la notion d’abstraction, puis une extension de celle ci : l’abstraction probabiliste.

Les travaux que je présenterais ont été réalisés en commun avec Sophie Laplante, Richard Lassaigne, Frédéric Magniez et Michel de Rougemont.