Counterexamples in probabilistic model checking


Han, Tingting and Katoen, Joost-Pieter (2007) Counterexamples in probabilistic model checking. In: 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007, 24 March - 1 April 2007, Braga, Portugal (pp. pp. 72-86).

open access
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.
Item Type:Conference or Workshop Item
Copyright:© 2007 Springer
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Official URL:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 245829