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.
| Identifer | oai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QQLA.2005/22641 |
| Date | 04 1900 |
| Creators | Nafa, Thouria |
| Contributors | Desharnais, Josée |
| Publisher | Université Laval |
| Source Sets | Library and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada |
| Language | French |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation |
| Format | text/html, application/pdf |
| Rights | © Thouria Nafa, 2005 |
Page generated in 0.0018 seconds