Un ensemble d'outils de conversion en automate de co-Büchi

Auteurs

Alexandre Gbaguidi Aïsse

Type

techreport

Année

2017

Numéro

1705

Résumé

Grâce au format HOA, il y a de moins en moins de barrières entre des ω-automates avec différentes conditions d'acceptation. Spot, une bibliothèque manipulant les ω-automates supporte des conditions d'acceptations arbitraires et propose déjà quelques conversions entre elles. Nous rajoutons de nouveaux algorithmes de conversions capables de convertir (quand c'est possible) n'importe quelle condition d'acceptation classique vers du co-Büchi déterministe. Boker and Kupferman ont mis au point des méthodes asymptotiquement optimales réalisant ces conversions. Nous avons implémenté leurs méthodes avec quelques optimisations et adaptations: nous supportons les conditions d'acceptations dites "Streett-like", celles écrites sous forme normale disjonctive (y compris celles dites "Rabin-like") ainsi que les acceptations basées sur les transitions ("transition-based"). Ces algorithmes peuvent être utilisés pour vérifier si une formule LTL est de la famille "persistence".