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 14 Janvier 2003

Model Checking, abstraction et abstraction probabiliste

par 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.

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