La vérification formelle de systèmes réactifs probabilistes finis

Le champ de notre projet de recherche est la vérification des systèmes probabilistes interactifs. Étant donnée une formule de la logique PCTL, qui décrit les spécifications d'un système probabiliste, et un modèle, nous nous intéressons à vérifier si celui-ci satisfait la formule donnée. Ceci est fait à l'aide d'une méthode formelle appelée le model-checking. Nous nous restreindrons dans ce travail aux systèmes probabilistes finis ayant une structure particulière sans cycle qu'on appellera systèmes par niveaux. Les systèmes considérés ont un nombre fini d'états et les transitions sont quantifiées avec une mesure de probabilité. Nous désirons déterminer si le model-checking d'une telle structure pourrait être amélioré en utilisant la particularité de cette structure. L'application d'un tel algorithme serait de permettre le model-checking efficace pour les systèmes continus. À cet effet, nous avons élaboré une nouvelle méthode de vérification par modelchecking adaptée aux systèmes par niveaux. Celle-ci consiste, étant donné un modèle représentant un système par niveaux et une formule logique PCTL, à déterminer si ce modèle satisfait cette formule à un niveau i donné du système considéré. À partir de cette méthode, nous avons également étudié la complexité qui lui est associée. Celle-ci a été comparée à la complexité de la méthode de vérification classique. Nous en avons conclu que la méthode élaborée est légèrement plus avantageuse en terme de temps que la méthode classique