Automated Verification Techniques for Probabilistic Systems

Abstract : This tutorial provides an introduction to probabilistic model checking, a technique for automatically verifying quantitative properties of probabilistic systems. We focus on Markov decision processes (MDPs), which model both stochastic and nondeterministic behaviour. We describe methods to analyse a wide range of their properties, including specifications in the temporal logics PCTL and LTL, probabilistic safety properties and cost- or reward-based measures. We also discuss multi-objective probabilistic model checking, used to analyse trade-offs between several different quantitative properties. Applications of the techniques in this tutorial include performance and dependability analysis of networked systems, communication protocols and randomised distributed algorithms. Since such systems often comprise several components operating in parallel, we also cover techniques for compositional modelling and verification of multi-component probabilistic systems. Finally, we describe three large case studies which illustrate practical applications of the various methods discussed in the tutorial.
Type de document :
Chapitre d'ouvrage
M. Bernardo and V. Issarny. Formal Methods for Eternal Networked Software Systems (SFM'11), LNCS 6659, Springer, pp.53--113, 2011
Liste complète des métadonnées

Littérature citée [88 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00648037
Contributeur : Hongyang Qu <>
Soumis le : dimanche 4 décembre 2011 - 23:04:18
Dernière modification le : mardi 6 décembre 2011 - 10:41:25
Document(s) archivé(s) le : lundi 5 décembre 2016 - 08:07:20

Fichier

sfm11.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

  • HAL Id : hal-00648037, version 1

Collections

Citation

Vojtech Forejt, Marta Kwiatkowska, Gethin Norman, David Parker. Automated Verification Techniques for Probabilistic Systems. M. Bernardo and V. Issarny. Formal Methods for Eternal Networked Software Systems (SFM'11), LNCS 6659, Springer, pp.53--113, 2011. 〈hal-00648037〉

Partager

Métriques

Consultations de la notice

186

Téléchargements de fichiers

382