Providing evidence of likely being on time – Counterexample generation for CTMC model checking


Share/Save/Bookmark

Han, T. and Katoen, J.P. (2007) Providing evidence of likely being on time – Counterexample generation for CTMC model checking. In: Providing evidence of likely being on time: Counterexample generation for CTMC model checking, 22-25 Oct 2007, Tokyo, Japan.

[img]PDF
Restricted to UT campus only
: Request a copy
185Kb
Abstract:Probabilistic model checkers typically provide a list of
individual state probabilities on the refutation of a temporal logic formula. For large state spaces, this information is far too detailed to act as useful diagnostic feedback. For quantitative (constrained) reachability problems, sets of paths that carry enough probability mass are more adequate. We recently have shown that in the context of discrete-time probabilistic processes, such sets of smallest size can be efficiently computed by (hop-constrained) $k$-shortest path algorithms. This paper considers the problem of generating counterexamples for continuous-time Markov chains. The key contribution is a set of approximate algorithms for computing small sets of paths that indicate the violation of time-bounded (constrained) reachability probabilities.
Item Type:Conference or Workshop Item
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/62042
Official URL:http://dx.doi.org/10.1007/978-3-540-75596-8_24
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 245830