The Probabilistic Model Checking Landscape

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

    36 Citations (Scopus)
    191 Downloads (Pure)

    Abstract

    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)
    Pages31-45
    Number of pages15
    ISBN (Print)978-1-4503-4391-6
    DOIs
    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

    Name
    PublisherACM

    Conference

    Conference31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016
    Abbreviated titleLICS
    CountryUnited States
    CityNew York
    Period5/07/168/07/16

    Keywords

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

    Cite this