Counterexamples in probabilistic model checking

Tingting Han, Joost P. Katoen

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

38 Citations (Scopus)
46 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
Han, Tingting ; Katoen, Joost P. / Counterexamples in probabilistic model checking. Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems. editor / O. Grumberg ; M. Huth. Berlin, Germany : Springer, 2007. pp. 72-86 (Lecture Notes in Computer Science; Supplement).
@inproceedings{49c6b490cf544a8288266bf70fc1853b,
title = "Counterexamples in probabilistic model checking",
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.",
keywords = "EWI-11507, METIS-245829, IR-64507",
author = "Tingting Han and Katoen, {Joost P.}",
note = "10.1007/978-3-540-71209-1_8",
year = "2007",
month = "7",
day = "31",
doi = "10.1007/978-3-540-71209-1_8",
language = "Undefined",
isbn = "978-3-540-71208-4",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
number = "Supplement",
pages = "72--86",
editor = "O. Grumberg and M. Huth",
booktitle = "Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems",

}

Han, T & Katoen, JP 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., 10.1007/978-3-540-71209-1_8, Lecture Notes in Computer Science, no. Supplement, vol. 4424, Springer, Berlin, Germany, pp. 72-86, 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007, Braga, Portugal, 24/03/07. https://doi.org/10.1007/978-3-540-71209-1_8

Counterexamples in probabilistic model checking. / Han, Tingting; Katoen, Joost P.

Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems. ed. / O. Grumberg; M. Huth. Berlin, Germany : Springer, 2007. p. 72-86 10.1007/978-3-540-71209-1_8 (Lecture Notes in Computer Science; Vol. 4424, No. Supplement).

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

TY - GEN

T1 - Counterexamples in probabilistic model checking

AU - Han, Tingting

AU - Katoen, Joost P.

N1 - 10.1007/978-3-540-71209-1_8

PY - 2007/7/31

Y1 - 2007/7/31

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

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

KW - EWI-11507

KW - METIS-245829

KW - IR-64507

U2 - 10.1007/978-3-540-71209-1_8

DO - 10.1007/978-3-540-71209-1_8

M3 - Conference contribution

SN - 978-3-540-71208-4

T3 - Lecture Notes in Computer Science

SP - 72

EP - 86

BT - Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems

A2 - Grumberg, O.

A2 - Huth, M.

PB - Springer

CY - Berlin, Germany

ER -

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