Abstract
Random phenomena occur in many applications: security, communication protocols, distributed algorithms, and performance and dependability analysis, to mention a few. In the last two decades, efficient model-checking algorithms and tools have been developed to support the automated verification of models that incorporate randomness. Popular models are Markov decision processes and (continuous-time) Markov chains. Recent advances such as compositional abstraction-refinement and counterexample generation have significantly improved the applicability of these techniques. First promising steps have been made to cover more powerful models, real-time linear specifications, and parametric model checking. In this tutorial I will describe the state of the art, and will detail some of the major recent advancements in probabilistic model checking.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsAuthor information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Katoen, JP. (2010). Advances in Probabilistic Model Checking. In: Barthe, G., Hermenegildo, M. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2010. Lecture Notes in Computer Science, vol 5944. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11319-2_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-11319-2_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11318-5
Online ISBN: 978-3-642-11319-2
eBook Packages: Computer ScienceComputer Science (R0)