Advances in Probabilistic Model Checking

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    60 Downloads (Pure)


    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.
    Original languageUndefined
    Title of host publication11th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2010
    EditorsG. Barthe, M. Hermenegildo
    Place of PublicationBerlin
    Number of pages1
    ISBN (Print)978-3-642-11318-5
    Publication statusPublished - Jan 2010

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag


    • IR-72600
    • EWI-18212
    • METIS-270939

    Cite this