Améliorer la determinisation d'automates de Büchi

Auteurs

Alexandre Lewkowicz

Type

techreport

Année

2016

Numéro

1601

Résumé

L'algorithme de Safra permet de construire des automates de Rabin déterministes à partir d'automates de Büchi non-déterministes. Il existe une variante à cette méthode qui permet de construire des automates à parités déterministes. Cependant, ces méthodes produisent des automates avec 2^O(nlogn) états. Il existe des améliorations qui permettent de réduire le nombre d'états dans beaucoup de cas. Nous présentons deux nouvelles stratégies pour aider à réduire le nombre d'états final. La première stratégie utilise les composantes fortement connexes et utilise cette information pour suivre des chemins de Safra différents. La deuxième stratégie utilise l'information retournée par la bisimulation pour retirer des états équivalents. Ceci permet d'éviter de parcourir plusieurs chemins équivalents et ainsi de réduire le nombre d'états final. On montre que nos stratégies permettent souvent de construire des automates déterministes avec moins d'états et que ces automates reconnaissent toujours le même language. On donne des benchmarks pour voir le gain apporté par nos stratégies et on utilise un outil appelé ltl2dstar qui produit des automates de Rabin déterministes à partir de formules LTL pour comparer nos résultats.