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
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 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. |