Une implementation efficace de déterminisation d'automates de Büchi généralisés à transitions acceptantes

Auteurs

Alexandre Lewkowicz

Type

techreport

Année

2015

Numéro

1503

Résumé

Dans le model checking probabiliste, l'utilisation d' ω-automates déterministes permet de faciliter les calculs probabilistes grâce à l'unicité de chaque chemin. Malheureusement, il existe peu de traducteurs LTL qui produisent des ω-automates déterministes. De plus, ceux produits par Spot, une bibliothèques de model checking, ne le sont pas forcément. La powerset construction n'arrive pas toujours à déterminiser les automates de Büchi. Cependant, en mémorisant les chemins acceptants, la construction de Safra arrive à convertir les automates nondéterministes de Büchi en automates déterministes de Rabin. Le changement de condition d'acceptation est nécessaire car les automates de Büchi déterministes sont moins expressifs que leurs variantes nondéterministes. L'implémentation de cette construction permettra à Spot de déterminiser tous types d'automates et de calculer leurs compléments. Dans ce papier, on verra comment implémenter de manière efficace cette construction et comment l'étendre à la déterminisation d'automates de Büchi généralisés à transitions acceptantes.