Counterexamples in probabilistic model checking

Tingting Han; Joost P. Katoen

doi:10.1007/978-3-540-71209-1_8

Counterexamples in probabilistic model checking

Tingting Han, Joost P. Katoen

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

48 Citations (Scopus)

209 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 language	Undefined
Title of host publication	Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems
Editors	O. Grumberg, M. Huth
Place of Publication	Berlin, Germany
Publisher	Springer
Pages	72-86
Number of pages	15
ISBN (Print)	978-3-540-71208-4
DOIs	https://doi.org/10.1007/978-3-540-71209-1_8
Publication status	Published - 31 Jul 2007
Event	13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007 - Braga, Portugal Duration: 24 Mar 2007 → 1 Apr 2007 Conference number: 13

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Number	Supplement
Volume	4424

Conference

Conference	13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007
Abbreviated title	TACAS
Country/Territory	Portugal
City	Braga
Period	24/03/07 → 1/04/07

Keywords

EWI-11507
METIS-245829
IR-64507

Access to Document

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

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). Article 10.1007/978-3-540-71209-1_8 (Lecture Notes in Computer Science; Vol. 4424, No. Supplement). Springer. https://doi.org/10.1007/978-3-540-71209-1_8

@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 ; 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007 ; Conference date: 24-03-2007 Through 01-04-2007",

year = "2007",

month = jul,

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",

address = "Germany",

}

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 proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Counterexamples in probabilistic model checking

AU - Han, Tingting

AU - Katoen, Joost P.

N1 - Conference code: 13

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

T2 - 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007

Y2 - 24 March 2007 through 1 April 2007

ER -