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

From LRDE

Revision as of 17:03, 9 January 2018 by Bot (talk | contribs) (Created page with "{{CSIReportFR | authors = Thomas Badie | titre = Réduction basées sur la bisimulation appliquées aux TGBA | year = 2011 | resume = Spot est une bibliothèque C++ de model c...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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.