### Abstract

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

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 | Portugal |

City | Braga |

Period | 24/03/07 → 1/04/07 |

### Keywords

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

### Cite this

*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

}

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

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