Résumé technique : Complémentation des automates à ascenseur d'Emerson-Lei

Énoncé du problème

La complémentation des $\omega$-automates est une opération fondamentale en méthodes formelles, essentielle pour des tâches telles que l'analyse de la terminaison de programmes, le model checking de logiques temporelles (par exemple, LTL, HyperLTL) et la décision de théories logiques (par exemple, S1S). Cependant, la complémentation des $\omega$-automates généraux est notoirement difficile, entraînant souvent une explosion de l'espace d'états qui rend la vérification pratique irréalisable.

Bien que des restrictions structurelles comme les « automates à ascenseur » (où chaque composante fortement connexe est soit déterministe, soit intrinsèquement faible) aient montré qu'elles permettent une complémentation plus efficace pour les automates de Büchi standards, ces optimisations n'ont pas été pleinement étendues aux automates dotés de conditions d'acceptation plus riches. Les automates d'Emerson-Lei (ELA), qui supportent des combinaisons booléennes arbitraires de prédicats Inf (infinitésimalement souvent) et Fin (fini souvent), offrent une plus grande concision et flexibilité mais manquent actuellement d'algorithmes de complémentation efficaces tenant compte de la structure. Les algorithmes existants pour les ELA non restreints souffrent d'une complexité asymptotique élevée, et il existe un fossé concernant les méthodes pratiques pour complémenter les ELA présentant la structure « ascenseur » fréquemment rencontrée dans les applications réelles.

Méthodologie

Le papier introduit les Automates à Ascenseur d'Emerson-Lei (ELEA), une généralisation des automates à ascenseur de Büchi au cadre d'acceptation d'Emerson-Lei. Les auteurs proposent un nouvel algorithme de complémentation qui exploite les propriétés structurelles des ELEA pour atteindre des bornes de complexité nettement meilleures que la complémentation des ELA généraux.

La méthodologie se déroule en trois étapes principales :

1. Automates Semi-Déterministes (ELSA) avec conditions spécifiques :
   Les auteurs traitent d'abord la complémentation des Automates Semi-Déterministes d'Emerson-Lei (ELSA), où les parcours entrent éventuellement dans une composante déterministe. Ils développent des constructions pour deux cas spécifiques :

   • Paires de Rabin Généralisées : L'algorithme combine la construction de Miyano-Hayashi (pour les conditions Fin) et l'algorithme NCSB (pour les conditions Inf). Il utilise une structure de macro-état $(N, R, C, S_1, \dots, S_k, B)$ pour suivre les parcours dans la partie non déterministe ($N$) et la partie déterministe. La partie déterministe est divisée en ensembles suivant les violations de Fin ($R$) et les violations de Inf ($C$ et les ensembles sûrs $S_i$). Un ensemble de points de rupture global $B$ garantit que tous les parcours sont inspectés infiniment souvent.
   • Paires de Streett Généralisées : En tant que dual de la construction de Rabin, cette construction utilise un compteur de planification round-robin ($z$) pour invalider séquentiellement toutes les conditions de la paire de Streett. Elle réutilise des ensembles entre une instance NCSB (pour la condition Inf) et plusieurs instances de Miyano-Hayashi (pour les conditions Fin).

2. Procédure inductive pour les conditions d'Emerson-Lei arbitraires :
   Pour gérer les combinaisons booléennes arbitraires de Inf et Fin, les auteurs introduisent une approche par arbre de macro-états. La condition d'acceptation niée $\psi = \neg Acc$ est représentée sous forme d'un arbre reflétant sa structure syntaxique.

   • Mode Échantillonnage (Sampling Mode) : Les parcours entrant dans la composante déterministe sont assignés de manière non déterministe à des sous-arbres correspondant aux disjonctions de $\psi$.
   • Mode Vérification (Checking Mode) : L'algorithme vérifie que les parcours satisfont les sous-formules assignées. Pour les conditions Inf, il utilise des ensembles de points de rupture pour assurer des visites infinies ; pour les conditions Fin, il s'assure que les parcours évitent certaines couleurs.
   • Optimisations : Le papier détaille plusieurs optimisations pour réduire l'explosion de l'espace d'états :
     • Normalisation de l'arbre de macro-états : Fusion des suivis de parcours redondants lorsque les parcours fusionnent.
     • Optimisation du point de rupture partagé : Utilisation d'un point de rupture unique partagé pour plusieurs feuilles Inf via une planification round-robin.
     • Optimisation OR-FIN : Propagation séquentielle des états violant les conditions à travers les feuilles Fin dans les disjonctions pour éviter une ramification exponentielle.

3. Extension aux automates complets à ascenseur et non restreints :
   Les techniques développées pour les ELSAs sont étendues aux pleins ELEAs. Les auteurs notent qu'en pratique, de nombreux automates non-ascenseurs sont « presque ascenseurs » (ne contenant que quelques composantes fortement connexes non-ascenseurs). Leur conversion traite cela efficacement, en tirant parti du fait que la plupart des composantes fortement connexes dans les automates pratiques sont déjà des composantes ascenseurs.

Contributions clés et résultats

• Définition des ELEA : Le papier définit formellement les Automates à Ascenseur d'Emerson-Lei, généralisant le concept d'automates à ascenseur aux conditions d'acceptation riches.
• Amélioration des bornes de complexité : L'algorithme proposé atteint une complexité de l'espace d'états asymptotiquement bien plus faible pour le complément d'un ELEA par rapport aux meilleurs algorithmes connus pour les ELA non restreints.
  • Pour une paire de Rabin généralisée avec $k$ paires, la taille du complément est bornée par $(k+3)n$ (ou $(5+k)n$ dans le cas général présenté dans la section 3), alors que les ELA non restreints ont des bornes comme $O(n^{k}(0.76n)^{n})$.
  • Le Tableau 1 du papier fournit une comparaison exhaustive, montrant des améliorations exponentielles ou polynomiales par rapport aux bornes non restreintes pour diverses conditions (Büchi, Rabin, Streett, Parité et Emerson-Lei).
• Implémentation pratique et évaluation : L'algorithme est implémenté dans l'outil Kofola. Les comparaisons expérimentales avec l'outil de pointe Spot démontrent que Kofola produit souvent des compléments dont la taille est bien plus petite. Les tests de référence incluent des ELA issus de la littérature, des automates de Rabin généralisés générés aléatoirement, et des ELA dérivés de traductions LTL.

Signification et revendications

Les auteurs affirment que ce travail représente la première étape vers des algorithmes pratiques pour la complémentation, la détermination et le test d'universalité et d'inclusion pour les automates d'Emerson-Lei dotés de conditions d'acceptation riches.

La signification réside dans le pont jeté entre la concision théorique (fournie par les ELEA) et l'efficacité de la vérification pratique. En exploitant la prévalence structurelle des composantes ascenseurs dans les automates réels (comme indiqué dans les travaux antérieurs [1]), les auteurs fournissent une méthode qui réduit drastiquement le problème de l'explosion d'états inhérent à la complémentation. Le papier positionne cela comme une contribution fondamentale, permettant des flux de travail de vérification plus efficaces pour les systèmes modélisés avec des conditions d'acceptation sophistiquées, sans inventer de nouvelles applications au-delà de celles déjà établies dans le domaine (model checking LTL, vérification de propriétés hyper-logiques).

Le travail est modeste dans sa portée, se concentrant strictement sur le problème de la complémentation et ses implications immédiates pour la détermination et le test d'inclusion, tout en reconnaissant que des travaux supplémentaires sont nécessaires pour réaliser pleinement des algorithmes pratiques pour toutes les opérations sur les ELEA.