After many months of implementation and testing we finally released the DiPro tool for probabilistic counterexample generation tool.
I will give a talk on DiPro’s features on the SPIN 2011 Workshop (July 14-15), co-located with CAV 2011 in Snowbird Utah.
What is DiPro?
Current stochastic model checkers do not make counterexamples for property violations readily available. DiPro is a tool, that applies 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 DiPro very efficient and highly scalable. They can also be guided using heuristics which usually improve the performance of the method.
Counterexamples provided by DiPro 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.
DiPro allows for the computation of counterexamples for the stochastic model checkers PRISM or MRMC.
Thank you very much for this posts. Cheers 🙂
Thank you very much for this posts. Cheers 🙂
Thanks for the good work. But I didn’t find any examples or documentations, which makes it extremely hard to use.