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

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

Récupéré en direct depuis OpenAlex et désinversé. Les résumés ne sont pas conservés dans cette base de données : les index inversés représentent 8,6 Go des 9,3 Go de texte de la base, et le serveur dispose de 13 Go libres.