Sciweavers

Share
TSE
2010

Directed Explicit State-Space Search in the Generation of Counterexamples for Stochastic Model Checking

9 years 10 months ago
Directed Explicit State-Space Search in the Generation of Counterexamples for Stochastic Model Checking
Current stochastic model checkers do not make counterexamples for property violations readily available. In this paper we apply directed explicit state space search to discrete- and continuous-time Markov chains in order to compute counterexamples for the violation of PCTL or CSL properties. Directed explicit state space search algorithms explore the state space on-the-fly which makes our method very efficient and highly scalable. They can also be guided using heuristics which usually improve the performance of the method. Counterexamples provided by our method have two important properties. First, they include those traces which contribute the most amount of probability to the property violation. Hence, they show the most probable offending execution scenarios of the system. Second, the obtained counterexamples tend to be small. Hence, they can be effectively analyzed by a human user. Both properties make the counterexamples obtained by our method very useful for debugging purposes. ...
Husain Aljazzar, Stefan Leue
Added 22 May 2011
Updated 22 May 2011
Type Journal
Year 2010
Where TSE
Authors Husain Aljazzar, Stefan Leue
Comments (0)
books