Modélisation et vérification de systèmes probabilistes

L'implication croissante de l'informatique dans des domaines aussi  variés que les télécommunications, les transports, l'économie, ou la  santé, s'accompagne du nécessaire développement de méthodes formelles  de validation des systèmes informatiques. La vérification (ou model- checking) est une des techniques utilisées pour s'assurer du bon  fonctionnement des programmes.

Dans cet exposé nous nous intéresserons plus particulièrement aux modèles et aux algorithmes dédiés aux systèmes présentant des aspects probabilistes. Les aspects probabilistes sont typiquement essentiels pour représenter de façon réaliste les  comportements non fiables et non prévisibles des systèmes.

L'exposé  présentera dans un premier temps les modèles probabilistes classiques  et leurs techniques de vérification associées, puis évoquera quelques récents résultats du domaine.