Model Checking Stochastique

Le model checking déterministe reposant sur CTL (Computationnal Tree Logic) dispose d'algorithmes efficaces contre l'explosion combinatoire des états (par exemple, la réduction sur les ordres partiels et les BDD (binary decision diagrams). Il est alors envisageable de vérifier une propriété logique sur un espace d'états très grand pour tester des systèmes en vraie grandeur. Cela n'est pas encore le cas pour des systèmes probabilistes fautes d'algorithmes efficaces associés aux opérateurs probabilistes employés. On se place ici dans le formalisme CSL une extension stochastique de CTL faisant l'objet de travaux depuis 99 dans la communauté PAPM (Process Algebra and Performance Model) à laquelle nous participons.

CSL ajoute deux opérateurs à CTL pour traiter les comportements stationnaires et les transitoires. Les opérateurs de chemin $until \cal U$ et $next X$ sont étendus pour comprendre un intervalle de temps. La propriété la plus importante est que les mesures exprimées en CSL ne représentent pas une valeur mais une contrainte numérique à respecter. Ainsi $S_{\unlhd p} (\Phi)$ signifie que la probabilité stationnaire de l'ensemble $\Phi$ est inférieure à $p$. De la même façon, ${\cal P}_{\unlhd p} (\phi)$ signifie que les chemins satisfaisant $\phi$ sont de probabilité inférieure à $p$.

Les propriétés d'existence de chemin de probabilité non nulle et sans modèle de temps se traduisent par des propriétés déterministes d'existence de chemin. Elles peuvent donc être traités par des algorithmes sur les problèmes déterministes, moyennant quelques hypothèses stochastiques simples. Par contre, les formules faisant intervenir des seuils de probabilités sont calculées explicitement, ce qui est impossible dès que l'espace contient de l'ordre de $10^6$ états atteignables.

Les ``modèle checker'' probabilistes ne permettent pas actuellement de tirer partie de cette définition des mesures à base de seuil. Ils se contentent de calculer exactement les probabilités du modèle initial et de vérifier ensuite la contrainte. Il est clair que les concepts de bornes stochastiques ou de bornes de probabilités permettent de simplifier grandement certaines de ces vérifications.

Le but du projet est donc aussi de fournir des algorithmes de bornes numériques associées à des structures employées en ``model checking'' (par exemple, la représentation tensorielle ou les BDDs). ces algorithmes pourront alors être intégrés à des outils de model checking par les équipes du domaine.