Return to search

Évaluation symbolique de systèmes probabilistes à espace d'états continu

Nous présentons une méthode symbolique pour représenter des modèles probabilistes
à espace d’états continu (LMP). Ces modèles représentent des systèmes de transitions
qui ont un nombre d’états non-dénombrable. L’objectif de l’utilisation d’une méthode
symbolique est de consommer moins de mémoire lors de l’enregistrement du modèle.
Notre technique pour enregistrer symboliquement les modèles est l’utilisation des diagrammes
de décision binaire à terminaux multiples (MTBDD). Ces diagrammes offrent
la possibilité d’enregistrer des fonctions à variables booléennes, ainsi que des graphes,
de façon plus concise que les techniques plus fréquemment utilisées. Nous employons
les MTBDD dans un vérificateur de modèles de type LMP nommé CISMO.
La vérification de modèles est une technique entièrement automatique qui est utilisée
pour vérifier si un modèle respecte ou non sa spécification. L’espace mémoire nécessaire
pour faire la vérification dépend entre autres des structures utilisées pour enregistrer
le modèle. Dans la première version de CISMO, le modèle était enregistré à l’aide de
structures de données traditionnelles, comme des vecteurs. Cette façon de faire est
qualifiée d’explicite. Nos modifications de CISMO lui permettent maintenant de faire
la vérification de façon symbolique, à l’aide des MTBDD, en plus de la façon explicite.
Nos principales contributions sont la description de deux heuristiques qui, dans certains
contextes, réduisent la taille des diagrammes de décision binaire ordonnés, ainsi que
la modification de CISMO. L’analyse de la mémoire consommée par CISMO après
nos modifications nous montre que l’utilisation des diagrammes de décision permet de
sauver de la mémoire.

Identiferoai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QQLA.2005/22827
Date07 1900
CreatorsPaquette, Simon
ContributorsDesharnais, Josée
PublisherUniversité Laval
Source SetsLibrary and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada
LanguageFrench
Detected LanguageFrench
TypeElectronic Thesis or Dissertation
Formattext/html, application/pdf
Rights© Simon Paquette, 2005

Page generated in 0.0019 seconds