Résumé Technique : Un Algorithme Correct pour l'Identification des Ensembles de Variables Indépendantes dans les Systèmes Réactifs

Énoncé du Problème

La synthèse réactive, la construction automatique de systèmes satisfaisant des spécifications de Logique Temporelle Linéaire (LTL) face à tous les comportements possibles de l'environnement, est un problème de complexité élevée (2EXPTIME-complet). Pour répondre aux enjeux de scalabilité, une stratégie courante consiste à décomposer une spécification complexe en sous-spécifications plus petites et indépendantes qui peuvent être résolues séparément.

Le présent article revoit l'algorithme DecomposeContract (DC) introduit par Iannopollo (2018) et Iannopollo et al. (2024). Cet algorithme utilise un modèle de vérification (model checker) pour identifier des ensembles de variables contrôlées par le système qui se comportent de manière indépendante au sein d'une formule LTL. Bien que l'algorithme DC original soit sûr (tout ensemble qu'il identifie comme indépendant est effectivement indépendant), il n'est pas complet. Il peut échouer à détecter des décompositions plus fines, renvoyant un seul grand ensemble de variables dépendantes alors qu'une partition en ensembles indépendés plus petits est possible. Cette limitation entrave l'exploitation totale de la décomposition pour améliorer la scalabilité de la synthèse.

Méthodologie et Fondements Sémantiques

1. Analyse Sémantique de l'Indépendance

Les auteurs fournissent une analyse sémantique rigoureuse de la notion d'indépendance utilisée dans DC. Ils formalisent l'indépendance à l'aide de concepts d'algèbre relationnelle, spécifiquement les opérateurs de projection et de jointure appliqués à des ensembles de traces.

• Projection de Trace ($\sigma \upharpoonright V$) : Restreint une trace à un sous-ensemble de variables $V$ tout en préservant les variables de l'environnement.
• Jointure ($\Sigma_1 \bowtie \Sigma_2$) : Combine des ensembles de traces sur différents sous-ensembles de variables en un ensemble de traces sur leur union, à condition que les traces concordent sur l'intersection.
• Indépendance par Jointure : Un ensemble de variables système $V \subseteq O$ est défini comme indépendant dans une formule $\phi$ si et seulement si la jointure des projections de l'ensemble de modèles $\Sigma_\phi$ sur $V$ et son complément $\bar{V}$ reconstruit l'ensemble de modèles original :
  $$(\Sigma_\phi \upharpoonright V) \bowtie (\Sigma_\phi \upharpoonright \bar{V}) = \Sigma_\phi$$
  Les auteurs prouvent que cette définition sémantique est équivalente à la condition de validité syntaxique utilisée dans l'algorithme DC original : $(\phi_V \land \phi_{\bar{V}}) \to \phi$ est valide.

2. La Limite de l'Algorithme DC Original

L'algorithme DC original construit les ensembles indépendants de manière incrémentale. En partant d'une seule variable, il vérifie si l'ensemble actuel $V$ est indépendant. Si la vérification de validité échoue, le modèle de vérification renvoie une trace de contre-exemple. L'algorithme analyse ensuite cette trace pour trouver les variables dont les valeurs diffèrent de leurs homologues "primés" (fraîches) dans la projection, les ajoutant ainsi à $V$.

L'article démontre que cette approche est incomplète car elle repose sur une vérification directe entre l'ensemble actuel et les variables restantes. Elle ne tient pas compte des dépendances médiées. Comme le montre l'Exemple 11, une variable $b$ peut être dépendante d'un ensemble uniquement lorsqu'elle est considérée aux côtés d'une troisième variable $a$, même si l'interaction directe entre $b$ et le reste de l'ensemble ne révèle pas immédiatement cette dépendance. Par conséquent, DC peut conclure prématurément qu'un ensemble est indépendant ou échouer à fusionner les variables nécessaires, aboutissant à des ensembles indépendants non minimaux.

3. La Solution Proposée : L'Algorithme NDC

Pour atteindre la complétude, les auteurs proposent NDC (New DecomposeContract). La modification centrale réside dans la fonction ParseTrace, remplacée par NewParseTrace.

• Détection de Dépendance Affinée : Lorsque la vérification de validité échoue, NewParseTrace n'ajoute pas simplement toutes les variables qui diffèrent dans le contre-exemple. Au lieu de cela, il construit de manière itérative une formule binds qui accumule les contraintes ($\Diamond(z \leftrightarrow \neg z')$) sur les variables identifiées comme dépendantes.
• Raffinement Itératif : L'algorithme interroge le modèle de vérification avec une disjonction : binds $\lor$ ((\phi_V \land \phi_{\bar{V}}) \to \phi). Si cette formule est invalide, le modèle de vérification fournit une nouvelle trace où les contraintes actuelles de binds sont violées, révélant une nouvelle variable $z$ qui doit être ajoutée à l'ensemble.
• Garantie Théorique : L'algorithme repose sur le Lemme 6, qui établit que si un ensemble $V$ est dépendant au sein d'un sur-ensemble indépendant plus large $W$, alors aucune variable $q \in W$ ne peut "témoigner" de l'indépendance de $V$ à moins que la dépendance ne soit explicitement exposée par l'accumulation de contraintes. Cela garantit que l'algorithme continue d'étendre l'ensemble jusqu'à ce qu'il atteigne un ensemble indépendant minimal.

Contributions Clés et Résultats

1. Formalisation Mathématique : L'article fournit le premier compte rendu sémantique rigoureux de la notion d'indépendance utilisée dans les travaux d'Iannopollo, en la définissant via les projections et les jointures de traces. Cela clarifie les fondements théoriques de la méthode de décomposition.
2. Preuve d'Incomplétude : Les auteurs présentent un contre-exemple concret (Exemple 6 et Exemple 11) démontrant que l'algorithme DC original n'est pas complet et peut manquer des décompositions valides.
3. Algorithme Correct et Complet (NDC) : L'article introduit NDC, un algorithme raffiné qui préserve la nature en temps polynomial de la méthode originale (hors coûts du modèle de vérification) tout en assurant la complétude.
4. Garantie de Minimalité : Le principal résultat théorique (Théorème 1) prouve que NDC renvoie une partition des variables système en ensembles indépendants minimaux. Cela signifie que si un ensemble est renvoyé comme indépendant, aucun sous-ensemble propre non vide de celui-ci n'est lui-même indépendant. C'est une garantie plus forte que celle du DC original, qui ne garantit que la sûreté.
5. Limites de la Réalisabilité : L'article distingue explicitement la satisfaisabilité (où les traces sont les objets sémantiques) de la réalisabilité (où les stratégies gagnantes sont les objets sémantiques). Les auteurs notent que si NDC est complet pour identifier l'indépendance dans le cadre de la satisfaisabilité, étendre ces résultats à la réalisabilité est nettement plus complexe. Dans le cadre de la réalisabilité, l'ensemble des traces induites par les stratégies gagnantes est un sous-ensemble de toutes les traces satisfaisantes, et la minimalité de la décomposition n'est pas garantie comme étant calculable avec la même efficacité que l'approche basée sur la satisfaisabilité.

Signification et Revendications

L'article affirme que sa principale contribution est théorique, fournissant un fondement rigoureux pour les méthodes de décomposition en synthèse réactive. En clarifiant la sémantique de l'indépendance et en corrigeant la procédure algorithmique, les auteurs permettent la décomposition fiable des spécifications LTL en composants indépendants minimaux.

La signification réside dans :

• Correction : Garantir que la décomposition ne manque pas d'opportunités de scinder les spécifications, ce qui est crucial pour la scalabilité des outils de synthèse.
• Efficacité : Maintenir l'efficacité pratique de l'utilisation des modèles de vérification (qui sont hautement optimisés) plutôt que de recourir à des opérations de théorie des automates coûteuses comme la complémentation.
• Clarté : Délimiter explicitement les frontières de la méthode, particulièrement la distinction entre l'indépendance basée sur la satisfaisabilité et l'indépendance basée sur la stratégie, afin d'éviter des attentes trop optimistes concernant l'application directe de ces résultats au problème complet de la réalisabilité.

Ce travail ne propose pas de nouveaux tests expérimentaux ou de futures implémentations d'outils, mais se concentre sur l'établissement de la correction mathématique et de la complétude de la logique de décomposition elle-même.