Résumé Technique : Vérification Statistique Multi-Objectifs par Échantillonnage de Stratégies Légères

Énoncé du Problème

La vérification statistique (SMC - Statistical Model Checking) est une technique bien établie pour la vérification de systèmes probabilistes à grands espaces d'états où la vérification de modèles probabilistes (PMC) exhaustive échoue en raison de l'explosion de l'espace d'états. Cependant, les approches SMC existantes sont limitées à l'évaluation d'une seule propriété à la fois. Dans de nombreux scénarios pratiques, tels que l'équilibrage entre l'utilisation de la batterie d'un satellite et son utilité ou l'optimisation du coût d'une pompe à chaleur par rapport au confort, les décideurs ont besoin du front de Pareto : l'ensemble des compromis optimaux entre plusieurs objectifs, souvent conflictuels.

Bien que des algorithmes de PMC multi-objectifs existent (par exemple, en utilisant la programmation linéaire ou l'itération de valeur), ils nécessitent une exploration complète de l'espace d'états, ce qui les rend inapplicables aux modèles comportant des milliards d'états ou des espaces d'objectifs de grande dimension. De plus, les outils existants comme Uppaal Stratego ne gèrent les problèmes multi-objectifs que via un ordonnancement lexicographique ou une optimisation unidimensionnelle, échouant ainsi à capturer les compromis entre des objectifs de priorité égale. Il n'existe actuellement aucune approche SMC capable de calculer des fronts de Pareto pour des requêtes multi-objectifs tout en maintenant l'empreinte mémoire constante caractéristique de la SMC.

Méthodologie

Le papier propose la première approche SMC pour les requêtes de Pareto multi-objectifs, basée sur l'échantillonnage de stratégies légères (LSS - Lightweight Strategy Sampling). La méthodologie centrale repose sur les composants suivants :

1. Échantillonnage de Stratégies Légères (LSS)

Pour gérer le non-déterminisme des processus de décision markoviens (MDP) sans stocker d'informations de stratégie par état, les auteurs utilisent le LSS. Au lieu de stocker explicitement une stratégie, le LSS utilise un identifiant compact (par exemple, un entier de 32 bits) et une fonction de hachage pour résoudre de manière déterministe les choix non déterministes lors de la simulation. Cela permet la simulation d'un vaste nombre de stratégies distinctes en utilisant une mémoire constante, indépendamment de la taille de l'espace d'états du modèle.

2. Approximation Statistique du Front de Pareto

L'approche échantillonne des stratégies déterministes et les évalue via la SMC pour obtenir des intervalles de confiance (CI) pour chaque objectif.

• Boîtes de Confiance : Pour une stratégie $\sigma$ échantillonnée, la SMC produit une boîte de confiance $d$-dimensionnelle $B_\sigma$ autour du vecteur de moyenne estimée $\hat{x}_\sigma$.
• Sous-approximation et Sur-approximation : L'enveloppe convexe des coins « les plus pessimistes » de ces boîtes forme une sous-approximation ($\underline{C}$) candidate de l'ensemble réalisable. Inversement, les coins « les plus optimistes » forment une sur-approximation ($\overline{C}$) candidate.
• Comparaisons Multiples : Pour garantir la correction simultanée de toutes les boîtes de confiance avec une probabilité $\gamma$, les auteurs appliquent la correction de Bonferroni (borne de l'union) afin de répartir le budget d'erreur entre les stratégies et les dimensions.

3. Algorithmes

Le papier introduit deux catégories d'algorithmes :

A. Échantillonnage Incrémental avec Convergence
Ce schéma échantillonne indéfiniment des lots de stratégies. Il ajuste dynamiquement le budget d'erreur par lot (en utilisant un facteur $f$) pour garantir que, dans la limite, les sous- et sur-approximations convergent vers une bande de confiance simultanée autour du véritable front de Pareto. Cela fournit une garantie théorique de convergence presque sûre compte tenu d'un LSS idéal.

B. Échantillonnage à Budget Fixe
Reconnaissant que les applications pratiques disposent d'un temps fini, trois algorithmes heuristiques sont proposés pour trouver la meilleure approximation dans un budget de simulation fixe :

1. Affinement du Vecteur de Poids (WVR - Weight Vector Refinement) : Adapte les techniques de PMC multi-objectifs en linéarisant les objectifs. Il affine itérativement les vecteurs de poids basés sur la distance entre les approximations actuelles et écarte les stratégies sous-optimales.
2. Budget d'Itérations Fixe (FIB - Fixed Iteration Budget) : Échantillonne un ensemble initial de stratégies et effectue des cycles de simulation itératifs, écartant les stratégies les moins performantes à chaque itération pour concentrer le budget sur les candidats prometteurs.
3. Budget de Stratégies Fixe (FSB - Fixed Strategy Budget) : Similaire à FIB, mais garantit que l'ensemble final de stratégies survivantes reçoit un nombre uniforme de cycles de simulation, en échantillonnant de nouvelles stratégies pour remplacer celles qui ont été écartées.

Heuristiques de Sélection de Stratégie :
Pour filtrer les stratégies, les auteurs définissent plusieurs règles basées sur les moyennes d'échantillonnage et les intervalles de confiance (ex: « Simple », « Assez Loin », « Conservativement Loin »). Ces règles déterminent si une stratégie est dominée par une autre avec une confiance statistique suffisante pour être écartée.

Contributions Clés

1. Première SMC Multi-Objectif : Le papier présente le premier cadre SMC capable d'approximer des fronts de Pareto pour $d$ objectifs de priorité égale.
2. Mémoire Constante : L'approche conserve l'avantage principal de la SMC : l'utilisation de la mémoire est constante par rapport à la taille de l'espace d'états du modèle, permettant l'analyse de modèles comportant des milliards d'états.
3. Garanties Statistiques : Le schéma incrémental fournit une garantie théorique de convergence vers une bande de confiance autour du véritable front de Pareto. Les algorithmes à budget fixe fournissent des bornes inférieures statistiquement valides (sous-approximations) avec un niveau de confiance spécifié.
4. Implémentation et Évaluation : Les techniques sont implémentées dans le simulateur modes au sein de la boîte à outils Modest. Les auteurs évaluent l'approche sur 40 instances de référence issues de la littérature de la vérification quantitative et de l'apprentissage par renforcement, en comparant les résultats avec l'outil de PMC Storm.

Résultats Expérimentaux

Les expériences démontrent que l'approche SMC proposée peut gérer des instances où les outils de PMC (Storm) échouent en raison de l'explosion de l'espace d'états ou d'un dépassement de délai (timeout).

• Scalabilité : Pour de grands modèles (ex: fruit_tree avec $2.7 \times 10^9$ états, variantes de puddle_world avec des centaines de millions d'états), l'approche SMC réussit à calculer des approximations de fronts de Pareto en quelques secondes ou minutes, là où les outils de PMC ont expiré ou n'ont pas pu terminer.
• Précision : Pour les modèles plus petits où les résultats de PMC sont disponibles, les approximations SMC correspondent souvent étroitement au véritable front de Pareto (ex: modèles deep_sea et fruit_tree avec un $\epsilon$ multiplicatif proche de 1). Cependant, la précision varie ; pour certains modèles comme breakable_bottles, l'approximation peut être plus éloignée du front réel, soulignant la nature stochastique de l'échantillonnage.
• Performance des Algorithmes : Parmi les algorithmes à budget fixe, le FSB (Fixed Strategy Budget) combiné à l'heuristique Simple et une configuration favorisant un grand nombre de stratégies initiales avec peu de cycles par stratégie, a généralement produit les meilleurs résultats de hypervolume.
• Impact des Heuristiques : La règle « Simple » (écartant les stratégies sur la base des seules moyennes d'échantillonnage) a souvent été la plus performante, suggérant que l'écart précoce des stratégies non prometteuses est bénéfique dans l'ensemble des benchmarks testés.

Signification et Revendications

Les auteurs affirment que ce travail comble une lacune critique entre la scalabilité de la SMC et la complexité de l'optimisation multi-objectif. En exploitant l'échantillonnage de stratégies légères, l'approche permet la vérification des compromis dans des systèmes qui seraient autrement intraitables pour les méthodes exhaustives.

Le papier reconnaît modestement certaines limites :

• Sur-approximation : Bien que le schéma incrémental converge vers une bande de confiance, les algorithmes à budget fixe ne peuvent garantir une sur-approximation valide en temps fini car ils peuvent manquer la stratégie optimale.
• Espace de Stratégies : La méthode suppose un espace de stratégies fini (via des identifiants de taille fixe). Bien que pratique, c'est une limitation par rapport à l'espace théorique infini des stratégies dans les MDP généraux.
• Classe de Modèles : Bien que démontrée sur les MDP, l'approche est directement applicable à toute classe de modèles supportée par le LSS, tels que les automates de Markov et les automates temporels probabilistes, à condition que les exécutions se terminent presque sûrement.

Ce travail est présenté comme une étape fondamentale, offrant un outil pratique pour la vérification multi-objectif dans les systèmes à grande échelle où les méthodes exhaustives traditionnelles sont indisponibles.