Un Feedback Arc Set pour Spot

Auteurs

Alexandre Lewkowicz

Type

techreport

Année

2014

Numéro

1406

Résumé

Spot est une bibliothèque extensible pour le model checking qui utilise les automates de Büchi généralisés à transitions acceptantes. Il contient de nombreux algorithmes de pointes. Dans ce papier, on se concentre sur deux de ses algorithmes qui construisent des automates avec plus de transitions que nécessaire. En pratique ces constructions utiliseraient moins de transitions si elles pouvaient calculer un feedback arc set (FAS), c'est-à-dire un ensemble de transitions à retirer du graphe pour le rendre acyclique. Dans l'absoluon veut un FAS minimal, mais ce problème est NP-difficile. On adapte et améliore une heuristique proposée par Eades et al. qui permet une construction en temps linéaire. On montre comment cet algorithme bénéficie à la complémentation d'automates de Büchi déterministes et la traduction d'automates de Rabin en automates de Büchi. En fonction de l'automata traité on remarque une amélioration montant jusqu'à 31%. Ces résultats varient beaucoup selon le nombre de cycles et d'états acceptant.