Méthodes de réduction par ordre partiel adaptatives.

From LRDE

Résumé

Le model checking explicite de systèmes concurrents souffre d'une croissance exponentielle du nombre d'états représentant un système. Les méthodes de réduction par ordre partiel sont un ensemble de méthodes permettant de combattre ce problème. Celles-ci permettent d'ignorer les états redondants lors de la génération de l'espace d'états. Parmis elles, nous avons choisi les algorithmes two phase et ample set comme base pour nos investigations. Ceux-ci ont été implémentés dans Spot, la bibliothèque C++ de model checking développée au LRDE, en utilisant l'interface DiVine. En se basant sur ces méthodes et sur le fait que les algorithmes dans Spot sont calculés à la volée, nous avons défini une nouvelle classe de méthodes appelées méthodes de réduction par ordre partiel adaptatives. L'idée est de se baser sur l'état courant de l'automate de la formule et non sur la formule tout entière. Les résultats obtenus sur notre suite de tests montrent que cette méthode donne de meilleurs résultats que les méthodes d'ordre partiel classiques.