| abstract |
Currently, stochastic model checkers can efficiently analyse stochastic
models. However, they are unable to provide diagnostics information.
This constrains the practical use of stochastic model checking. In this
talk I will present our method to select diagnostic traces for
probabilistic timed reachability on discrete-time Markov chains. We
employ directed explicit-state search algorithms to such diagnostic
traces carrying a high amount of probability. Additionally, some initial
ideas will be presented how to use visualization techniques to present
the result in an comprehendible way.
|
