Symbolic counterexample generation for large discrete-time Markov chains ?
We present a general framework for generating counterexamples symbolically for large discrete-time Markov chains. We use SAT-solving techniques as well as symbolic graph algorithms. We provide a large comparison between explicit and symbolic approaches for counterexample generation. Our benchmarks show that we are able to generate counterexamples for systems with billions of states.
counterexample markov chain model checking binary decision diagram