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)

Abstract

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
PublisherSpringer
Pages331-346
Number of pages16
ISBN (Print)978-3-540-75595-1
DOIs
Publication statusPublished - 2007

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
NumberSupplement
Volume4762

Keywords

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

Cite this

Han, T., & Katoen, J. P. (2007). Providing evidence of likely being on time - Counterexample generation for CTMC model checking. In K. Namjoshi, T. Yoneda, T. Higashino, & Y. Okamura (Eds.), Providing evidence of likely being on time: Counterexample generation for CTMC model checking (pp. 331-346). [10.1007/978-3-540-75596-8_24] (Lecture Notes in Computer Science; Vol. 4762, No. Supplement). Springer. https://doi.org/10.1007/978-3-540-75596-8_24
Han, Tingting ; Katoen, Joost P. / Providing evidence of likely being on time - Counterexample generation for CTMC model checking. Providing evidence of likely being on time: Counterexample generation for CTMC model checking. editor / K. Namjoshi ; T. Yoneda ; T. Higashino ; Y. Okamura. Springer, 2007. pp. 331-346 (Lecture Notes in Computer Science; Supplement).
@inproceedings{42358fb44f34466d96b4bf7d96e5caba,
title = "Providing evidence of likely being on time - Counterexample generation for CTMC model checking",
abstract = "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.",
keywords = "IR-62042, EWI-11508, METIS-245830",
author = "Tingting Han and Katoen, {Joost P.}",
note = "10.1007/978-3-540-75596-8_24",
year = "2007",
doi = "10.1007/978-3-540-75596-8_24",
language = "Undefined",
isbn = "978-3-540-75595-1",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
number = "Supplement",
pages = "331--346",
editor = "K. Namjoshi and T. Yoneda and T. Higashino and Y. Okamura",
booktitle = "Providing evidence of likely being on time: Counterexample generation for CTMC model checking",

}

Han, T & Katoen, JP 2007, Providing evidence of likely being on time - Counterexample generation for CTMC model checking. in K Namjoshi, T Yoneda, T Higashino & Y Okamura (eds), Providing evidence of likely being on time: Counterexample generation for CTMC model checking., 10.1007/978-3-540-75596-8_24, Lecture Notes in Computer Science, no. Supplement, vol. 4762, Springer, pp. 331-346. https://doi.org/10.1007/978-3-540-75596-8_24

Providing evidence of likely being on time - Counterexample generation for CTMC model checking. / Han, Tingting; Katoen, Joost P.

Providing evidence of likely being on time: Counterexample generation for CTMC model checking. ed. / K. Namjoshi; T. Yoneda; T. Higashino; Y. Okamura. Springer, 2007. p. 331-346 10.1007/978-3-540-75596-8_24 (Lecture Notes in Computer Science; Vol. 4762, No. Supplement).

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

TY - GEN

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

AU - Han, Tingting

AU - Katoen, Joost P.

N1 - 10.1007/978-3-540-75596-8_24

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

KW - IR-62042

KW - EWI-11508

KW - METIS-245830

U2 - 10.1007/978-3-540-75596-8_24

DO - 10.1007/978-3-540-75596-8_24

M3 - Conference contribution

SN - 978-3-540-75595-1

T3 - Lecture Notes in Computer Science

SP - 331

EP - 346

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

A2 - Namjoshi, K.

A2 - Yoneda, T.

A2 - Higashino, T.

A2 - Okamura, Y.

PB - Springer

ER -

Han T, Katoen JP. Providing evidence of likely being on time - Counterexample generation for CTMC model checking. In Namjoshi K, Yoneda T, Higashino T, Okamura Y, editors, Providing evidence of likely being on time: Counterexample generation for CTMC model checking. Springer. 2007. p. 331-346. 10.1007/978-3-540-75596-8_24. (Lecture Notes in Computer Science; Supplement). https://doi.org/10.1007/978-3-540-75596-8_24