Symbolic Counterexample Generation for Discrete-time Markov Chains

Speaker

Nils Jansen

Title Symbolic Counterexample Generation for Discrete-time Markov Chains
When 05.09.2012, 10.00
Where Room 5052
Abstract In this talk we present our new results on the generation of counterexamples for discrete-time Markov chains (DTMCs) and PCTL properties. Whereas most available methods use explicit representations for at least some intermediate results, our aim is to develop fully symbolic algorithms.

As in most related work, our counterexample computations are based on path searches. We first adapt bounded model checking as a path search algorithm and extend it with a novel SAT-solving heuristic to prefer paths with higher probabilities. As a second approach, we use symbolic graph algorithms to find counterexamples. Experiments show that our approaches, in contrast to other existing techniques, are applicable to very large systems with millions of states.

Slides