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

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

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