Réduction basées sur la bisimulation appliquées aux TGBA

Auteurs

Thomas Badie

Type

techreport

Année

2011

Numéro

1104

Projects

Spot

Mots-clés

automata, reduction, bisimulation, BDD, state, TGBA

Résumé

Spot est une bibliothèque C++ de model checking utilisant l'approche par automates. Pour représenter les propriétés à vérifier, nous utilisons des formules LTL, qui sont traduites en automates. Dans Spot, ces automates sont des Automates de Büchi généralisés basés sur les transitions (TGBA). Un enjeu pour tout model checker, est d'être rapide. Une manière de faire est de rendre les automates aussi petit que possible. La littérature scientifique propose de nombreux algorithmes pour arriver à notre but. La bisimulation et la simulation réduisent des automates qui reconnaissent des mots de longueur infinis. Cette présentation montre comment adapter ces algorithmes pour des TGBA ainsi que le gain apporté par l'implémentation de la bisimulationce qui souligne l'importance d'implémenter la simulation pour réduire les TGBA.