💻 computer science

Kofola 1.0: A Modular Approach to {\omega}-Regular Complementation and Inclusion Checking (Technical Report)

Cet article présente Kofola, un outil efficace et robuste qui utilise un cadre modulaire pour décomposer les automates de Büchi en composantes fortement connexes afin d'effectuer des vérifications de complémentation et d'inclusion sur mesure, démontrant des performances supérieures aux outils de l'état de l'art grâce à une vérification de vacuité à la volée et à de nouvelles heuristiques.

Auteurs originaux : Ondrej Alexaj, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, Yong Li, Nicolas Mazzocchi

Publié 2026-05-18

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Ondrej Alexaj, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, Yong Li, Nicolas Mazzocchi

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous êtes inspecteur de contrôle qualité pour une usine massive et infinie. Cette usine produit des flux incessants de produits (appelés « mots » en informatique). Vous disposez de deux machines : Machine A et Machine B.

Votre tâche consiste à répondre à une question très difficile : « Tout produit fabriqué par la Machine A est-il également fabriqué par la Machine B ? »

Si la réponse est « Oui », alors la Machine A est sûre d'utilisation. S'il existe même un seul produit fabriqué par la Machine A que la Machine B ne fabrique jamais, alors la Machine A est dangereuse.

Ceci est le problème central de la Vérification d'Inclusion de Langages. C'est une tâche fondamentale pour vérifier que les logiciels et le matériel informatique se comportent correctement. Cependant, comme les flux de produits sont infinis, vérifier cela manuellement est impossible. Vous avez besoin d'un robot ultra-intelligent pour le faire.

Voici Kofola, un nouveau robot hautement efficace conçu pour résoudre ce problème. Voici comment il fonctionne, décomposé en concepts simples :

1. L'Ancienne Méthode vs La Méthode Kofola

Auparavant, les robots tentant de résoudre ce problème devaient examiner l'ensemble du plancher de l'usine en une seule fois. Ils essayaient de construire une carte géante de tous les chemins possibles que la Machine A pouvait emprunter et de les comparer à ceux de la Machine B. Cette carte était si immense qu'elle faisait souvent exploser le cerveau du robot (un problème appelé « explosion de l'espace d'états »).

Le Secret de Kofola : L'Approche Modulaire
Au lieu d'examiner toute l'usine d'un coup, Kofola est un maître organisateur. Il observe la Machine B et dit : « Cette usine n'est pas un grand chaos ; elle est en fait composée de quartiers distincts. »

Kofola décompose la Machine B en Composantes Fortement Connexes (CFC). Imaginez-les comme différentes pièces ou zones de l'usine :

Les Impasses : Des pièces où la machine cesse de produire des produits.
Les Boucles Simples : Des pièces où la machine tourne en rond, faisant la même chose encore et encore.
Les Zones Déterministes : Des pièces où la machine n'a qu'un seul choix à chaque étape (comme un train sur une voie unique).
Les Zones Chaotiques : Des pièces où la machine a de nombreux choix et peut aller dans différentes directions (comme un labyrinthe).

Kofola traite chaque « quartier » différemment. Il utilise un outil spécialisé et simple pour les boucles simples et un outil lourd pour les zones chaotiques. Il ne gaspille pas d'énergie à essayer de résoudre les parties faciles avec un marteau-piqueur.

2. La Nouvelle Découverte « IADAC »

L'article introduit un nouveau type de quartier appelé IADAC (Composante d'Acceptation Initiale Presque Déterministe).

L'Analogie : Imaginez un couloir menant à une pièce. Le couloir est une voie droite et unique (déterministe). Une fois entré dans la pièce, vous pourriez avoir des choix. Mais voici l'astuce : une fois que vous quittez cette pièce, vous ne pouvez plus jamais revenir au couloir.
Pourquoi c'est important : Parce que le couloir est si prévisible, Kofola peut utiliser une méthode très rapide et légère pour le vérifier, plutôt que la méthode lourde et lente nécessaire pour les parties chaotiques. C'est un nouveau type de zone que les auteurs ont identifié et optimisé.

3. L'Inspecteur « Paresseux » (Vérification à la Volée)

Habituellement, pour vérifier si l'usine est sûre, vous devez construire l'intégralité de la carte de l'usine avant de pouvoir dire « Sûr » ou « Dangereux ».

Kofola est paresseux au maximum (dans le bon sens). Il commence à construire la carte, mais dès qu'il trouve suffisamment de preuves pour décider de la réponse, il s'arrête.

S'il trouve un « mauvais produit » tôt, il crie immédiatement : « Dangereux ! » et arrête de travailler.
Il ne perd pas de temps à cartographier le reste de l'usine si la réponse est déjà claire.

Ceci est réalisé grâce à un nouvel algorithme de « vérification de vacuité ». Imaginez que vous cherchez un type spécifique de bug dans une pièce sombre. Au lieu d'allumer les lumières pour toute la pièce, vous n'éclairez avec votre lampe de poche que le chemin que vous parcourez. Si vous trouvez le bug, vous vous arrêtez. Si vous parcourez tout le chemin sans le trouver, vous savez que la pièce est claire. Kofola fait cela instantanément pendant qu'il construit la carte.

4. Les Résultats : Kofola Gagne la Course

Les auteurs ont testé Kofola contre les meilleurs robots existants (des outils comme Spot, Rabit et Bait) en utilisant des milliers de plans d'usines réels.

Robustesse : Kofola était le seul outil à avoir résolu avec succès chaque cas de test sans planter ni épuiser la mémoire. Les autres ont échoué sur de nombreux cas difficiles.
Vitesse : Sur de nombreux problèmes pratiques, Kofola n'était pas seulement plus rapide ; il était plus rapide d'ordres de grandeur. Dans certains cas, alors que d'autres outils tentaient encore de construire la carte après 2 minutes, Kofola avait déjà terminé en une fraction de seconde.
Taille : Les cartes construites par Kofola étaient souvent beaucoup plus petites et plus compactes que celles construites par les concurrents.

Résumé

Kofola est un nouvel outil ultra-efficace pour vérifier si un système informatique est « contenu » dans un autre. Il fonctionne en :

Décomposant le problème en quartiers plus petits et gérables.
Utilisant le bon outil pour chaque type de quartier spécifique (y compris un nouveau type qu'il a découvert).
Étant paresseux, en arrêtant le travail dès qu'il a suffisamment d'informations pour donner une réponse.

Le résultat est un outil plus rapide, plus fiable, capable de gérer des problèmes beaucoup plus vastes et complexes que tout ce qui est actuellement disponible. C'est une amélioration significative pour le « contrôle qualité » des systèmes informatiques.

Résumé technique : Kofola 1.0 – Une approche modulaire pour la complémentation ω-régulière et la vérification d'inclusion

Énoncé du problème

La vérification de l'inclusion de langages pour les automates de Büchi (AB) est un problème fondamental en vérification basée sur la théorie des automates, avec des applications critiques dans la vérification de modèles, la surveillance et la démonstration de théorèmes. Le problème est PSpace-complet et reste computationnellement exigeant à mesure que les spécifications des systèmes augmentent en taille et en complexité. Décider si $L_1 \subseteq L_2$ revient à vérifier la vacuité de $L_1 \cap \overline{L_2}$ , où $\overline{L_2}$ est le complément de $L_2$ . Cette réduction présente deux défis principaux :

Complémentation compacte : Construire l'automate complément $\overline{L_2}$ efficacement sans provoquer d'explosion de l'espace d'états.
Exploration efficace : Explorer l'automate produit de $L_1 \cap \overline{L_2}$ , qui est souvent énorme.

Les outils existants reposent largement sur des constructions de complémentation classiques basées sur Ramsey ou sur la déterminisation, remontant à plus de trois décennies. Bien que des avancées récentes en complémentation existent, elles n'ont pas été pleinement intégrées dans les vérificateurs d'inclusion pratiques.

Méthodologie

L'article présente Kofola, un outil efficace implémenté en C++ qui met en œuvre un cadre de complémentation modulaire de l'état de l'art. La méthodologie repose sur la décomposition de l'automate d'entrée en composantes fortement connexes (CFC) et l'application d'algorithmes de complémentation adaptés à chaque composante en fonction de ses propriétés structurelles.

1. Décomposition structurelle et classification des composantes

Kofola effectue une analyse structurelle fine de l'automate à complémenter ( $A_2$ ). Il classe ses CFC maximales en quatre catégories distinctes :

Composantes non acceptantes : Gérées via la construction classique des sous-ensembles.
Composantes acceptantes intrinsèquement faibles (IWAC) : Composantes où tous les cycles acceptent.
Composantes acceptantes déterministes (DAC) : Composantes ne possédant que des transitions déterministes.
Composantes acceptantes initialement presque déterministes (IADAC) : Un nouveau type de composante identifié dans cet article. Il s'agit de CFC déterministes accessibles depuis les états initiaux via des CFC déterministes, ne permettant la non-déterminisme que sur des chemins sans cycle entre les CFC.
Composantes acceptantes non déterministes (NAC) : Les CFC acceptantes restantes.

2. Cadre de complémentation modulaire

Pour chaque type de composante, Kofola applique un algorithme de complémentation partielle dédié :

IWAC : Utilise la construction classique de Miyano-Hayashi, générant une condition d'acceptation $Inf(1)$.
DAC : Utilise une modification de l'algorithme NCSB, générant une condition d'acceptation $Inf(2)$.
NAC : Prend en charge deux approches selon la tâche :
- Complémentation : Utilise une approche basée sur la déterminisation (variante de Safra-Piterman) pour produire des automates plus petits.
- Vérification d'inclusion : Utilise une approche basée sur les tranches, mieux adaptée aux tests de vacuité du produit à la volée.
IADAC : L'article introduit un nouvel algorithme partiel pour ces composantes. Il déterminise les IADAC en utilisant une construction des sous-ensembles et émet un marqueur de rejet ($Fin(0)$) chaque fois qu'un parcours suivi observe une transition acceptante. La correction repose sur le fait que les parcours dans les IADAC sont bornés en raison de leur non-déterminisme restreint.

L'algorithme de haut niveau synchronise ces constructions partielles. L'automate complément résultant est un automate de Rabin généralisé simple (SGRA) avec une seule condition d'acceptation de la forme $Fin(0) \land Inf(1) \land \dots \land Inf(k-1)$ .

3. Vérification de vacuité à la volée

Pour faire face à l'explosion de l'espace d'états dans la vérification d'inclusion, Kofola emploie un nouvel algorithme de vérification de vacuité à la volée pour le SGRA résultant.

Construction paresseuse : Contrairement aux outils qui nécessitent la construction explicite de l'automate produit complet, Kofola explore l'espace d'états de manière paresseuse.
Algorithme : L'algorithme est une variante de l'algorithme de Couvreur étendue avec un prédicat $Fin$. Il effectue une recherche en profondeur, gérant une pile d'ensembles de transitions pour détecter les CFC.
Terminaison : La recherche se termine dès que l'espace d'états exploré est suffisant pour décider du résultat (soit en trouvant un cycle acceptant, soit en prouvant la vacuité). Cela minimise la partie générée du complément, ce qui est crucial car la complémentation est la source principale de l'explosion.

Contributions clés

Outil Kofola : Un outil efficace et modulaire pour la complémentation d'AB et la vérification d'inclusion de langages.
Identification des IADAC : L'introduction et la formalisation des composantes acceptantes initialement presque déterministes (IADAC) en tant que classe structurelle distincte.
Nouvel algorithme de complémentation : Un algorithme partiel dédié pour les IADAC qui génère la condition $Fin(0)$, permettant la construction d'une seule paire de Rabin généralisée.
Vérification de vacuité paresseuse : Un nouvel algorithme à la volée pour les SGRA qui évite la construction explicite d'un automate complet, permettant une terminaison anticipée.
Cadre modulaire : Une architecture flexible permettant de combiner synchroniquement différents algorithmes partiels basés sur l'analyse structurelle.

Résultats expérimentaux

Les auteurs ont évalué Kofola par rapport aux outils de l'état de l'art : Spot, Ranker, Owl, Bait, Forklift et Rabit.

Benchmarks de complémentation

Jeu de données : 31 273 automates provenant de sources diverses (terminaison de programmes, logique des mots de Sturmian, hyperpropriétés, S1S, traduction LTL et génération aléatoire).
Robustesse : Kofola a été le seul outil à compléter avec succès les 31 273 automates d'entrée. L'outil suivant le plus robuste, Spot, a échoué sur 2 instances en raison de limites de mémoire.
Taille : Kofola a produit des automates complément significativement plus petits en moyenne (79,24 états) par rapport à Spot (115,38 états) et Ranker (45,80 états, bien que Ranker ait échoué sur 443 instances).
Performance : Kofola a résolu le plus grand nombre d'instances et a souvent surpassé ses concurrents de plusieurs ordres de grandeur en temps d'exécution.

Benchmarks de vérification d'inclusion

Jeu de données : 1 014 problèmes d'inclusion provenant de la terminaison de programmes, de la vérification de systèmes concurrents, de la vérification de modèles d'hyperpropriétés et de la démonstration de théorèmes.
Performance : Kofola a résolu le plus grand nombre d'instances (seulement 2 non résolues) et a eu le temps d'exécution total le plus faible (141 secondes pour les problèmes résolus).
Comparaison : Kofola a strictement gagné contre Spot(Det) sur 263 instances et n'a perdu sur aucune. Il a considérablement surpassé les outils basés sur Ramsey (Bait, Forklift, Rabit), qui nécessitaient souvent un ordre de grandeur de temps supplémentaire.
Observation : 98 % des automates du côté droit des requêtes d'inclusion (ceux étant complémentés) étaient des automates ascenseur (ne contenant aucune NAC), soulignant la pertinence pratique de l'exploitation des propriétés structurelles.

Importance et affirmations

L'article affirme que Kofola établit une nouvelle norme en matière d'efficacité et de robustesse pour la complémentation d'AB et la vérification d'inclusion. Son importance réside dans :

Praticité : Il apporte des techniques de complémentation modernes basées sur la décomposition à la vérification d'inclusion pratique, dépassant les constructions classiques.
Évolutivité : En combinant la décomposition structurelle avec la vérification de vacuité paresseuse à la volée, il atténue efficacement l'explosion de l'espace d'états, résolvant des instances qui sont intraitables pour les outils existants.
Extensibilité : L'architecture modulaire permet l'intégration de nouveaux algorithmes de complémentation partielle pour des types de composantes spécifiques.

Les auteurs positionnent Kofola non pas comme une amélioration incrémentale, mais comme un outil hautement compétitif qui surpasse souvent les solutions de l'état de l'art de plusieurs ordres de grandeur sur des benchmarks dérivés d'applications pratiques.