Model checking et encadrement stochastique, PRISM

Le "model checking" stochastique est un moyen de vérification des performances des systèmes probabilistes spécifiés à l'aide des chaînes de Markov (discrètes ou continues) et des logiques temporelles comme PCTL (Probabilistic Computational Tree Logic) dans le cas des chaînes discrètes , CSL (Continuous Stochastic Logic) dans le cas des chaînes continues et PRCTL (Probabilistic Reward Computational Tree Logic) dans les chaînes associées à des récompenses.

Le modèle checking stochastique de sûreté de fonctionnement repose sur la vérification de la validité de formules spécifiant des mesures de récompenses à l'état stationnaire et transitoire. On a donc les mêmes problèmes d'explosion combinatoire des espaces d'état lors des vérifications. Actuellement les "model checkers" probabilistes se contentent de calculer exactement les probabilités du modèle et de vérifier ensuite la contrainte spécifiée par la formule. Il est clair que l'utilisation des concepts des bornes stochastiques simplifie dans certains cas, la vérification. Nous avons proposé, dans le cadre de nos travaux, une approche de vérification de ces formules se basant sur les techniques d'encadrement stochastiques. Cette approche réduit la taille de l'espace des états et la complexité de la résolution numérique. Elle permet la vérification des formules spécifiant des mesures de récompenses désignés par les opérateurs suivants : $\mathcal{I}_{I}^{n}(\phi) \mid \mathcal{C}_{I}^{n}(\phi) \mid \mathcal{E}_{I}^{n}(\phi)\mid \mathcal{E}_{I}(\phi)$.

• Le premier opérateur $\mathcal{I}_{I}^{n}(\phi)$ est vérifié si la récompense à l'instant $n$ est états vérifiant la formule $\phi$ est dans l'intervalle I.
• Le deuxième opérateur $\mathcal{C}_{I}^{n}(\phi)$ est vérifié si la valeur de la récompense cumulée depuis l'instant $0$ jusqu'à l'instant $n$ pour les états vérifiant la formule $\phi$ est dans l'intervalle I.
• L'opérateur $\mathcal{E}_{I}^{n}(\phi)$ est vrai si le taux de récompense depuis l'instant $0$ à l'instant $n$ pour les états vérifiant la formule $\phi$ est dans l'intervalle I.
• Et finalement l'opérateur de récompense stationnaire $\mathcal{E}_{I}(\phi)$ est satisfait si la récompense stationnaire des états vérifiant la formule $\phi$ est à valeur dans I.

Ainsi la vérification de ces formules nécessite le calcul des probabilités stationnaires et transitoires à un instant bien déterminé ou à une séquence d'instants succesifs.

Illustrons ceci sur un exemple. On considère un système de file d'attente Geo/D/1/B avec une gestion d'accès de type RED (Random Early Detection). On modélisé par une chaîne de Markov discrète où on ne présente que le nombre de paquets en attente. Ceci est un modèle approché car le mécanisme RED repose sur une destruction probabiliste des paquets entrant avec un seuil qui dépent de la moyenne mobile de la file et non pas de sa valeur instantanée. Néanmoins, on ne représente ici que la valeur actuelle de la taille de la file et on suppose que le taux de rejet du paquet dépend de cette taille. Lorsque la taille de la file dépasse la moitié du buffer, RED commence à rejeter aléatoirement des paquets lors de leur admission. Pour évaluer les pertes des paquets dans la chaîne, on désigne comme fonction de récompense le nombre moyen de paquets perdus par slot. A chaque état est associé sa valeur de récompense et des formules (appelées propositions atomiques) spécifiant l'état.

On associe aux états de la chaîne où il y a des pertes de paquets la formule $\phi=rejet$ et à l'état où le buffer est plein la formule $\phi=plein \wedge rejet$. $\phi$ peut aussi s'exprimer suivant les logiques temporelles PCTL ou CSL, exemple $\phi=\diamond^{k}plein$ spécifiant les états pour lesquels on atteint l'état du système plein dans au plus $k$ étapes. S'intéréssant à mesurer des récompenses pour les états qui vérifient la formule $\phi$, le "model checking" possède des opérateurs qui expriment les mesures de récompense du système et en particulier dans les états qui vérifient $\phi$. Dans le cas de la file exemple, pour évaluer le taux de rejet des paquets depuis l'instant $0$ jusqu'à l'instant $n$ et voir s'il dépasse ou pas un certain seuil $r$, il suffit de vérifier l'opérateur $\mathcal{E}_{I}^{n}(rejet)$ avec $I=[0, r]$ dans le "model checker".

En utilisant des récompense qui sont croissantes, on peut employer des bornes "st" sur la chaine pour obtenir une borne sup ou inf des récompenses et il est possible d'éviter de calculer les distributions de la chaîne d'origine. La vérification des formules s'effectue en comparant les récompenses des bornes inférieures et supérieures avec les seuils de l'intervalle $I=[a,b]$. Soit min et max les bornes inf et sup calculées, on a quatre cas en général:

1. $min$ et $max$ sont dans $I$. On peut donc conclure "Oui" immédiatement

2. $min$ est supérieur à $b$. On peut donc conclure "Non" immédiatement.

3. $max$ est inférieur à $a$. On peut donc conclure "Non" immédiatement.

4. $min$ est inférieur à $a$ ou $max$ est supérieur à $b$, on ne peut alors rien conlure avec cette borne. Il faut améliorer la borne ou dans le pire des cas, faire le calcul exact.

La stratégie de constructon des partitions pour l'algorithme LIMSUB repose d'abord sur la division de l'espace d'états en deux sous-ensembles : le premier, $S_{yes}$, contient les états qui satisfont la formule $\phi$ et le deuxième, $S_{no}$, contient les états qui ne la satisfont pas. On réduit avec cette décomposition le travail uniquement sur l'espace d'état $S_{yes}$. De plus, on agrège les états de $S_{yes}$ qui ont des valeurs de récompense proches pour obtenir un espace d'état plus petit et on calcule les bornes (supérieures et inférieures) sur les chaînes bornantes de taille inférieure à celle des chaînes de Markov d'origine.