The Probabilistic Model Checking Landscape

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

    83 Citations (Scopus)
    275 Downloads (Pure)


    Randomization is a key element in sequential and distributed computing. Reasoning about randomized algorithms is highly nontrivial. In the 1980s, this initiated first proof methods, logics, and model-checking algorithms. The field of probabilistic verification has developed considerably since then. This paper surveys the algorithmic verification of probabilistic models, in particular probabilistic model checking. We provide an informal account of the main models, the underlying algorithms, applications from reliability and dependability analysis—and beyond—and describe recent developments towards automated parameter synthesis.
    Original languageUndefined
    Title of host publicationProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016)
    Place of PublicationUSA
    PublisherAssociation for Computing Machinery (ACM)
    Number of pages15
    ISBN (Print)978-1-4503-4391-6
    Publication statusPublished - Jul 2016
    Event31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 - Columbia University, New York, United States
    Duration: 5 Jul 20168 Jul 2016
    Conference number: 31

    Publication series



    Conference31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016
    Abbreviated titleLICS
    Country/TerritoryUnited States
    CityNew York


    • EC Grant Agreement nr.: FP7/2007-2013
    • EC Grant Agreement nr.: FP7/318490
    • IR-100650
    • METIS-317201
    • EWI-27009

    Cite this