Counterexamples in probabilistic model checking

Tingting Han, Joost P. Katoen

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

    39 Citations (Scopus)
    92 Downloads (Pure)

    Abstract

    This paper considers algorithms for counterexample generation for (bounded) probabilistic reachability properties in fully probabilistic systems. Finding the strongest evidence (i.e, the most probable path) violating a (bounded) until-formula is shown to be reducible to a single-source (hop-constrained) shortest path problem. Counterexamples of smallest size that are mostly deviating from the required probability bound can be computed by adopting (partially new hopconstrained) k shortest paths algorithms that dynamically determine k.
    Original languageUndefined
    Title of host publicationProceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems
    EditorsO. Grumberg, M. Huth
    Place of PublicationBerlin, Germany
    PublisherSpringer
    Pages72-86
    Number of pages15
    ISBN (Print)978-3-540-71208-4
    DOIs
    Publication statusPublished - 31 Jul 2007
    Event13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007 - Braga, Portugal
    Duration: 24 Mar 20071 Apr 2007
    Conference number: 13

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    NumberSupplement
    Volume4424

    Conference

    Conference13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007
    Abbreviated titleTACAS
    CountryPortugal
    CityBraga
    Period24/03/071/04/07

    Keywords

    • EWI-11507
    • METIS-245829
    • IR-64507

    Cite this

    Han, T., & Katoen, J. P. (2007). Counterexamples in probabilistic model checking. In O. Grumberg, & M. Huth (Eds.), Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (pp. 72-86). [10.1007/978-3-540-71209-1_8] (Lecture Notes in Computer Science; Vol. 4424, No. Supplement). Berlin, Germany: Springer. https://doi.org/10.1007/978-3-540-71209-1_8