Counterexamples in probabilistic model checking


Share/Save/Bookmark

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.

[img]
Preview
PDF
151Kb
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
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/64507
Official URL:http://dx.doi.org/10.1007/978-3-540-71209-1_8
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 245829