Extended Directed Search for Probabilistic Timed Reachability

Current numerical model checkers for stochastic systems can efficiently analyse stochastic models. However, the fact that they are unable to provide debugging information constrains their practical use. In precursory work we proposed a method to select diagnostic traces, in the parlance of functional model checking commonly referred to as failure traces or counterexamples, for probabilistic timed reachability properties on discrete-time and continuous-time Markov chains. We applied directed explicit-state search algorithms, like Z , to determine a diagnostic trace which carries large amount of probability. In this paper we extend this approach to determining sets of traces that carry large probability mass, since properties of stochastic systems are typically not violated by single traces, but by collections of those. To this end we extend existing heuristics guided search algorithms so that they select sets of traces. The result is provided in the form of a Markov chain. Such diagnost...

• Type: Conference
• Year: 2006
• Where: FORMATS
• Authors: Husain Aljazzar, Stefan Leue
• Keywords: Diagnostic Trace, Formal Methods, FORMATS 2006, Markov Chains, Stochastic Systems