Méthodes de réduction par ordre partiel dans Spot
From LRDE
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
- Auteurs
- Pierre Parutto
- Type
- techreport
- Année
- 2012
- Numéro
- 1205
Résumé
Spot est une bibliothèque de model checking implémentant une approche par automates. Pour le moment les algorithmes de vérification de propriétés dans Spot utilisent l'espace d'états sans réduction du système. Ils souffrent donc de l'explosion combinatoire de la taille de ce dernier. Une manière de résoudre ce problème est d'utiliser des méthodes de réduction par ordre partiel. Ces méthodes permettent d'ignorer certains comportements équivalents du système pour une certaine propriété. Ainsi il est possible de réduire la taille de l'espace d'états généré tout en conservant le même comportement général. Le but de ce travail est d'évaluer comment ces méthodes d'ordre partiel peuvent être intégrées dans Spot.