Model checking meets probability: a gentle introduction

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

    6 Citations (Scopus)
    50 Downloads (Pure)

    Abstract

    This paper considers fully probabilistic system models. Each transition is quantified with a probability—its likelihood of occurrence. Properties are expressed as automata that either accept or reject system runs. The central question is to determine the fraction of accepted system runs. We also consider probabilistic timed system models. Their properties are timed automata that accept timed runs iff all timing constraints resent in the automaton are met; otherwise it rejects. The central question is to determine the fraction of accepted timed system runs.
    Original languageUndefined
    Title of host publicationEngineering Dependable Software Systems
    Place of PublicationAmsterdam
    PublisherIOS Press
    Pages177-205
    Number of pages29
    ISBN (Print)978-1-61499-206-6
    DOIs
    Publication statusPublished - 2013

    Publication series

    NameNATO Science for Peace and Security Series - D: Information and Communication Security
    PublisherIOS Press
    Number34
    Volume34
    ISSN (Print)1874-6268

    Keywords

    • EWI-23887
    • IR-88331
    • METIS-300115

    Cite this

    Katoen, J. P. (2013). Model checking meets probability: a gentle introduction. In Engineering Dependable Software Systems (pp. 177-205). (NATO Science for Peace and Security Series - D: Information and Communication Security; Vol. 34, No. 34). Amsterdam: IOS Press. https://doi.org/10.3233/978-1-61499-207-3-177