Méthodes de réduction par ordre partiel dans Spot

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.