Réduction par simulation pour les TGBA
From LRDE
- Auteurs
- Thomas Badie
- Type
- techreport
- Année
- 2013
- Numéro
- 1214
- Projects
- Spot
- Mots-clés
- automata, BDD, bisimulation, simulation, model checkingreduction, TGBA
Résumé
L'approche par automates du model checking s'appuie traditionnellement sur des Automates de Büchi (BA) qu'on souhaite les plus petits possible. Spot, bibliothèque de model checking, utilise principalement des TGBA qui généralisent les BA. Nous avons déjà présenté une méthode de réduction par simulation (dite directe). Cette technique a permis de produire des automates plus petits que dans les précédentes versions. La simulation consiste à fusionner les états ayant le même suffixe infini. Nous montrons que nous pouvons aussi fusionner ceux ayant le même préfixe infini (c'est la cosimulation). On peut répéter la simulation et la cosimulation pour créer la simulation itérée. Cette méthode est incluse dans Spot 1.0 et est une grande amélioration de la simulation. On expérimente aussi une méthode qui consiste à modifier certaines conditions d'acceptations (appellées sans importances). Puisque celles qui sont sur les transitions entre composantes fortement connexes n'ont pas d'influence sur le langage, on peut les modifier pour aider la simulation.