Providing evidence of likely being on time - Counterexample generation for CTMC model checking

Tingting Han, Joost P. Katoen

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

    13 Citations (Scopus)


    Probabilistic model checkers typically provide a list of individual state probabilities on the refutation of a temporal logic formula. For large state spaces, this information is far too detailed to act as useful diagnostic feedback. For quantitative (constrained) reachability problems, sets of paths that carry enough probability mass are more adequate. We recently have shown that in the context of discrete-time probabilistic processes, such sets of smallest size can be efficiently computed by (hop-constrained) $k$-shortest path algorithms. This paper considers the problem of generating counterexamples for continuous-time Markov chains. The key contribution is a set of approximate algorithms for computing small sets of paths that indicate the violation of time-bounded (constrained) reachability probabilities.
    Original languageUndefined
    Title of host publicationProviding evidence of likely being on time: Counterexample generation for CTMC model checking
    EditorsK. Namjoshi, T. Yoneda, T. Higashino, Y. Okamura
    Number of pages16
    ISBN (Print)978-3-540-75595-1
    Publication statusPublished - 2007

    Publication series

    NameLecture Notes in Computer Science


    • IR-62042
    • EWI-11508
    • METIS-245830

    Cite this