Résumé technique : Sur la continuité de la distance de bisimilitude probabiliste

1. Énoncé du problème

La bisimilitude probabiliste est une équivalence comportementale standard pour les chaînes de Markov étiquetées (LMC), utilisée pour minimiser les espaces d'états et vérifier les propriétés des systèmes. Cependant, la bisimilitude exacte est fragile : de petites perturbations dans les probabilités de transition peuvent entraîner la perte totale d'équivalence entre les états. Pour remédier à cela, la distance de bisimilitude probabiliste ($\delta_\tau$) a été introduite comme une mesure quantitative de la différence de comportement, où $\delta_\tau(s, t) = 0$ si et seulement si $s$ et $t$ sont bisimilaires.

Une limitation critique de cette métrique est son potentiel de discontinuité. Comme l'ont noté Jaeger et al. [25], de petits changements dans les probabilités de transition peuvent provoquer des sauts brusques et non négligeables dans la distance entre les états. Ce manque de continuité compromet l'applicabilité de la métrique aux modèles dérivés empiriquement, où les probabilités de transition sont souvent des approximations de données expérimentales. Si la distance est discontinue, s'appuyer sur elle pour fusionner des états ou approximer les résultats de la vérification de modèles peut être dangereux, car la « similitude apparente » peut ne pas être robuste face à l'incertitude.

Dans des travaux antérieurs [17], les auteurs ont introduit la bisimilitude robuste ($\simeq$) comme une condition suffisante pour la continuité de la distance de bisimilitude pour les paires d'états bisimilaires. Cependant, deux questions fondamentales restaient ouvertes :

1. La bisimilitude robuste est-elle également une condition nécessaire pour la continuité ?
2. Comment caractériser et décider la continuité pour des paires d'états non bisimilaires ?

2. Méthodologie et cadre théorique

L'article traite ces questions en étendant le cadre théorique des couplages et des politiques sur l'espace d'états produit $S \times S$.

2.1 Préliminaires

Les auteurs utilisent la définition standard de la bisimulation basée sur les couplages (Définition 3). La distance de bisimilitude $\delta_\tau$ est définie comme le plus petit point fixe d'une fonction $\Delta_\tau$, qui minimise la distance attendue sur tous les couplages des distributions de transition.
Crucialement, la distance est caractérisée via des politiques (Définition 10). Une politique $P$ induit une chaîne de Markov sur $S \times S$. La distance $\delta_\tau(s, t)$ correspond à la probabilité minimale d'atteindre l'ensemble des paires ayant des étiquettes différentes ($S^2_1$) à partir de $(s, t)$ dans la chaîne induite (Proposition 11).

2.2 Bisimilitude robuste et continuité

La bisimilitude robuste ($s \simeq t$) est définie par l'existence d'une politique $P$ telle que la probabilité d'atteindre l'ensemble diagonal $S^2_\Delta$ (où les états sont identiques) à partir de $(s, t)$ est de 1.

• Résultat précédent (Théorème 13) : Si $s \simeq t$, alors $\delta_{(\cdot)}(s, t)$ est continue en $\tau$.
• Nouvelle contribution (Théorème 14) : Les auteurs prouvent la réciproque : pour les états bisimilaires ($s \sim t$), la continuité de la fonction de distance est vérifiée si et seulement si $s \simeq t$. Cela établit la bisimilitude robuste comme une condition nécessaire et suffisante pour la continuité au sein de l'ensemble des paires bisimilaires.

2.3 Caractérisation générale pour des paires arbitraires

L'article étend l'analyse aux paires d'états arbitraires (y compris les non-bisimilaires).

• Théorème 17 : Pour tout $s, t \in S$, la fonction de distance $\delta_{(\cdot)}(s, t)$ est continue en $\tau$ si et seulement s'il existe une politique $P$ telle que la probabilité d'atteindre $S^2_\Delta$ à partir de $(s, t)$ est exactement $1 - \delta_\tau(s, t)$.
  • Cette condition implique que la « perte » pour atteindre la diagonale (qui augmenterait la distance vers 1) est exactement équilibrée par la valeur de la distance elle-même.
  • Si aucune telle politique n'existe (c'est-à-dire que la probabilité maximale d'atteindre la diagonale est strictement inférieure à $1 - \delta_\tau(s, t)$), la distance est discontinue.

2.4 Procédure de décision algorithmique

Sur la base du Théorème 17, les auteurs développent l'Algorithme 1 pour décider de la continuité pour toutes les paires d'états en temps polynomial.

• Mécanisme : L'algorithme calcule l'ensemble des paires discontinues en identifiant de manière itérative les paires qui ne peuvent pas atteindre l'ensemble « robuste » sans passer par un ensemble « mauvais » (paires qui sont bisimilaires mais pas robustement si, ou paires qui mènent inévitablement à des désaccords d'étiquettes).
• Calcul du point fixe : L'algorithme utilise des fonctions monotones $A$ et $B$ sur le treillis des paires d'états. Il calcule le plus petit point fixe $\alpha$ (paires discontinues) et le plus grand point fixe $\beta$ (paires continues).
• Complexité : La vérification des couplages optimaux (ligne 6 de l'Algorithme 1) est réduite à un problème de flot maximum à coût minimum (Proposition 25), soluble en temps polynomial. L'algorithme global s'exécute en temps polynomial par rapport à la taille de l'espace d'états.

3. Contributions clés

1. Nécessité de la bisimilitude robuste : L'article prouve que la bisimilitude robuste est non seulement suffisante mais aussi nécessaire pour la continuité de la distance de bisimilitude pour les paires d'états bisimilaires, résolvant ainsi une conjecture de [17].
2. Caractérisation complète : Les auteurs fournissent une caractérisation théorique complète de la continuité pour toutes les paires d'états (bisimilaires ou non) via le Théorème 17, liant la continuité à l'existence d'une politique spécifique maximisant l'accessibilité à la diagonale.
3. Algorithme de décision en temps polynomial : Un nouvel algorithme est présenté qui décide de la continuité pour toutes les paires d'états en temps polynomial.
4. Validation expérimentale : L'algorithme a été implémenté dans le vérificateur de modèles PRISM. Des expériences sur le Quantitative Verification Benchmark Set (QVBS) et des algorithmes Java randomisés (via jpf-probabilistic) démontrent que décider de la continuité n'ajoute qu'un surcoût minimal par rapport au calcul de la distance elle-même. Dans de nombreux cas, la vérification de la continuité est nettement plus rapide.

4. Résultats et évaluation expérimentale

L'évaluation expérimentale s'est concentrée sur des benchmarks où les modèles minimisés sous la bisimilitude traditionnelle et la bisimilitude robuste diffèrent (indiquant une potentielle discontinuité).

• Efficacité : Pour la plupart des benchmarks, le temps requis pour décider de la continuité était inférieur ou comparable au temps requis pour calculer la distance de bisimilitude. Par exemple, dans le benchmark oscillators, le calcul de la distance a pris environ 5 secondes, tandis que la vérification de la continuité a pris environ 0,002 seconde.
• Cas triviaux : Lorsque la distance est continue pour toutes les paires (par exemple, lorsque la bisimilitude traditionnelle et la bisimilitude robuste coïncident), l'algorithme se termine presque instantanément.
• Praticité : Les résultats confirment que l'étape supplémentaire de vérification de la continuité est informatiquement réalisable et fournit une garantie de robustesse pour les modèles ayant des probabilités de transition incertaines.

5. Signification et revendications

L'article affirme combler les lacunes théoriques concernant la continuité de la distance de bisimilitude probabiliste. En prouvant que la bisimilitude robuste est la condition exacte de la continuité dans le cas de la bisimilitude et en fournissant une caractérisation générale pour toutes les paires, ce travail permet aux praticiens de :

• Évaluer la robustesse : Déterminer si la similitude comportementale entre deux états est stable sous de petites perturbations des probabilités de transition.
• Réduction de modèle sûre : Fusionner en toute sécurité les états dans des modèles dérivés empiriquement uniquement lorsque la continuité est garantie, évitant ainsi le risque de « sauts de distance » qui pourraient invalider les résultats de la vérification de modèles.
• Vérification efficace : Intégrer les vérifications de continuité dans les flux de travail de vérification existants avec un coût de performance négligeable.

Les auteurs notent que bien que le présent travail établisse la décidabilité et la caractérisation, les travaux futurs viseront à fournir des bornes quantitatives sur l'augmentation possible de la distance sous des perturbations et à étudier la continuité sous des perturbations préservant la structure du graphe.