Advances in Probabilistic Model Checking

Abstract : Probabilistic model checking is an automated verification method that aims to establish the correctness of probabilistic systems. Probability may arise, for example, due to failures of unreliable components, communication across lossy media, or through the use of randomisation in distributed protocols. Probabilistic model checking enables a range of exhaustive, quantitative analyses of properties such as "the probability of a message being delivered within 5ms is at least 0.89". In the last ten years, probabilistic model checking has been successfully applied to numerous real-world case studies, and is now a highly active field of research. This tutorial gives an introduction to probabilistic model checking, as well as presenting material on selected recent advances. The first half of the tutorial concerns two classical probabilistic models, discrete-time Markov chains and Markov decision processes, explaining the underlying theory and model checking algorithms for the temporal logic PCTL. The second half discusses two advanced topics: quantitative abstraction refinement and model checking for probabilistic timed automata. We also briefly summarise the functionality of the probabilistic model checker PRISM, the leading tool in the area.
Type de document :
Chapitre d'ouvrage
O. Grumberg and T. Nipkow and J. Esparza. Proc. 2011 Marktoberdorf Summer School: Tools for Analysis and Verification of Software Safety and Security, IOS Press, 2012
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00664777
Contributeur : Hongyang Qu <>
Soumis le : mardi 31 janvier 2012 - 14:44:04
Dernière modification le : mercredi 1 février 2012 - 11:11:32
Document(s) archivé(s) le : mercredi 14 décembre 2016 - 04:06:35

Fichier

marktoberdorf11.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : hal-00664777, version 1

Collections

Citation

Marta Kwiatkowska, David Parker. Advances in Probabilistic Model Checking. O. Grumberg and T. Nipkow and J. Esparza. Proc. 2011 Marktoberdorf Summer School: Tools for Analysis and Verification of Software Safety and Security, IOS Press, 2012. 〈hal-00664777〉

Partager

Métriques

Consultations de la notice

229

Téléchargements de fichiers

185